lean-lockstep

A project harness for Lean 4 formalization work done by several agents at once: AI coding agents of any kind (anything that can run a shell command or call an MCP tool) and people. It keeps the state of the project (which statements are open, claimed, proved, and what depends on what) derived from the compiled Lean environment, and it records who is doing what, why, and with how much memory.

• State comes from Lean, not from a document. Each open statement is a node: a theorem with a sorry in its own blueprint module, tagged in its docstring. lockstep extract reads the compiled environment and reports each node as open, claimed or closed (sorry-free with allowlisted axioms). There is no hand-kept status file that can drift.
• Approved statements are locked. harness/statements.lock records the type hash of every approved statement. A proof that quietly weakens its statement shows up as a lock violation; changing a statement takes lockstep node restate, which logs who approved it and why. This is the failure mode that matters most when agents write the proofs.
• Agents coordinate through the harness. Claims expire and carry the intent (--why); every release records an outcome; lockstep log and lockstep journal keep the trail; long commands run as recorded, memory-capped jobs that every agent can see.
• Audits scale. The axiom audit is a per-module taint scan with a cache, which finishes on projects where #print axioms does not.
• No client or model is assumed. Every command has a CLI and an MCP tool. A git pre-commit hook guards commits for everyone; optional Claude Code hooks add a session banner and a guard against compute launched outside the harness.

Status: experimental (0.1). Built and used in two research projects; expect rough edges outside them. Linux first.

Requirements

• Python 3.11 or newer. The core has no dependencies; extras: mcp (MCP server), test (pytest), research (NumPy for research-library probes).
• Lean 4 through elan, Lake, and git.
• The memory guard runs each lake invocation in a capped systemd-run --user scope, so it needs Linux with a systemd user session. Elsewhere set [build] guard = false.
• bwrap (bubblewrap) for the sandboxed proof checks of the experimental automation layer.

Try it

examples/minimal is a Lean-only Lake project (no Mathlib) with one core lemma and an empty blueprint. From a checkout of this repository:

cd examples/minimal
export LOCKSTEP_AGENT=me:demo            # every claim, job and log entry is recorded under this id
../../bin/lockstep build core
../../bin/lockstep extract               # writes harness/nodes.json, index.json, status.md
../../bin/lockstep node add --name double_succ --ws A --kind formalization \
  --type "(n : Nat) : (n + 1) + (n + 1) = 2 * n + 2" \
  --description "Doubling a successor." --depends double --dangling-ok "example"
../../bin/lockstep ready                 # Demo.double_succ is open and ready
../../bin/lockstep claim double_succ --why "rewrite with Demo.double, then omega"
# replace the `sorry` in DemoBlueprint/A/DoubleSucc.lean with `rw [double]; omega`
../../bin/lockstep check double_succ     # sorry=False status=closed
../../bin/lockstep close double_succ     # moves it into the core library, records the attempt
../../bin/lockstep audit && ../../bin/lockstep journal

tests/test_example_lifecycle.py runs the same sequence whenever lake is installed. To start over, run git checkout -- . && git clean -fdx . in examples/minimal.

Installing

The harness writes Lean files into the project (the extractor, node modules) and its lock hashes depend on the toolchain, so pin the version a project uses. Either:

• From PyPI, which puts lockstep and lockstep-mcp on the PATH:

  uv tool install "lean-lockstep[mcp]==0.1.0"     # or: pipx install "lean-lockstep[mcp]==0.1.0"
  

  Without PyPI access, install a tag from git instead: uv tool install "lean-lockstep[mcp] @ git+https://github.com/GLitchfield/lean-lockstep@v0.1.0".
• As a git submodule, pinned by commit and upgraded by bumping the pin, which suits a project that also develops the harness:

  git submodule add https://github.com/GLitchfield/lean-lockstep tools/lockstep
  uv venv tools/lockstep/.venv && uv pip install -e "tools/lockstep[mcp]"
  

  tools/lockstep/bin/lockstep and tools/lockstep/bin/lockstep-mcp prefer that virtualenv and fall back to the system python3.

The commands below write lockstep; with a submodule, that is tools/lockstep/bin/lockstep.

Adopting it in a project

