CBMC: Bounded model checker for C, used on mlkem-native and s2n
===============================================================

CBMC 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
Category: Verified implementations
Targets: C, mlkem-native, s2n
Approach: Bounded model checking for memory safety and assertions
Access: Open source (BSD-4)
Status: Active, mature
Strengths: Mature and widely deployed. | Concrete counterexamples. | No spec needed for memory safety.
Limits: Bounded. | No functional correctness. | Modelling effort for harnesses.
Firms using it: none listed
Sources: https://github.com/diffblue/cbmc

Source page: https://sorryfree.com/frameworks/cbmc/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13