Papers for

formal methods practitioners

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Framework improves checking and trust in automated Lean proofs

FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification

Abstract: Coding agents increasingly automate Lean proof development, but successful compilation alone does not establish that a candidate proves the intended statement under acceptable assumptions. We present FORALL-LEAN-AGENT, a frontend-agnostic framework for auditable reasoning in formal mathematics and software verification. The framework combines isolated workspaces, Lean tools, and fresh review with statement comparison, axiom audits, and independent proof checking where supported. Verification evidence and reviewer decisions are bound to the same candidate artifact, making acceptance traceable. We evaluate the framework on VeriSoftBench, PutnamBench, and both problems in the Lean Eval softwareverification track. On the 100-task VeriSoftBench subset, integration with FORALLLEAN-AGENT raises benchmark-rule success from 93 to 100 for GPT-5.6 Sol at low effort while reducing cost from $69 to $62. The PutnamBench evaluation accepts all 672 problems at an average of $4.72 each. These results show that agent harness design can improve correctness and efficiency while providing evidence beyond aggregate solve counts.

Thu 1 OctSoftware EngineeringArtificial IntelligenceLogic in Computer Science
The gist
Automated computer programs can help write complicated math and software proofs using a system called Lean, but just finishing a proof doesn't guarantee it's actually correct. The authors created a new system called FORALL-LEAN-AGENT that helps check these proofs more carefully and makes it easy to audit the reasoning behind them. Their system uses separate work areas, special tools, and independent checks to make sure proofs follow the rules and assumptions properly. They tested it on several challenging sets of problems and found that it improved success rates and lowered costs when using AI agents to generate the proofs.
Open → 2610.00885v1