cs.SEOct 1, 2026
SaveFORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification
Organizations: Astrio Labs
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 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.
Figures & tables
| System | Model | Effort | Target protocol | Rules | Strict | Indep. | Input tokens (cached, M) | Output tokens (M) | Cost |
| Aleph Prover ‡ | – | – | Unknown | 94 | – | – | – | – | – |
| Aristotle ‡ | – | – | Unknown | 69 | – | – | – | – | – |
| VeriSoftBench ‡ | Gemini-3-Pro | – | Pass@8, | 65 | – | – | – | – | – |
| Claude Code | Opus 5 | xhigh | Pass@8, | 100 | 89 | – | 53.8 (50.1) | 2.09 | $135 |
| Forall-Lean-Agent | Opus 5 | xhigh | Pass@8, | 100 | 96 | 69/69 | 45.3 (44.0) | 1.58 | $111 |
| Claude Code | Opus 5 | low | Pass@8, | 99 | 87 | 62/69 | 62.9 (58.7) | 1.18 | $101 |
Table 1: Results on the 100-task VeriSoftBench-Aristotle subset. Rules denotes benchmark-rule success, Strict excludes disallowed kernel axioms, and Indep. reports independent-checker acceptances over judged candidates. § Numina-Lean-Agent runs its released protocol, one sample with up to ten rounds, rather than the target protocol used for the other systems, so its total is not a like-for-like comparison. Target protocols are requested settings. Recorded budgets differ. Token counts are in millions. Input totals include cached tokens, shown in parentheses. Output includes reasoning tokens where reported. Dashes indicate unreported values. ‡ Published baselines [ 28 , 27 ] . Appendix A documents validation coverage.
Figure 2: Repository proof success under alternative execution protocols and the distribution of review rounds.
| Problem | Holes | Submission | Model | Verification |
| coc_strong_normalization | 6 thm | 233 files / 28.6k lines | GPT-6 Astra | Benchmark validated |
| rcf_quantifier_elimination | 1 def + 3 thm | 1 file / 1.5k lines | GPT-6 Astra | Benchmark validated |
Table 2: Lean Eval software-verification developments completed with Forall-Lean-Agent and GPT-6 Astra. The submissions pass native compilation, fresh review, comparator validation, and independent-kernel checks.
| System | Reported resources | Solved | Evaluation setting |
| Aleph Prover [ 18 ] | avg 1,468 | 672 | closed system |
| NEAR AI, DeepSeek V4 a | mean $0.17 | 672 | shell agent with retries |
| Humanfia b | avg $44.5 | 672 | GPT-5.6 Sol at xhigh effort |
| Goedel-Architect [ 9 ] | 8 blueprints, 4 retries per node, avg $5.8 | 642 | |
| Seed-Prover 1.5 [ 8 ] | 10 H20-days | 581 | |
| Hilbert [ 26 ] | avg Pass@1840 | 462 | evaluated on 660 problems |
Table 3: Comparison on the Lean answer-given version of PutnamBench. Leaderboard totals [ 20 ] use different benchmark versions, models, budgets, and statement revisions. Reported resource statistics for Forall-Lean-Agent cover all 672 accepted problems.
Figure 3: Resource use across all 672 accepted PutnamBench problems. 662 receive approval in the first review round and 651 require no continuation request. Median wall time is 27 minutes and the maximum is 211 minutes.
| Threat | Evidence | Control |
| Permission bypass allowed access to the reference repository | reference similarity of 0.99 to 1.00 and transcript path evidence | operating-system restrictions across the process tree |
| Unrestricted network access exposed public reference material | reference similarity of 1.00 and recorded curl access | provider-only network proxy with refusal logs |
| Filesystem search located alternative benchmark copies | reference similarity of 1.00 and recorded search paths | pattern-based restrictions covering alternative checkouts |
| Stored and submitted proofs differed in 5 of 97 cases | serial verification of recovered submit-time artifacts | candidate digests and single-use sample directories |
| Scorer dependencies were unavailable for five valid samples | independent rescoring of an all-negative task | pinned interpreter and toolchain with environment checks |
| Authentication errors generated 229 false failure records | error returns with zero inference expenditure | interruption status and resumable tasks |
Table 4: Observed threats to evaluation validity and the corresponding controls. Access violations can inflate success counts, while artifact drift, scorer failures, and service interruptions can produce incorrect negative outcomes.
Appendix figures & tables2 assets
Supplementary material from the paper’s appendix.
Appendix
| System and configuration | clean | VCV | FR | Ark | loom | juvix | veil | Leroy | Expr | iris | pcf | Total |
| Tasks | 47 | 17 | 7 | 5 | 5 | 5 | 5 | 4 | 3 | 1 | 1 | 100 |
| Claude Code Fable 5 low, unaided | 43 | 17 | 7 | 5 | 5 | 5 | 5 | 4 | 3 | 1 | 1 | 96 |
| Claude Code Opus 5 low, unaided | 46 | 17 | 7 | 5 | 5 | 5 | 5 | 4 | 3 | 1 | 1 | 99 |
| Forall-Lean-Agent + Claude Code Fable 5 low | 47 | 17 | 7 | 5 | 5 | 5 | 5 | 4 | 3 | 1 | 1 | 100 |
| Forall-Lean-Agent + Claude Code Opus 5 low | 47 | 17 | 7 | 5 | 5 | 5 | 5 | 4 | 3 | 1 | 1 | 100 |
| Forall-Lean-Agent + Codex Sol low | 47 | 17 | 7 | 5 | 5 | 5 | 5 | 4 | 3 | 1 | 1 | 100 |
Table 5: Repository-level results. Codex Sol low includes the final acceptance on clean . Codex Sol xhigh shows the initial 97-task total before fresh retries, with its cumulative result in Table 1 . VCV denotes VCV-io, FR denotes lean-formal-reasoning-program, Ark denotes ArkLib, juvix denotes juvix-lean, Leroy denotes the compiler course, Expr denotes LeanExprEvaluator, iris denotes iris-lean, and pcf denotes pcf-lean.
| Year | 62 | 63 | 64 | 65 | 66 | 67 | 68 | 69 | 70 | 71 | 72 | 73 | 74 | 75 | 76 | 77 |
| In benchmark | 11 | 9 | 12 | 12 | 12 | 12 | 11 | 11 | 10 | 10 | 11 | 9 | 10 | 11 | 9 | 10 |
| Accepted | 11 | 9 | 12 | 12 | 12 | 12 | 11 | 11 | 10 | 10 | 11 | 9 | 10 | 11 | 9 | 10 |
| Year | 78 | 79 | 80 | 81 | 82 | 83 | 84 | 85 | 86 | 87 | 88 | 89 | 90 | 91 | 92 | 93 |
| In benchmark | 11 | 10 | 10 | 8 | 9 | 9 | 8 | 10 | 12 | 11 | 12 | 9 | 10 | 10 | 11 | 11 |
| Accepted | 11 | 10 | 10 | 8 | 9 | 9 | 8 | 10 | 12 | 11 | 12 | 9 | 10 | 10 | 11 | 11 |
| Year | 94 | 95 | 96 | 97 | 98 | 99 | 00 | 01 | 02 | 03 | 04 | 05 | 06 | 07 | 08 | 09 |
Table 6: Year-ordered PutnamBench coverage. The evaluation records and accepts all 672 problems.