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.

pip install formal-proof-mcp

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

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 six tools
formal-proof-mcp                 # serve MCP over stdio

Wire it into Claude Desktop or Cursor:

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

The six tools

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.

The rest of the portfolio

Seventeen 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

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.