Coding agents are getting alarmingly good at finding security exploits. But they're also making one of the strongest tools for preventing entire classes of bugs accessible to almost anyone: formal verification.
Historically, very few developers used formal verification because the cost and expertise required were simply too high. You needed to understand the math, different verification languages, their tradeoffs, and how to use and maintain them.
Vaibhav (VB) Srivastav@reach_vbpast ~48 hours in security:
> PHP: unauthenticated remote code execution
> GitLab: CVSS 10.0 remote code execution
> Node.js: Brotli decoder RCE
…But coding agents are changing that.
The create-formal-verification-skill by Poteto, aka Lauren Tan, is really impressive. It can:
- Find high-value properties in your codebase worth proving.
- Choose the appropriate verification tool.
- Set up verification and check that it's proving the intended property.
- Generate a reusable skill so future coding agents can maintain the verification.
All without you having to become an expert in formal verification.
Lauren Tan (Poteto)@potetopstack v0.15.27 ships with a new skill /create-formal-verification-skill!
it's still in beta, and similar to /create-verification-skill, this is a meta-skill that creates a new skill…
However, there's an important catch. With tools like TLA+ and Quint, you're often not proving your actual executable code. You're proving a simplified model of it. And when coding agents keep modifying your implementation, that model can drift out of sync. Your proof might still pass, but you're no longer proving the behavior of the code you're shipping.
There are some really interesting approaches to closing this gap:
- Victor Taelin's Bend2 lets your agent write executable code and proofs in the same language. It's built with coding agents in mind. The code you're proving is the code you're running, eliminating the separate-model problem.
- For state-machine-heavy applications, a more experimental approach is to make states and transitions explicit in the actual application code, then verify temporal logic properties directly against that same executable representation. No separate model to maintain. The challenge is making sure the checker itself is trustworthy.
And we're already seeing formal verification being applied in increasingly ambitious ways:
- Anthropic used Claude to prove no-crash properties for 239 entry points across 123 open-source libraries, working at the compiled RISC-V code level.
Anthropic@AnthropicAINew on our Frontier Red Team blog: using Claude to formally verify software at large scale.
- Satnam Singh's team at Harmonic just launched Aristotle for formal verification of C software and Verilog hardware designs, with proofs that can be checked on every commit.
Satnam Singh@satnam6502Prove memory safety about your C programs.
Prove a C model is equivalent to its SystemVerilog implementation.
Harmonic@HarmonicMathWe’re bringing Aristotle to code.
AI is writing more code than anyone can review. We're building the AI that verifies it.- And with Poteto's skill, individual developers can now start applying formal verification to their own projects without years of specialist expertise.
Formal verification is becoming part of the regular coding-agent feedback loop. And this could fundamentally change how we build reliable software with coding agents.
Brandon Kase and I explored all of this in our latest Superlinear episode.
If you're thinking of adding formal verification to your coding-agent workflow, it's worth understanding the tradeoffs before you start trusting the proofs that pass the check.
Episode timestamps
- 00:00Coding agents changed formal verification
- 02:04Tests vs. formal verification
- 06:36Poteto's formal verification skill
- 08:16The catch: verified models drift from your code
- 12:17General purpose languages like Bend2
- 14:28TLA+ and Quint for state-machines
- 16:27Build verification into the application
- 20:38Statecharts and experimental TypeScript checker
- 27:27Closing thoughts and Superlinear Discord