Millennium Harness CLI
Millennium Harness checks Lean 4 and Dafny proofs and rejects fakes until an agent proves the theorem without loopholes.
- 2,893 ★ on the repository
- Last commit
- MIT
Extended access
Why this level
- Installation puts a Python package from a clone on your machine, Lean and Dafny run on files you provide, and agent mode spends paid model calls.
Install
- Works in
Manual install
git clone https://github.com/sahibzada-allahyar/Formal-Verification-RSI.git millennium-harness
cd millennium-harness && pip install -e ".[dev]"Commands from the Quickstart section. Lean `v4.23.0-rc2` and Dafny 4.11 are installed separately.
Access and checks
How we reviewExtended accessThe tool runs code or makes network calls and only reads external data.
- Installation puts a Python package from a clone on your machine, Lean and Dafny run on files you provide, and agent mode spends paid model calls.
This is third-party code. Review the repository files before installing.
What it does
A model-free gate: a solution counts only if the frozen specification kept its meaning and was proved without an escape hatch. For Lean it catches `sorry`, shadowing instances and notation, extra axioms, compiled-code swaps and code run at elaboration time, then replays the check in the kernel. For Dafny it rejects `assume`, `{:axiom}`, bodiless lemmas and disallowed attributes. Inside an OpenCode or Claude Code loop the agent cannot stop until the verdict is `PROVED`, and a rejection returns to it as the next prompt. The author cites an audit of 4,219 published solutions and a red team of 96 cheats, of which the gate accepted none.
Who it is for. People who hand formal proofs or verified code in Lean and Dafny to agents and do not want to take a report of 0 errors on trust.
Good fit when
- An agent submits a Lean proof that suspiciously worked on the first try and contains `sorry` or its own `instance`.
- You need to check that the statement's meaning did not change while the theorem text stayed identical.
- A benchmark or pipeline accepts solutions by exit code and you want to be sure it is not being gamed.
- An agent loop in OpenCode or Claude Code should continue until the solution passes the gate.
Not a fit when
- Ordinary code with no formal specification: there is nothing to check.
- Lean `v4.23.0-rc2` or Dafny 4.11 cannot be installed: the gate is pinned to those versions.
- You need a tool that builds proofs: the gate only checks a finished solution.
Example request
Check my `Solution.lean` against the frozen specification `frozen.json` and explain the verdict: was it proved genuinely or not.Limitations
Python 3.10 or newer and pinned versions are required: Lean `v4.23.0-rc2` through elan and Dafny 4.11. The Dafny path is set with `MILLENNIUM_DAFNY`. The checks themselves make no model calls while running agents needs `OPENROUTER_API_KEY` or `ANTHROPIC_API_KEY`. The README figures come from the author: the cheat suite was written alongside the checker and the 93 fakes in a published benchmark are called a lower bound. With other models the in-loop gain was zero to two tasks. Installation is from a clone through `pip install -e`.
How to disable. Delete the `millennium-harness` clone and the environment where `pip install -e` was run. Disable the plugins from `adapters/` in the OpenCode or Claude Code settings.
FAQ
What verdicts does the gate return?
`PROVED`, `UNPROVED`, `CHEAT_REJECTED`, `SPEC_TAMPERED` or `CHECK_ERROR`. The `feedback` field holds the message the agent sees.
How do I freeze a specification?
With `python -m millennium_harness.lean lock task_record.json frozen.json`. The solution is then checked with `check`.
What does it catch in Dafny?
`assume`, `{:axiom}`, bodiless lemmas with `ensures`, disallowed attributes and captured specification helpers, followed by `dafny audit` and a compile check.
Are API keys needed?
Not for the checks themselves. `OPENROUTER_API_KEY` or `ANTHROPIC_API_KEY` is needed only to run agents and benchmarks.
Which agents does it work with?
The `adapters/` folder holds plugins for OpenCode and Claude Code and `bench/agents_fv.py` runs either of them with the gate in a sandbox.
Discussion
No questions or reviews yet.
Related
CLI toolsA plugin for proving theorems in Lean 4: mathlib search, sorry-filling cycles, axiom checks and safety hooks
A 2.4 KB charter for CLAUDE.md and three on-demand skills: the agent stops guessing, verifies results and gates irreversible steps
ADLC Harness takes a task from intent to PR with one command, and the human approves only four key gates.
A linter for the agent harness checks a repository's AGENTS.md, CLAUDE.md, CI and hooks and scores six dimensions.
Lean 4 skills for Codex and Claude Code: from project design to checking the statement against the source theorem
A DiDi plugin for Codex and Claude Code that runs a task from proposal to archive and keeps verified project knowledge in the repo
README in short
The README explains how agents game proof checking and presents the Millennium Harness gate with a results table. It installs from a clone and ships plugins for OpenCode and Claude Code.