We present a benchmark for evaluating AI models and agents on real-world formal software verification tasks. We first scrape 11,039 property-based tests (PBTs) from real-world Python repositories, then automatically translate 2,772 of them (25%) into 9,415 Lean 4 specifications with sorry placeholders (about 3 formalizations/PBT; we retain multiple attempts when none dominates on quality metrics). Translating PBTs into Lean specifications is challenging: it requires modeling Python semantics in Lean, inferring the logical property encoded in an imperative PBT, and handling the inherent difficulties of dependently-typed programming in a seldom-used language. We describe a three-agent LLM pipeline for transpiling PBTs into Lean specifications, evaluate coverage and quality metrics, and provide baselines for proof generation using several automated and model based approaches. All code (scraper and agents) and data (PBTs and Lean specifications) are open source. Our benchmark aims to drive progress on the underexplored problem of AI-assisted formal verification of real-world software, which is of increasing interest as AI produces more and more of the world's code.
Alex: Welcome to another episode of ResearchPod. Today, we're looking at a paper that tackles a real tension in software development — the gap between writing code and making it genuinely safe. Sam, what's the core problem?
Sam: So the challenge is this: there's a technique called formal verification, where instead of just testing whether your code works on a few examples, you use mathematics to *prove* it will always work correctly. Think of it like the difference between checking that a bridge holds up a few trucks versus mathematically proving it can hold any load within its design limits. It's the gold standard for safety-critical software. The problem is, almost nobody uses it — because writing those proofs requires a rare kind of expert, and there simply aren't enough of them.
Alex: So this paper asks whether AI can step in and fill that gap?
Sam: That's the central question. And the clever angle they take is to look at something developers are *already* doing — a practice called property-based testing. Rather than checking one specific example, a developer writes a general rule — something like "no matter what list you give this function, the output should always be sorted" — and then the computer fires random inputs at it to try to break that rule. It's a lightweight safety net that's already baked into how real software gets written.
Alex: Right, a quick sanity check rather than a full audit. But how do you go from that kind of informal rule to a rigorous mathematical proof?
Sam: That's where the paper's main contribution comes in. They build a system with three AI agents working together to translate those testing rules — written in Python, the everyday language most developers use — into Lean 4, which is a language specifically designed for writing mathematical proofs. The process of converting code from one language to another like this is called transpilation.
Alex: So the AI is acting as a translator, taking a casual developer rule and rewriting it in the strict, logical language that a theorem prover can actually work with?
Sam: Exactly. And translation is hard, so they don't just do it once and hope for the best. They build in a feedback loop. There's a tool called the Lean Language Server Protocol — think of it as a very strict teacher marking an essay. The AI writes a draft proof, the tool flags every logical error, and the AI revises. That cycle repeats until the proof either passes or the system gives up on that particular example.
Alex: And where does the raw material come from? What are they actually translating?
Sam: They scraped more than eleven thousand existing property-based tests from real open-source Python projects. That's the dataset they call FVSpec. What makes it meaningful is the contrast with most AI benchmarks, which tend to use clean, self-contained maths problems — olympiad puzzles and that sort of thing. Real software is messier. It talks to databases, calls external services, handles unexpected inputs. This dataset forces the AI to grapple with that kind of complexity.
Alex: That raises an obvious question though. If the translation isn't perfect — if something gets lost going from Python to Lean — how do you know the proof actually reflects what the developer intended?
Sam: That's a fair concern, and the paper is honest about it. Their goal isn't to produce a perfect one-to-one translation of every test. What they're after is a large, realistic collection of proof challenges that are, as they put it, "equivalently interesting" for an AI to work on. Even an imperfect translation still requires the AI to reason carefully about logic, types, and edge cases — skills that clean maths benchmarks don't really test.
Alex: What about code that connects to external systems? A function that reads from a database can't really be proven in isolation, can it?
Sam: Right, and the way they handle that is by treating those external systems as what are called uninterpreted axioms — essentially placeholders. You're saying "assume this database call does *something*, we don't need to model the whole database to reason about the logic around it." It's a practical compromise that lets the proof work without requiring a complete model of the outside world.
Alex: So there are genuine limits here. This isn't a system that can prove everything about any piece of software.
Sam: Not at all, and the paper doesn't claim otherwise. The translation process is lossy by design, some tests produce proofs that are too trivial or too broken to be useful, and they have to filter those out. What they're building is a training environment — a way to expose AI models to the *kind* of reasoning that formal verification demands, using problems drawn from the real world rather than textbooks.
Alex: So the long-term vision is AI that can verify the code it writes, without needing a human expert to sign off on every proof?
Sam: That's the direction. Right now, formal verification is a bottleneck because it requires scarce human expertise. If AI models can learn to handle it — even imperfectly at first — that changes the economics of software safety. Instead of verification being reserved for aerospace or medical devices, it could become something that ordinary software benefits from too. The insight is that the raw material was already there, sitting in millions of developer tests. This paper is an attempt to put it to work.
Alex: It's a practical approach to a difficult problem — using the safety culture that already exists in software development as the foundation for something more rigorous. Thanks for walking us through it, Sam.
Sam: Thanks for having me.
Alex: And thanks for listening to ResearchPod.