CBMC

Direct answerCBMC is the bounded model checker behind Kani and the memory-safety proofs of mlkem-native and AWS s2n. It proves absence of memory errors and assertion failures in C within loop bounds.

Maintainer: Diffblue, AWS and community
Website: https://github.com/diffblue/cbmc
Repository: https://github.com/diffblue/cbmc
Category: Verified implementations
Targets: Cmlkem-natives2n
Approach: Bounded model checking for memory safety and assertions
Access: Open source (BSD-4)
Status (2026-09-13): Active, mature

Last reviewed 2026-09-13 by the sorryfree editors.

What CBMC does

mlkem-native pairs CBMC memory-safety proofs with s2n-bignum functional proofs, a pragmatic model for post-quantum C libraries.

Where it is strong

Mature and widely deployed.
Concrete counterexamples.
No spec needed for memory safety.

Limits and caveats

Bounded.
No functional correctness.
Modelling effort for harnesses.

When to choose it

Use CBMC on C cryptographic code for memory safety before any deeper verification.

Who works with CBMC

No firm on this index lists CBMC as a core tool yet; the firms below cover the same problem class.

Top-listed for implementation verification work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website

Jasmin and libjade, hax, Cryptol and SAW, Fiat-Crypto, HACL*, Vale and EverCrypt, Aeneas, Kani, CryptoLine, Verus.

Sources

CBMC repository

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