Beyond Vibe Coding: Formal Verification for AI-Generated Software

AI coding agents can now write substantial amounts of open-source software—but generated code still needs more than a plausible implementation and a passing test suite. How can we gain stronger confidence that AI-written code is actually correct?
In this session, Carl will demonstrate a workflow in which AI not only writes code, but also creates a formal specification and produces a machine-checked proof of correctness.
Carl is applying this approach to RangeSetBlaze, an open-source Rust library, using Lean, a theorem prover and programming language for formal verification, to state and prove key correctness properties. The result is a development workflow that goes beyond conventional testing: instead of checking a collection of examples, formal verification can establish that specified properties hold across all relevant inputs.
The broader idea is language-independent. As AI becomes increasingly capable of generating both software and proofs, formal verification may become practical for a much wider range of everyday software development. AI can take on much of the traditionally difficult and time-consuming proof engineering while developers focus on defining the right specifications and reviewing the resulting guarantees.
The session will explore:

• How an AI-assisted code → specification → proof workflow works in practice
• How Lean can be used to verify properties of real-world Rust software
• What machine-checked proofs provide beyond unit and integration tests
• Where AI-assisted formal verification works well—and where it still breaks down
• How formal proofs, testing, and code review can complement one another
• What this approach could mean for software engineering as AI takes on more of the coding

Rather than asking only, “Can AI write the code?”, this talk explores a more demanding question:
“Can AI help us prove that the code it writes is correct?”

### About the Speaker

Carl is a longtime member of the PyData community and a retired Principal Applied Scientist at Microsoft and Microsoft Research. He has presented five talks at PyData conferences and delivered a keynote at a PyData Seattle open-source software meetup in 2024.