CBMC model checker
Model checker in Developer tools
Free model checker that people use to formally verify C code; it is very capable but scales worse, suiting smaller modules rather than complete systems.
5 people recommended CBMC model checker in Hacker News comments, 1 had mixed feelings and 1 criticized it, November 2025 to October 2026.
Summary written by Claude from 11 comments.
7 people gave an opinion
- recommend it
- 5
- mixed feelings
- 1
- warn against or regret it
- 1
The record
Recommended in 5 of 12 months
In 6 different threads.
- November 2025: recommended
- December 2025: recommended
- January 2026: not recommended
- February 2026: not recommended
- March 2026: not recommended
- April 2026: recommended
- May 2026: not recommended
- June 2026: not recommended
- July 2026: recommended
- August 2026: not recommended
- September 2026: recommended
- October 2026: not recommended
Why it doesn’t carry the badge
- 5 people recommend itNeeds 10 or more, not met.
- 5 recommenders for every criticNeeds 2 to 1 or better, met.
- Recommended in 5 of 12 monthsNeeds 4 or more, met.
- Recommended in 6 threadsNeeds 5 or more, met.
- The biggest thread supplies 40% of its recommendersNeeds half or less, met.
The same rules apply to every product, and the badge can’t be bought. Mixed feelings count toward neither side. How the badge works
What people say about it
Reasons grouped from a sample of 11 of the 11 opinions about it, picked in proportion to how many people recommend it, have mixed feelings and criticize it. Each mark is one comment in the sample. Open a reason to read what they said.
Why people recommend it
Each mark is one comment
Verifies C code effectively
“99% of code that I've written can be verified via the CBMC / CProver model checker”
Comment from 13 Dec 2025 in “The Coming Need for Formal Specification” “I use C and C++ model checkers, like cbmc and its variants (esbmc) successfully”
Comment from 17 Dec 2025 in “Dafny: Verification-Aware Programming Language” “I have found huge value in CBMC and KLEE for statically verifying C code”
Comment from 27 Nov 2025 in “Coq: The World's Best Macro Assembler? (2013) [pdf]” - Comment from 25 Jul 2026 in “Memory Safety Absolutists”
What people said
All 11 opinions about it, newest first. Each links to the original comment.
“I also tried converting CBMC's intermediate representation, "GOTO Programs" to Lean”
“For full formal proofs it's easier to use cbmc or esbmc though”
“I have had great success model checking C with CBMC.”
“Usually bounded, usually assertion-style, no type-level integration.”
“between cbmc, frama-c and coccinelle there is hardly another language with comparable tooling”
“I use C and C++ model checkers, like cbmc and its variants (esbmc) successfully”
“99% of code that I've written can be verified via the CBMC / CProver model checker”
“CBMC scales worse (best for smaller modules, not complete systems), but is also very capable.”
“These sound like astounding systems.”
“The modeling language is also just C, which simplifies things HUGELY.”
“I have found huge value in CBMC and KLEE for statically verifying C code”
Counts come from 1,791,911 Hacker News comments labeled by Claude, November 2025 to October 2026, with data through October 31, 2026. Counts updated 2 Nov 2026. How we count. Report a mistake.