Lf-lean: The frontier of verified software engineering

We present lf-lean

, a verified translation of all 1,276 statements of the Logical Foundations textbook from Rocq to Lean, produced by frontier AI with ~2 person-days of human effort versus an estimated ~2.75 person-years manually (a 350x speed-up). We achieve this through task-level specification generators: because many software transformations are semantics-preserving, correctness can be defined once for an entire task class and checked automatically across all instances and codebases. This scales human oversight from 𝒪(𝓃) to 𝒪(1) regardless of program complexity. Placed on METR's time horizon graph, our result suggests verified software engineering is advancing faster than expected.

Introduction

As AIs automate increasingly complex software tasks, a fundamental tension emerges: how do we know the code they produce is correct? The standard approach of reviewing AI-generated code and its tests doesn’t scale. Human review effort grows proportionally with code volume, while AI code generation capacity grows exponentially.1 If this trend continues, we’re headed toward a world where code deployment is bottlenecked on human review capacity, or just deployed without review.

This post introduces a different approach: task-level specification generators. Instead of reviewing each piece of generated code individually, we review a correctness specification once for an entire class of tasks, and the correctness specification covers all instances of the task across any codebase. The key insight is that for many important software transformations (translation, optimization, refactoring), we can define what “correct” means generically, without reference to any specific codebase. Moreover, as codebase complexity increases, a lot of feature implementation is a semantics-preserving transformation of existing features, so the correctness specification for the new feature is a simple corollary of the correctness specification for the existing features. Thus, building task-level specification generators helps scale oversight in two ways: (1) you can easily work on many more codebases simultaneously, and (2) what works on simple codebases extends to arbitrarily complex ones.

We prototype task-level specification generation with rocq-dove

, building a scalable environment for verified translation2 from Rocq3 to Lean. Given any Rocq source code, rocq-dove

automatically generates a correctness specification (a theorem that any valid translation must satisfy) and grades model-generated translations and proofs against it. Because the specification is derived from the source code itself, rocq-dove

scales to arbitrary codebases without additional human effort.

We use rocq-dove

to generate an environment for a verified translation of all 1,276 statements4 in Logical Foundations5 1Software Foundations, Volume 1: Logical Foundationssoftwarefoundations.cis.upenn.edu, 2024 . Using our scaffold, frontier AI models6 autonomously produced verified translations of 97% of the statements.7 We solved 6 extreme-difficulty statements manually (~2 person-days), after which models completed the remaining 2.5%. For context, we estimate the full task would have taken 3 person-months for translation plus 2.5 person-years for verification if done entirely by humans.8

Two key world-view updates:

Verified software engineering can scale without marginal human oversight.rocq-dove

automatically generated correctness specifications for the 1,276 translations inlf-lean

. No human judgment was needed to define “correct” for each case. Combined with rich feedback from the proof assistant, this creates a dense reward signal that lets AI iterate toward correct solutions autonomously. - **AI capabilities on software verification are advancing faster than expected.**We developedlf-lean

, the first sufficiently complex evaluation to demonstrate this. Compared to METR’s time horizon trend 2Measuring AI Ability to Complete Long TasksMETR Blog, 2025 on unverified software engineering, verified software engineering appears to be catching up.

The implication is that software verification, long considered too expensive for practical software development, may become the more scalable approach in an era of AI-assisted programming. When humans can’t review all the code AI produces, having machines verify correctness automatically becomes not just nice to have, but necessary.

In what follows, we explain task-level specification generators, the conceptual framework that lets correctness checking scale without marginal human effort. We then describe rocq-dove

, our prototype environment for verified translation from Rocq to Lean, and how we applied it to produce lf-lean

. We present details of how we achieved a 350× speedup over manual verification, and make the case for scaling verified software engineering.

Task-Level Specification Generators

The scaling problem with AI coding is that humans can only review so much. As models generate more code more quickly, human oversight becomes the bottleneck.

One response is to make review faster—better tooling, smarter sampling, and more efficient workflows. This can mitigate the immediate issue, but doesn’t change the fundamental scaling problem: a human must understand each codebase and write codebase-specific verification. Oversight effort remains linear: (\mathcal{O}(n)) where (n) is the number of tasks. This is akin to writing a formal specification for every codebase.

The other response is to make review amortizable. For certain task classes (\mathcal{T}) (e.g., translation, optimization, parallelization, refactoring), correctness can be defined generically, without reference to individual task details. A human reviews the specification generator for (\mathcal{T}) once; the system then automatically verifies any task instance. Human effort becomes (\mathcal{O}(1)) with respect to codebase count. Task-level specification involves defining a specification generator, which is a function that takes a particular instance of a task, or a description thereof, and outputs a specification for that specific instance.

When building a new toolchain, the ideal problem is useful, simple, and representative. We started with translation, which hits all three; there is real demand for porting codebases between languages 3It's COBOL all the way downIncrement, 2018 , it is the simplest semantics-preserving transformation, and it is paradigmatic for the generalized challenge of software verification—establishing semantic equivalence. Semantic equivalence often looks the same regardless of the exact specification or implementation, and verified translation captures this core difficulty, making it an effective task for training on software verification.

rocq-dove

: A Task-Level Specification Generator for Translating from Rocq to Lean

We developed a prototype task-level specification generator for the task of verified software translation from Rocq to Lean. Unlike an unverified software translation which yields only a translated version of the code, a verified translation produces a (translation, proof)

pair. The proof

then serves as a guarantee that the translation

is semantically equivalent to the source

. Even if the translation

is correct, the pair is rejected if the proof

does not verify its correctness. In this section, we describe the environment setup used for every codebase and the details of how we build typewise isomorphism.

Environment

We describe the general environment for verified translation from Rocq to Lean.

Specification Generation:rocq-dove

derives a theorem statement (\texttt{Thm}{ exttt{Rocq}}) directly from the Rocq source (\texttt{Src}{ exttt{Rocq}}). The theorem states that the translation istypewise isomorphicto the source; we describe nuances of the definition in the Typewise Isomorphism section.9 - Translation: The AI agent translates (