formal-proof-mcp

Your agent says it proved the theorem. Did anything actually check?

Six verification tools over the Model Context Protocol, with one invariant running through all of them:

A result that was not checked is never returned as a result that passed.

Not yet on PyPI. The command below is the one that works today. It installs from this repository, pinned to a tag.

pip install "git+https://github.com/nickharris808/formal-proof-mcp@v0.1.0"

pip install formal-proof-mcp is the intended command once the name is published. It 404s today, which is why it is not the first step above. The tag is pinned rather than @main so a reader installs the exact code this README documents.

Why this exists

Coding agents are fluent about correctness. They will tell you a proof went through, a bound holds, a graph is deadlock-free — and the failure mode is not that they lie, it is that nothing on the other end ever ran. A missing Lean toolchain, an uninstalled dependency, an empty input: each returns something, and "something" reads as success.

So every response here carries status, and the three values are kept strictly apart:

An agent that reads "no Lean toolchain installed" as "no errors found" will confidently assert a proof it never checked. This server makes that confusion impossible to express.

Related MCP server: prova-mcp

The check that matters most

lake build exits 0 on a development riddled with sorry. Lean accepts the placeholder, compiles happily, and reports success. Compiling is necessary and nowhere near sufficient — only #print axioms reveals what a theorem actually rests on:

$ formal-proof-mcp --selftest
  ok    clean axioms accepted
  ok    sorryAx caught
  ok    empty audit FAILS rather than passing quietly
  ok    0-of-250 bounded at ~1.2%
  ok    acyclic graph certified
  ok    cycle caught with its path
  ok    non-decreasing rank caught
  ok    unknown tool fails loudly
  ok    tools/list returns all six

  lean toolchain: present

selftest passed.

Note line 3. An axiom audit over empty input fails. A coverage tool that cannot cover anything must never pass quietly — that is how an entire corpus goes unaudited while CI stays green.

Install

Not yet on PyPI. pip install formal-proof-mcp is the intended install once published; until then install from the repository — it works exactly the same:

pip install git+https://github.com/nickharris808/formal-proof-mcp@main

pip install formal-proof-mcp                 # zero dependencies
pip install "formal-proof-mcp[siblings]"     # adds cert_verify and residency_check

30-second quickstart

formal-proof-mcp --selftest      # prove each tool actually fires
formal-proof-mcp --list-tools    # the ten tools
formal-proof-mcp                 # serve MCP over stdio

Wire it into Claude Desktop or Cursor:

{
  "mcpServers": {
    "formal-proof": { "command": "formal-proof-mcp" }
  }
}

The ten tools

Added in 0.2 — the rest of the portfolio

Each of these delegates to a sibling package. If that package is not installed the result is unavailable, never ok — an agent reading "not installed" as "checked and fine" is the exact failure this server exists to prevent, and a missing optional dependency is the likeliest way to produce it. There is a test that blocks the import and asserts the status.

Not yet on PyPI. pip install formal-proof-mcp is the intended install once published; until then install from the repository — it works exactly the same:

pip install git+https://github.com/nickharris808/formal-proof-mcp@main

pip install "formal-proof-mcp[portfolio]"     # the server plus all four

prereg_check is the one to reach for first. An agent about to run an experiment can be told, before it burns a GPU hour, that its rule cannot fail:

{"decision_rule": "argmax_flips > 0",
 "metrics": {"argmax_flips": {"type": "integer", "lo": 0, "hi": 0}}}

{"status": "failed", "verdict": "UNFALSIFIABLE",
 "explanation": "THE FINDING CAN NEVER BE REPORTED. ... The run is guaranteed to return the null
                 before any data is collected."}

Worked example — driving it the way a client does

Pipe JSON-RPC in, read JSON-RPC out:

$ printf '%s\n' \
  '{"jsonrpc":"2.0","id":1,"method":"initialize","params":{}}' \
  '{"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"gridlock_check",
    "arguments":{"edges":[["a","b"],["b","c"],["c","a"]]}}}' \
  | formal-proof-mcp

initialize -> {'name': 'formal-proof-mcp', 'version': '0.1.0'} 2024-11-05
id=2 isError=True status=failed  wait-for cycle: a -> b -> c -> a

And the audit that catches an assumed theorem:

id=2 isError=True status=failed
  1 theorem(s) depend on sorryAx: these are ASSUMED, not proved, and the development
  still compiles

isError is how the agent learns a check failed rather than merely returned, and the cycle comes back as a path so the answer is actionable rather than a bare boolean.

Honest limits

• lean_check needs a Lean toolchain. Without one it returns unavailable, never a pass. Install via elan.

• cert_verify and residency_check delegate to signoff-cert and kvleak. Absent, they report unavailable with the pip install line — they never fake a verdict.

• The axiom allowlist is a policy choice, not a law. Classical.choice is permitted by default; tighten it with the allowed argument if your development is constructive.

• gridlock_check reasons about the graph you hand it. It cannot know whether that graph faithfully models your system, which is the part only you can supply.

• No auto-repair loop is included. The server returns the compiler error; the retry is the agent's to run. An earlier draft of this README promised a bounded repair loop, which the code does not implement — the error trace is what ships.

• No SDK, by design. MCP is JSON-RPC 2.0 over stdio; implementing it directly keeps the dependency count at zero and the whole transport auditable in one short file.

The commercial edition

This server verifies and reports. It does not gate.

The gate corpus, the automated repair mechanisms, and the certificate-issuing faucet are the licensed offering — an operator who wants a failed check to block a deploy is performing the step this package deliberately does not. See CLAIMS-MAP.md for exactly where that line sits.

Reading is free. Enforcing is licensed.

Licence

Apache-2.0 · CLEAN — exposes a toolchain and reports; implements no filed apparatus.

Honest scope — what a passing run proves, and what it does not

The two halves are inseparable. A tool that states only the first half is marketing.

It proves:

• whether Lean source compiles, and what axioms a theorem actually rests on (including sorryAx)

• whether a wait-for graph can wedge, and an exact k-of-n bound

• explicitly, when a check COULD NOT RUN — unavailable is never merged into ok

It does NOT prove:

• that a theorem says what its name or docstring suggests. #print axioms proves the dependency set is clean, never that the statement is the one you wanted

• that a passing lake build means anything — a development full of sorry compiles and exits 0

• anything when the toolchain is absent; it reports unavailable and stops

Full CLI reference, generated from --help: docs/CLI.md

Contributing

Bug reports and pull requests welcome — see CONTRIBUTING.md.

A false accusation is a defect of equal severity to a missed detection. If this tool flags something correct, open an issue with the input and the verdict you expected: over-refusal trains people to bypass refusals, which destroys the tool.

Citation metadata is in CITATION.cff.

The rest of the portfolio

25 artifacts, one idea: a measurement you cannot check is a press release. Every tool here reports; none of them gates.

Tools

Benchmarks — each recomputes one of our own published numbers from its certificate

Datasets

Try it in a browser — no install, no GPU

Documentation

Everything above, explained in one place: https://nickharris808.github.io/evidence-docs/ — the tutorial, what this proves and what it does not, and a CLI reference generated by running --help on every published command.

The commercial edition

Everything above is measure-only and Apache-2.0: it tells you what is true and never acts on it. The enforcement side — binding a partition key at the admission decision, the compiled gate corpus, and the certificate-issuing faucet — is covered by filed patents and licensed separately.

Reading is free. Enforcing is licensed.