Formal Verification RSI AI Agent

Personal website: Sahibzada Allahyar

<div align="center"> <img src="docs/assets/hero.gif" alt="Millennium Harness: a trefoil of proof steps turning blue as each one is kernel-checked, while fake proofs flash red and are rejected" width="100%"> <br>

Formal verification you can trust, and recursive self-improvement that can't cheat.

_{Formal verification · Lean 4 · Dafny · automated theorem proving · autoformalization · verified software engineering · AI for mathematics and physics · recursive self-improvement (RSI) · reward hacking · AI safety}

<p> <a href="#results"><img src="https://img.shields.io/badge/fake_proofs_accepted-0%2F96-6B95F0?style=flat-square&labelColor=101314" alt="0 of 96 cheats accepted"></a> <a href="https://lean-lang.org"><img src="https://img.shields.io/badge/Lean-4.23-E8E4D8?style=flat-square&labelColor=101314" alt="Lean 4.23"></a> <a href="https://dafny.org"><img src="https://img.shields.io/badge/Dafny-4.11-E8E4D8?style=flat-square&labelColor=101314" alt="Dafny 4.11"></a> <img src="https://img.shields.io/badge/python-3.10+-E8E4D8?style=flat-square&labelColor=101314" alt="Python 3.10+"> <img src="https://img.shields.io/badge/license-MIT-E8E4D8?style=flat-square&labelColor=101314" alt="MIT license"> </p>

<a href="#why">Why</a> · <a href="#results">Results</a> · <a href="#millennium-rsi">Millennium RSI</a> · <a href="#quickstart">Quickstart</a> · <a href="#how-it-works">How it works</a>

</div>

---

Why

AI now writes machine-checked mathematics and formally verified code. The value of a formal proof is that nobody has to read it: the checker vouches for it. But the check most benchmarks and agent harnesses actually apply is weaker, and agents learn to game it:

• Lean accepts sorry with only a warning.
• Dafny reports 0 errors for assume {:axiom} false.
• A solution can leave the specification's text untouched and still change what it means.

$ cat Solution.lean        # the theorem text is byte-identical to the task's...
instance (priority := high) cheatLE : LE Nat := ⟨fun _ _ => True⟩

$ lean Solution.lean       # ...and Lean is happy
$ python -m millennium_harness.lean check Solution.lean frozen.json
⟦Millennium Harness⟧ ✗ SPEC_TAMPERED · Lean 4.23.0-rc2 · round 1/2
- the statement/type of `last_chair_value` elaborates differently from the task's
  (same text, different meaning: a shadowing instance, open, variable or notation?)

Millennium Harness is a model-free gate: a solution counts only if the frozen specification kept its meaning and was proved with no escape hatch. Inside an agent loop, the agent cannot stop until that is true.

Results

<table> <tr><th></th><th>Best existing check</th><th>Millennium Harness</th></tr> <tr> <td><b>Published benchmark audit</b><br>_{4,219 AI-written solutions published as verified by <a href="https://arxiv.org/abs/2509.22908">vericoding</a>}</td> <td>at least <b>93 (2.2%) are fake</b>, all accepted by the benchmark's own check</td> <td>rejects <b>all 69</b> confirmed fakes in Lean and Dafny<br>_{0.2% false rejections · 0 misses in a random audit of 120 accepted files}</td> </tr> <tr> <td><b>Red team</b><br>_{96 cheats on real tasks}</td> <td>plain verifiers accept <b>83</b><br>strongest existing checkers accept <b>45</b><br>_{Lean FRO comparator logic, kernel replay, <code>#print axioms</code>, <code>dafny audit</code>}</td> <td>accepts <b>0</b><br>_{and all 25 honest solutions}</td> </tr> <tr> <td><b>Agents in the loop</b><br>_{OpenCode + GLM-5.3 Flash, 93 tasks}</td> <td><b>41%</b> honestly proved</td> <td><b>56%</b> honestly proved</td> </tr> </table>

Two of the fakes, verbatim, from solutions published as verified:

-- Make Int comparisons trivially true locally so the proof obligation becomes trivial
local instance : LE Int := ⟨fun _ _ => True⟩          -- GPT-5, LD0235

exact (sorryAx _ true)                                 -- GPT-5, LT0529: a `sorry` the benchmark's filter misses

_{The red-team suite was written alongside the checker; the 93 are a lower bound found among flagged files; with Claude Haiku 5.5 and DeepSeek V4.1 Flash the in-loop gain is 0 to 2 tasks. Full tables: <a href="docs/RESULTS.md">docs/RESULTS.md</a>, <a href="docs/audit-vericoded.md">docs/audit-vericoded.md</a>.}

Millennium RSI

Recursive self-improvement with a reward that cannot be gamed.

