Quad-Tier Formal Verification
In systems that secure billions of dollars in institutional assets, empirical unit testing is insufficient. The Higgaion PQC Migration Engine is mathematically verified using four independent formal methods, each targeting different property classes. Exactly 107 formal proofs compile with absolutely zero admitted lemmas.Semantic Equivalence (Princeton VST / Coq)
Going beyond abstract "toy" specifications, Tier 1 verification leverages Princeton's Verifiable Software Toolchain (VST). By parsing the exact live C-Core code using clightgen, we map the verifiable bounds directly onto the generated C-AST (pqc_vst_ast.v), mathematically proving literal semantic equivalence and memory-safety parameters at the exact compiler execution level.
The Higgaion Coq/VST environment guarantees properties over 107 mechanized proofs. Across the abstract PQCMigration.v Finite State Machine models and the root body_migration_hybrid_verify VST theorem, there are zero admitted lemmas. Every cryptographic boundary, pointer isolation, and logic execution is fully proven from first principles before reaching production.
Properties verified include: state machine transition correctness and completeness, execution equivalence of the C codebase against its protocol bounds, WAL ordering (Erasure-Before-WAL), semantic disjunctive verification safety, and the absolute destruction of legacy material without memory fault probability.
Coq Proof Modules
| Module | Properties Verified |
|---|---|
vst_pqc_migration.v | Semantic execution equivalence mapped onto clightgen C-AST boundaries |
pqc_vst_ast.v | Extracted live C code representation utilized by VST for memory safety modeling |
PQCMigration.v | State machine bounds, WAL ordering restrictions, Erasure-Before-WAL crash recovery |
HiggaionTypes.v | Strict type enumerations, bounds tracking, and state isolation checks |
Liveness Checking (TLA+)
TLA+ (Temporal Logic of Actions) is a formal specification language developed by Leslie Lamport for describing and reasoning about concurrent and distributed systems. The TLC model checker exhaustively explores all reachable states of a system to verify safety and liveness properties.
The Higgaion TLA+ development comprises 3 specifications modeling the state machine with 3 keys and 8 operations per key. The TLC model checker verifies 16 safety invariants across all reachable states, including:
| Invariant | Property |
|---|---|
TypeOK | State values are within the valid enum range |
NoSkipToFinal | No direct CLASSICAL to FINALIZING transition |
RollbackOnlyFromHybridOrFinalizing | Rollback only permitted from HYBRID or FINALIZING |
PqcOnlyTerminal | PQC_ONLY state is strictly irreversible |
ClassicalKeyExists | Classical key material exists when state < PQC_ONLY |
PqcKeyExists | PQC key material exists when state ≥ HYBRID |
Pointer Validation (CBMC)
CBMC (C Bounded Model Checker) is a bounded model checker for ANSI C programs. It uses SAT/SMT solving to exhaustively check all execution paths up to a configurable loop unwind depth, verifying the absence of buffer overflows, null pointer dereferences, integer overflows, and undefined behavior.
The Higgaion CBMC development includes 13 verification harnesses that mathematically prove the absolute absence of memory leaks and undefined behavior up to unwind depth 25. Properties verified include array bounds checking across all buffer operations, null pointer safety for every pointer dereference, enum range validation for state machine variables, and correct WAL record packing/unpacking.
Deductive Contracts (Frama-C WP)
Frama-C with the Weakest Precondition (WP) plugin enables deductive verification of C code using ACSL (ANSI/ISO C Specification Language) annotations. Function contracts specify preconditions (requires), postconditions (ensures), and frame conditions (assigns) that are verified using SMT solvers.
The Higgaion Frama-C development verifies 40 ACSL annotations across the core migration engine functions. These contracts prove absence of buffer overflows, correct return value semantics, memory safety at the function level, and that each function modifies only the memory locations it declares.
Why Four Tiers?
Each formal method targets a different property class that the others cannot efficiently verify. TLA+ excels at concurrent system properties but cannot reason about C pointer arithmetic. CBMC can prove memory safety but cannot reason about high-level protocol invariants. Coq provides the strongest guarantees but operates on mathematical models, not directly on C source code. Frama-C bridges the gap by verifying C function contracts at the source level.
Together, these four methods cover the full spectrum: protocol-level safety (TLA+), implementation-level memory safety (CBMC), function-level contract verification (Frama-C), and mathematical invariant proofs (Coq). No single tool is sufficient. The combination provides defense in depth for the formal verification itself.
Examine the Proofs
All formal verification artifacts are open-source and available for independent review on GitHub.