1. Give the Lake package two libraries: a core library (proved results only) and a blueprint library whose root file imports every node module. lockstep node add maintains that root.
2. Copy examples/minimal/harness/ and edit harness/config.toml: namespaces, layers, build targets, memory caps. Start statements.lock as {} and allowlist.json as [].
3. Ignore the harness state directory (.lockstep/ with [project] state_home = ".lockstep").
4. Write the agent rules into the files your clients read (AGENTS.md, CLAUDE.md, ...) and list them under [rules]; lockstep rules checks that they carry the same rule list (cheap enough for CI). examples/minimal/AGENTS.md is a starting point. Tell each agent to export a stable LOCKSTEP_AGENT (for example <client>:<session id>); claims and logs are recorded under it.
5. Guard commits with the git hook, which works whoever commits:

   printf '#!/bin/sh\nexec lockstep hook pre-commit\n' > .git/hooks/pre-commit && chmod +x .git/hooks/pre-commit
   

   It refuses a commit that fails lockstep layers, lockstep extract --check (generated files out of date or a locked statement changed) or lockstep audit --changed.
6. Register the MCP server with your client: command lockstep-mcp (or tools/lockstep/bin/lockstep-mcp), stdio, no arguments. For example .mcp.json:

   { "mcpServers": { "lockstep": { "command": "tools/lockstep/bin/lockstep-mcp", "args": [] } } }
   

7. Optionally, for Claude Code, add the session and shell hooks to .claude/settings.json:

   { "hooks": {
       "SessionStart": [{ "hooks": [{ "type": "command", "command": "tools/lockstep/bin/lockstep hook session-start" }] }],
       "PreToolUse": [{ "matcher": "Bash", "hooks": [{ "type": "command", "command": "tools/lockstep/bin/lockstep hook pre-bash" }] }] } }
   

   session-start prints the session's agent id and lockstep status --brief. pre-bash blocks a bare nohup/systemd-run (compute goes through lockstep job run) and runs the commit guard before git commit/git push. Any client whose hooks pass the same JSON on stdin can use them.
8. In CI, python3 -m lockstep.lock BASE_LOCK HEAD_LOCK (with PYTHONPATH=tools/lockstep for a submodule) prints the log files a lock change must touch: restatements.md when an approved statement changed or disappeared, retired.md for a refutation. New entries need none.
9. Optionally, tools/lockstep/systemd/install.sh (from a checkout) installs a lockstep-nightly-<project id> user timer (03:00) that runs the guarded core build, lockstep extract --check and lockstep audit.

Commands

Every command takes --json, and all but the hooks are also MCP tools. Node names may be dotted relative to the declaration namespace (--name List.foo declares theorem List.foo in it), and --depends lists the project declarations a node waits on (library lemmas belong in the description).

Experimental

These work in the projects they came from but are less general; see docs/automation.md:

• Automation layer: durable operation … workflows run by lockstep worker, a results inbox, proof capture|check|prove, node finish, probe run|replay, context.
• Research library: lib search|show|list over a project catalog (harness/research/catalog.json).
• Certificate layers: [layers] rules for generated proof-module families, and storage share for their compiled artifacts.

Things that cost hours to learn

• Never import the project modules at the top of a lake env lean --run script that also calls importModules on them. The script's own import maps the oleans; the second load cannot mmap at the same addresses and reads them into anonymous memory instead (37 GB and a cgroup OOM kill on a project with large certificate modules). The extractor template imports only Lean; main imports the project.
• Never use importAll := true for the extractor environment (30+ GB). A plain import exposes every theorem value in env.header.moduleData.
• Never run bare lake build on big targets. Lake 5 has no -j; two dozen parallel compilers exhaust a 20 GB guard. lockstep build builds Lake's out-of-date list one module per guarded invocation first.
• #print axioms does not finish on large generated proof families (16 TB read in 3.5 h); the extractor's module-order taint scan with a per-module cache is the audit path.
• A module-system core root (module header) cannot import plain files. When the core root uses it, nodes are written in module form from the start, so a proof elaborates against the same imports before and after lockstep close.
• The elaborator moves parts of a proof into auxiliary declarations (foo._proof_1), so a dependency scan of a theorem's value alone reports the auxiliaries instead of the lemmas they use. The extractor looks through a declaration's own auxiliaries.

Development

uv venv .venv && uv pip install -e ".[test,mcp,research]"
.venv/bin/python -m pytest

Releases follow semantic versioning (0.x: minor versions may break). Changes are listed in CHANGELOG.md. To release, bump __version__ in lockstep/__init__.py, add the changelog entry, and push a vX.Y.Z tag: .github/workflows/release.yml builds the sdist and wheel and publishes them to PyPI through trusted publishing.

License

MIT; see LICENSE.