sahibzada-allahyar/Formal-Verification-RSI

What it solves

AI-written proofs often look valid but are fake: tools like Lean accept sorry with a warning, Dafny accepts assume {:axiom} false as zero errors, and a solution can keep a theorem's text byte-identical while changing its meaning via shadowing instances. Existing benchmark checks miss these cheats. Millennium Harness closes that gap by verifying not just that a file compiles, but that the frozen specification kept its original meaning and was proved with no escape hatch. It rejects every one of the 96 red-team cheats tested, while accepting all 25 honest solutions.

How it works

Lean – The harness freezes the statements and tests, then inspects the compiled environment after elaboration. It checks statement equality, compares axioms against a whitelist, watches for instances/notation that reach frozen declarations, detects compiled-code swaps (implemented_by/extern), prevents code running at elaboration time, and replays the kernel verification.

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

Agent loop – When used with an AI agent (OpenCode or Claude Code), the gate runs after the agent stops. If the verdict is not PROVED, the failure feedback becomes the next prompt, so the agent must keep trying until the proof is genuinely certified.

Recursive self-improvement – Millennium RSI treats the harness itself as data: a strategy and a lemma library. A proposed lemma is admitted only if it compiles on its own, uses no banned construct, and depends only on Lean's standard axioms. A child harness scores only proofs of unchanged statements, so gaming the reward (hiding sorry, editing theorems, redefining ≤) earns nothing.

Who it's for

• Researchers and engineers building AI systems that generate machine-checked mathematics or formally verified code.
• Teams working on recursive self-improvement who need a reward that cannot be gamed.
• Anyone auditing published AI-written proofs for correctness.

Highlights

• 0/96 red-team cheats accepted – all fake proofs rejected, all 25 honest solutions accepted.
• Audit of 4,219 published AI solutions – rejects all 69 confirmed fakes in Lean and Dafny, with 0.2% false rejections and no misses in a random audit of 120 accepted files.
• Agent study – with OpenCode + GLM-5.3 Flash on 93 tasks, honest proof rate rose from 41% (standard exit-code reward) to 56% with the harness.
• Poison-resistant library – every lemma is kernel-checked before admission; the library cannot be silently corrupted.
• Immutable reward – a child improves only if it certifies more held-out proofs of unchanged statements.
• Ablation built in – --reward exit0 runs the same loop on the usual exit-code criterion to measure how many of its accepted proofs are fake.
• MIT licensed – open source and self-contained, with Python 3.10+ and pinned Lean/Dafny toolchains.