Equivalence checking
Direct answerProving that two artifacts compute the same function, for example optimised assembly against a Cryptol reference, or the KEVM semantics against a Lean EVM model.
In more detail
Equivalence checking is how existing optimised code gets verified without rewriting it. Its limit is that the reference must itself be trusted or verified.
Frameworks that address it
Cryptol and SAW, CryptoLine, K framework and KEVM.
Related terms
Circuit soundness, Circuit completeness, Underconstrained circuit, Overconstrained circuit, Symbolic vs computational model, Specification gap, Trusted computing base and verification boundary, Proof assistant vs SMT-based verifier, Bounded model 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).