FVSpec is a benchmark for evaluating AI models and agents on real-world formal software verification. It extends FVAPPS with real-world property-based tests scraped from open-source Python repositories and translated into Lean 4 specifications. The work is conducted at Galois, Inc. and funded by the Advanced Research + Invention Agency (ARIA).
Acknowledgments
Beyond the core authorship, FVSpec would not have been possible without the contributions of many people and teams.
- Evan Boehs and Jake Ginesin for their work on the property-based test scraper.
- Juan Castaño for setting up the database and AWS infrastructure used for scraping.
- Benchify for their collaboration.
- The Galois program-management, IT, and contracting staff whose support made this work possible.
Additional acknowledgments for the broader property-based test dataset — including the Dartmouth DALI Lab for extending the scraper to support TypeScript PBTs — are listed with the PBT dataset.