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. Over 101 Coq theorems compile with absolutely zero admitted lemmas.
Deductive Reasoning (Coq / Rocq)
Coq (now Rocq 9.1.1) is an interactive theorem prover that allows writing mathematical definitions, executable algorithms, and proofs, then machine-checks those proofs for correctness. Unlike testing, which can only verify a finite number of cases, Coq proofs verify properties over all possible inputs and states.
The Higgaion Coq development contains over 101 mechanized theorems written in Gallina (Coq's specification language) across 24 proof files. Every theorem is fully proved from first principles. There are zero admitted lemmas, meaning no assumptions, no placeholders, and no skipped proofs. The Coq compiler independently verifies every single proof step.
Properties verified include: state machine transition correctness and completeness, WAL ordering guarantees (erasure before irreversible WAL write), disjunctive verification soundness, crash recovery safety (no resurrection of erased key material), self-test gating completeness, and the Gateway's strict isolation invariants.
Coq Proof Modules
| Module | Properties Verified |
|---|---|
PQCMigration.v | State machine transitions, WAL ordering, crash recovery, self-test gating |
Gateway.v | Strict isolation invariants, JWT validation, L7 inspection guards |
HiggaionTypes.v | Type definitions, state enumeration correctness, decidable equality |
BellLaPadula.v | Multi-level security lattice, no-read-up / no-write-down properties |
TokenConservation.v | Supply conservation across shard boundaries |
UTXOSafety.v | Double-spend prevention, UTXO lifecycle correctness |
MerkleTree.v | Path verification, root consistency, inclusion proofs |
Consensus.v | Quorum agreement, view change safety |
LockOrder.v | Deadlock freedom, ordered acquisition invariants |
ShardMigration.v | Cross-shard state consistency during migration |
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.