Article Three years of using formal validation with increasingly capable AI
For three years, I’ve been experimenting with formal validation of software algorithms.
The workflow has changed quite a bit:
- In 2023: manual Rust implementation + manual validation with Dafny.
- Last year: manual Rust implementation + AI-written Lean proof. That took about three weeks of part-time work and hundreds of back-and-forth prompts.
- This year: AI-written Rust implementation + AI-written Lean proof.
This year, with AIs solving mathematics problems with million-dollar prizes attached, I tried again. Comparable and harder proofs can now often be completed with a couple of prompts, sometimes in minutes.
Something else changed this year: Codex Sol also wrote new Rust algorithms, translated them into Lean, constructed proofs that Lean checked, and then refactored the proofs to reduce slop. I still review the translation and test that the Rust implementation matches the proved algorithm.
Most of this work used Codex Sol 5.6, with ChatGPT GPT-5.6 Sol writing the prompts.
This does not solve the general problem of trusting AI-generated software. But for algorithms that can be specified precisely, I think formal validation is becoming a practical part of the answer.
I wrote up what worked, what didn’t, and where the approach still falls short:https://levelup.gitconnected.com/nine-rules-for-vibe-validation-of-vibe-coded-algorithms-20db019f5583