`lf-lean`: The frontier of verified software engineering
Summary
lf-lean introduces a verified translation of 1,276 statements from the Logical Foundations textbook (Rocq) to Lean, produced with frontier AI and minimal human effort. It uses task-level specification generators (rocq-dove) to automate verification across codebases, achieving 97% automated translations and a 350× reduction in verification effort (about 15 hours of human work for the extreme cases). The work argues that verified software engineering can scale by composing verified components and treating dependencies as interfaces, situating results within METR’s time horizon framework and detailing methodology, dependencies, and appendix data.