sorryfreeLast reviewed 2026-09-13
Index › Glossary › Bounded model checking

Bounded model checking

Direct answerExhaustive exploration of all program executions up to a fixed depth or loop bound, reporting concrete counterexamples; sound only within the bound.

In more detail

Kani and CBMC are the cheapest verification most cryptographic Rust and C code will ever get: memory safety, absence of panics and user assertions with no specification language. They are not proofs of correctness against a cryptographic spec.

Frameworks that address it

Kani, CBMC.

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, 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