Articles
Insights on formal verification, code assurance, and the work of building software you can actually prove correct.
Proving the Foundation, Checking Every Change
Anthropic and Theorem just showed AI can produce machine-checked proofs about real software at scale. Their conclusion - that verification is moving from bolted-on to built-in - is one we share. Here is the layer we've been building: checking that every change, including every AI-written patch, keeps the behavior it should.
Everyone Says 'Verified.' Ask What You Get.
The word 'verification' now covers everything from a review bot's opinion to a machine-checked proof. Ask what artifact you get, what fraction of inputs it covers, and why anyone you show it to should believe it.
Why Formal Methods Matter: The Calendar Problem
A leap-year bug that hides at the century boundary: why testing samples the haystack and formal verification finds the needle.
Trust but Verify: Using a Neurosymbolic Model in Code Optimization
We let an LLM optimize a well-known code library, then made it prove every change. Here is what survived, what got caught, and where high confidence stops being a proof.
What Is FMToolkit?
FMToolkit answers one question: do these two functions behave identically? What it does, what it does not, and where it fits.
What Is Formal Verification and Why Does AI-Generated Code Need It?
AI writes code faster than ever. Speed doesn't equal correctness. Here's how formal verification closes that gap.