FVSpec: Real-World Property-Based Tests as Lean Challenges
Summary
This paper presents FVSpec, a benchmark for AI-assisted formal verification that translates real-world property-based tests from Python into Lean 4 specifications using a multi-agent LLM pipeline, aiming to drive progress on formal verification of real-world software.
View Cached Full Text
Cached at: 06/15/26, 04:59 PM
Paper page - FVSpec: Real-World Property-Based Tests as Lean Challenges
Source: https://huggingface.co/papers/2606.01008
Abstract
A benchmark for AI-assisted formal verification is presented, involving the translation of property-based tests from Python into Lean specifications using a multi-agent LLM pipeline.
We present a benchmark for evaluating AI models and agents on real-world formal software verification tasks. We first scrape 11,039property-based tests(PBTs) from real-world Python repositories, then automatically translate 2,772 of them (25%) into 9,415Lean 4specifications 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 ofdependently-typed programmingin a seldom-used language. We describe a three-agentLLM pipelinefor transpiling PBTs into Lean specifications, evaluate coverage and quality metrics, and provide baselines forproof generationusing 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-assistedformal verificationof real-world software, which is of increasing interest as AI produces more and more of the world’s code.
View arXiv pageView PDFProject pageAdd to collection
Get this paper in your agent:
hf papers read 2606\.01008
Don’t have the latest CLI?curl \-LsSf https://hf\.co/cli/install\.sh \| bash
Models citing this paper0
No model linking this paper
Cite arxiv.org/abs/2606.01008 in a model README.md to link it from this page.
Datasets citing this paper2
#### GaloisInc/fvspec-pbt Viewer• Updatedabout 1 hour ago • 21.7k • 59 #### GaloisInc/fvspec-fv Viewer• Updatedabout 1 hour ago • 9.42k • 55
Spaces citing this paper0
No Space linking this paper
Cite arxiv.org/abs/2606.01008 in a Space README.md to link it from this page.
Collections including this paper0
No Collection including this paper
Add this paper to acollectionto link it from this page.
Similar Articles
What your agent's green test suite actually proves
This article argues that standard test suites with fixed inputs and expected outputs are insufficient for AI agents due to infinite input spaces and non-deterministic behavior, advocating for property-based testing instead.
Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory
Introduces Lean4Agent, a framework using Lean4 for formal modeling and verification of agent workflows and trajectories, demonstrating improved performance on SWE-Bench and ELAIP-Bench.
Safety Testing LLM Agents at Scale: From Risk Discovery to Evidence-Grounded Verification
This paper presents Vera, an end-to-end automated safety testing framework for LLM agents that combines literature-driven risk discovery, combinatorial composition of safety cases, and evidence-grounded verification. Evaluations on four agent frameworks reveal substantial safety weaknesses, with average attack success rates reaching 93.9% under multi-channel attacks, and the release of Vera-Bench with 1600 executable safety cases.
VFEAgent: A Multimodal Agent Framework for End-to-End Automated Finite Element Analysis
This paper proposes VFEAgent, a multi-agent system that automates finite element analysis by integrating vision-language models with a verification-first code synthesis framework, enabling end-to-end simulation from images and problem descriptions.
Microsoft ASSERT: Test AI Agents with Plain Text Specs
Microsoft released ASSERT at Build 2026, an open-source framework that converts natural language behavior specifications into executable evaluations for AI agents.