What's this about?
AI agents are increasingly used for programming but offer no guarantee that the code they produce is correct. Vero investigates verified code generation: can an agent produce both an implementation *and* a machine-checked proof that it satisfies its specification?
What exactly is "formal verification"?
Testing shows that code works on the cases you tried. Formal verification proves mathematically that it works on all possible inputs, by expressing the intended behavior as a specification and having a proof checker confirm the implementation satisfies it. It's the highest assurance available in software and is used where failure is catastrophic — aerospace, cryptography, chip design. It's also extremely labor-intensive, which is why it stays rare, and why automating it is attractive.
Why is this worth noticing?
- It attacks the central objection to agent-written code — that you can't trust it — with the one technique that produces certainty rather than confidence.
- Proof checking is automatically verifiable, which makes it an unusually clean training signal: the agent can't talk its way to a passing grade, so this domain is largely immune to the specification-gaming the Economist piece describes.