sorryfreeLast reviewed 2026-09-13
Index › Glossary › Specification gap

Specification gap

Direct answerA mismatch between the property that was formally proved and the property that was actually needed, so a valid proof fails to cover real behaviour.

In more detail

The public example is sp1-lean's JALR theorem, which assumed a 4-byte-aligned jump target and therefore did not cover legitimate programs; the Ethereum Foundation disclosed the bug in May 2026. The Verification Theatre paper documents the same phenomenon in verified ML-KEM code. Reading the theorem statements and assumptions is as important as checking that the proof compiles.

Circuit soundness, Circuit completeness, Underconstrained circuit, Overconstrained circuit, Symbolic vs computational model, Trusted computing base and verification boundary, Proof assistant vs SMT-based verifier, Bounded model checking, Equivalence checking, Refinement, Constant-time verification, Arithmetization (R1CS, PLONKish, AIR), Extraction (code to model), Witness generation vs constraints

Getting help

Firms on this index that handle this in practice: zkSecurity, Galois, Veridise, Nethermind (Formal Verification team).

Last reviewed 2026-09-13 by the sorryfree editors. Machine-readable: data.json · summary.txt