Polyglot Formal Software Verification Constellation
A closed-loop architecture binding production languages to the OmegaHeart Lean 4 interactive theorem prover. Proving relational soundness, dataflow liveness, concurrency safety, and memory integrity with lossless 3-way CST reconciliation and mobile tactile bug hunting.
Architectural Philosophy
Stratified Verification Tiers
The APAF Constellation categorizes verification engines into four formal tiers according to verification depth and maturity, complemented by a gamified mobile tactile bug-hunting ecosystem.
OmegaHeart
Lean 4 Dependent Type Kernel & Master Catalog
The single authoritative source of mathematical truth across the entire constellation. Houses machine-checked dependent types, Kleene 3-valued logics, communicating sequential processes (CSP), and the central diagnostic schema (schema/diagnostic_catalog.json).
- ✓ Calculus of Inductive Constructions (CIC)
- ✓ Strict Zero-Sorry Invariant
- ✓ Universal Diagnostic Schema Target
Production Engines
GeneralKeen, OuroPy, Roar
Production-grade formal verification engines with comprehensive automated proof synthesis, path-sensitive VCG bug hunting, SMT constraint solving (Z3/Pyright), and full functional R purity proofs.
- ✓ GeneralKeen: Rust CIC Kernel & VCG Bug Hunter
- ✓ OuroPy: Python SMT & LibCST Lossless Repair
- ✓ Roar: R Functional AST to Lean 4 Compiler
Early Development
Torc, Sieve, OuroFlow, Gorget, Corselet
High-impact formal engines actively under development. Featuring independent benchmark tournaments, formal graph solvers, and initial CST semantic reconcilers across complex architectures.
- ✓ Torc (React DAG) & Sieve (SQL 3VL / DuckDB)
- ✓ OuroFlow (Nextflow KPN Dataflow Invariants)
- ✓ Gorget (Go CSP) & Corselet (C Memory Bounds)
Lightweight Sanitizers
Ruby (Rune) & Perl (Purly)
Laser-focused, single-pass zero-allocation static analyzers engineered for dynamic scripting and legacy pipelines. Target high-leverage hazards with sub-5ms CI/CD audit latencies.
- ✓ Rune: Ruby Frozen Mutations & N+1 Queries
- ✓ Purly: Perl Autovivification & 2-Arg Open Traps
- ✓ Pure Rust standalone token scanners
Constellation Mobile & Showcase
Constellation-Android, Android-Bench, Bug-Dex-Template
A complete gamified mobile experience and decentralized showcase substrate. Scan any public GitHub repository on your phone, hunt bugs in parallel across 9 languages, solve CST patch puzzles to accumulate XP, and publish trophies directly to your personal GitHub Pages portfolio (my-bug-dex) without needing repo commit rights.
Comprehensive Taxonomy
Technical Matrix & Execution Profile
| Package | Tier Classification | Target Domain | Formal Invariants Checked | Proof Obligations | Reconciler Tech | Independent Bench / Release |
|---|---|---|---|---|---|---|
| OmegaHeart | Tier 0 • Kernel | Formal Verification | Proof Calculus, TriBool 3VL, CSP Concurrency, KPN | Strict 0 Sorry | Self-Verifying Lake | OmegaHeart-bench ↗ |
| GeneralKeen | Tier 1 • Production | Rust / Systems | VCG Safety, Charon/Aeneas, Boundary Specs, Halting | Path-Sensitive VCG | 3-Way Semantic Merge | generalkeen-bench ↗ |
| OuroPy | Tier 1 • Production | Python Scientific | Type Narrowing, Shape Preservation, Z3 SMT Bounds | Ternary AST • SMT | Lossless CST (libcst) | ouropy-bench ↗ |
| Roar | Tier 1 • Production | R Statistical | Loop-Free Functional Purity, S3/S4 Dispatch, Dim Safety | AST Functional Proofs | R Parse Tree Repair | roar-bench ↗ |
| Torc | Tier 2 • Early Dev | TypeScript / React | Reactivity Cycles (E039), Hook Rules, Reducer Bisim | Reactivity DAG Model | 3-Way CST (Comment-Safe) | torc-bench ↗ |
| Sieve | Tier 2 • Early Dev | Relational SQL | 3VL NOT IN Nulls (E101), Join Hypergraphs, Pagination | Kleene 3VL • DuckDB | SQL In-Place Rewriter | sieve-bench ↗ |
| OuroFlow | Tier 2 • Early Dev | Nextflow DSL2 | Kahn Process Networks, Channel Linearity, Tuple Arity | Dataflow Liveness | DSL2 Channel Reconciler | ouroflow-bench ↗ |
| Gorget | Tier 2 • Early Dev | Go (Golang) | Channel Deadlock (GO-E01), Goroutine Leaks, Lock Inversion | CSP Algebra Model | Go AST Synthesizer | gorget-bench ↗ |
| Corselet | Tier 2 • Early Dev | C / Systems | Spatial Overflow (C-E01), Use-After-Free, Linear Heap | Linear Heap Invariants | C-to-Rust Transpiler | corselet-bench ↗ |
| Rune | Tier 3 • Sanitizer | Ruby | Frozen Object Mutation (RB-E01), N+1 Queries, Ractor Bounds | Fast Token Matcher | Ruby Source Rewriter | rune-bench ↗ |
| Purly | Tier 3 • Sanitizer | Perl 5 | Autovivification (PL-E01), Taint Mode, Bareword Handles | Single-Pass Scanner | Token Rewriter | purly-bench ↗ |
| Constellation-Android | Mobile • App | Android Mobile Game | Tactile Bug Hunter, Polyglot Verification, Trophy Sync | Pure Rust Core • JNI | In-Game CST Solver | v1.0.0 APK ↗ |
| Constellation-Android-Bench | Mobile • Bench | Polyglot Tournament | 27 Ground Truth Cases across all 9 target languages | 100% Prec / Recall | Parallel Rust Engine | android-bench ↗ |
| Bug-Dex-Template | Mobile • Showcase | GitHub Pages Substrate | Personal Bug Portfolio, CST Diff Viewer, Proof Modals, SVG Badges | JSON Schema v1.0.0 | my-bug-dex Demo ↗ | template repo ↗ |
Repository Directory
Explore the Constellation
Direct links to verified engine codebases, diagnostic sets, and benchmark suites.
OmegaHeart
Lean 4 Substrate & Universal Schema
Central dependent type kernel holding verified definitions and propositions for all downstream engines. Enforces the strict 0 sorry / 0 native_decide gate.
GeneralKeen
Rust VCG Bug-Hunter & Transpiler
Deep Calculus of Inductive Constructions engine, Charon/Aeneas translation, Prove2Me Tier 1 proof synthesis, and path-sensitive VCG bug hunting.
OuroPy
Scientific Python SMT Verifier
Closed-loop Python verification linking Pyright type narrowing and Z3 SMT solvers to Lean 4 formal contracts with libcst lossless repair.
Roar
R-to-Lean-to-R Compilation
AST parsing, functional purity verification, zero imperative loop enforcement, S3/S4 object-oriented semantics, and dimension safety.
Torc
React Reactivity & State Verifier
Reactivity DAG cycle detection (E039), Hook rules enforcement, pure reducer revert bisimulation, unkeyed dynamic lists, and 3-way CST merge.
Sieve
Relational Invariant Evaluator & Reconciler
Models ANSI SQL 3VL, Cartesian join hypergraphs, non-deterministic pagination under LIMIT/OFFSET, and functional dependencies against DuckDB.
OuroFlow
Workflow Dataflow & KPN Engine
Kahn Process Network dataflow deadlock-freedom, queue channel linearity, process tuple arity, container isolation, and resume cache invariants.
Gorget
CSP Concurrency & Channel Verifier
Communicating Sequential Processes (CSP) deadlock freedom, unbuffered channel bounds, goroutine leak invariants, and mutex lock hierarchy.
Corselet
C Spatial & Temporal Memory Safety
Linear heap balance, spatial buffer bounds, use-after-free, coordinate arithmetic overflow, strict aliasing, and C-to-Rust synthesis.
Rune
Ruby Immutability & Query Bounds
Targeted invariant checker for frozen object mutations (RB-E01), ActiveRecord N+1 queries (RB-E02), Ractor isolation, and method_missing totality.
Purly
Perl Scope & Taint Sanitizer
High-speed sanitizer targeting accidental hash autovivification (PL-E01), two-argument open command injections (PL-E06), bareword filehandles, and ReDoS.
Constellation-Android
Tactical Mobile Bug Hunter
Sci-fi tactical mobile game in Jetpack Compose + pure Rust core. Enter any public GitHub URL to sweep in parallel (< 150 ms), catch bugs, solve CST patches, and accumulate XP trophies.
Constellation-Android-Bench
Independent Polyglot Tournament Suite
Headless tournament bench evaluating the native multi-language core engine across 27 ground-truth test cases spanning SQL, React, Go, C, Python, Ruby, Perl, R, and Rust.
Bug-Dex-Template
Personal Verified Bug Portfolio Substrate
Ready-to-fork template for publishing caught bug cards, side-by-side CST patch diffs, Lean 4 proof modals, and dynamic SVG profile badges (my-bug-dex).