Post

LLMs write code fast, but how do you trust it? Unit tests only cover paths you think to test. Bounded model checking exhaustively explores all paths and gives mathematical proofs when it finds bugs. 🧵

Paulo Matos

@ocmatos.com

I built a Claude Code plugin for ESBMC (esbmc.github.io) — bringing formal verification into your agentic coding workflow. Ask Claude to check your code, ESBMC runs under the hood, and you get concrete counterexample traces when it finds bugs.

13/2/26, 8:42 pm0 reposts2 likes

Paulo Matos

@ocmatos.com

13 Feb

Now merged upstream! Supports C, C++, Python, Solidity & CUDA. Thanks to the ESBMC team for the quick merge 🙏 Full write-up & demo: p.ocmatos.com/blog/formal-...

p.ocmatos.comFormal Verification in Your Terminal: ESBMC meets Claude Code - Notes & CodeA new Claude Code plugin brings ESBMC bounded model checking directly into your AI-assisted development workflow.