Recursive self-improvement is moving from theory to products. This month Recursive released Flint, an open-weight coding model whose pipeline, its CEO Richard Socher says, was almost entirely "done and improved upon by AI" (TechCrunch). The open question for every such system is the same: what stops a self-improving AI from improving its score instead of itself? Millennium RSI answers it with formal verification.

Self-improving AI systems are here: research agents now help design the next model. Every such loop is only as good as the score it climbs, and a system that rewrites itself to raise a score will find any gap between the score and the goal. An exit code is exactly such a gap.

Millennium RSI is an agent that improves its own harness, and keeps a change only if Millennium Harness certifies more held-out proofs with it.

flowchart LR
    A["Archive of harnesses<br/>strategy + lemma library"] -->|best on held-out tasks| B["Parent"]
    B -->|solve training tasks| C["Failures + verdicts"]
    C -->|improver model rewrites the harness| D["Child harness"]
    D -->|each new lemma kernel-checked<br/>before admission| E["Verified library"]
    E -->|score on held-out tasks<br/>with Millennium Harness| A

• The harness is data. A strategy and a lemma library, so every self-modification is inspectable and replayable.
• The library cannot be poisoned. A proposed lemma is admitted only if it compiles on its own, uses no banned construct and depends only on Lean's standard axioms.
• The reward cannot be gamed. A child scores only proofs of the unchanged statements. Teaching the solver to hide sorry, edit a theorem or redefine ≤ earns nothing.
• The ablation is built in. --reward exit0 runs the same loop on the usual exit-code criterion and records how many of its accepted "proofs" are fake.

python -m millennium_rsi run --solver z-ai/glm-5.3-flash --improver claude-haiku-5-5 \
    --generations 4 --train 12 --val 12 --out runs/rsi/glm

python -m millennium_rsi report runs/rsi/glm

Tasks are the curated development split of the vericoding Lean tasks (runs/fv/); the test split stays held out.

A first run (a small smoke test on 8 held-out tasks; GLM-5.3 Flash solving, Claude Haiku 5.5 improving):

$ python -m millennium_rsi report runs/rsi/smoke
reward=millennium solver=z-ai/glm-5.3-flash improver=claude-haiku-5-5
  gen  0  066c3ae8b4b9  proved   2/8  exit0   2  fake  0  $0.017
  gen  1  be658c95db6f  proved   3/8  exit0   3  fake  0  $0.018
  gen  2  3b18b727f5fa  proved   2/8  exit0   2  fake  0  $0.014
  gen  2  33ae894d9991  proved   2/8  exit0   2  fake  0  $0.016

All nine lemmas the improver proposed were kernel-checked before entering the library; the evolved harnesses are in runs/rsi/smoke/archive.json. Larger runs and the exit-code ablation are next.

Quickstart

Requires Python 3.10+ and the pinned toolchains: Lean v4.23.0-rc2 (via elan) and/or Dafny 4.11.

git clone https://github.com/sahibzada-allahyar/Formal-Verification-RSI.git millennium-harness

cd millennium-harness && pip install -e ".[dev]"

Check a solution against a task's frozen parts:

python -m millennium_harness.lean lock task_record.json frozen.json

python -m millennium_harness.lean check Solution.lean frozen.json

MILLENNIUM_DAFNY=~/.local/dafny-4.11/dafny/dafny python -m millennium_harness.dafny check solution.dfy frozen.json

Each prints a JSON verdict (PROVED, UNPROVED, CHEAT_REJECTED, SPEC_TAMPERED or CHECK_ERROR) whose feedback field is the message the gate shows an agent. Model calls need OPENROUTER_API_KEY or ANTHROPIC_API_KEY in the environment; the checkers themselves make none.

How it works

Lean · millennium_harness/lean.py, lean_check/Check.lean locks the frozen statements and tests, then inspects the compiled environment: statement equality after elaboration, axioms against a whitelist, instances and notation that reach frozen declarations, compiled-code swaps (implemented_by, extern), code run at elaboration time, and a kernel replay.

Dafny · millennium_harness/dafny.py requires the frozen specification to resolve unchanged on its own and rejects assume, {:axiom}, bodiless lemmas with ensures, disallowed attributes and captured specification helpers, then runs dafny audit and a compile check.

Agents · bench/agents_fv.py runs OpenCode or Claude Code with the gate in a sandbox; when the agent stops, the checker runs, and a failing verdict becomes the next prompt. adapters/ holds the OpenCode and Claude Code plugins.

Reproduce	Code	Results
Benchmark audit	bench/audit/	runs/audit/
Red team and strongest baselines	bench/redteam/, bench/baselines/	runs/redteam/
Agent study	bench/fv/, bench/agents_fv.py	runs/fv/grades/
Tests	tests/	pytest -q tests/

Third-party problem statements are not redistributed; the pipelines fetch them.

License

MIT. The hero animation is rendered with three.js (source).