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:

status	meaning
ok	the check ran and passed
failed	the check ran and failed — with the real error attached, for the repair loop
unavailable	the check could not run. Explicitly not a pass.

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.

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 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

tool	what it answers
lean_check	Does this Lean 4 source compile? On failure, returns the compiler's own error so the agent repairs its proof instead of asserting one.
axiom_audit	What does the theorem actually rest on? Catches sorryAx and anything outside the allowlist.
bound	What does a k-of-n record support? Exact one-sided Clopper–Pearson. "It passed every time" is not a bound.
gridlock_check	Can this wait-for relation wedge? Returns the actual cycle, and optionally checks a strictly decreasing rank.
cert_verify	Is this signoff-cert/v1 certificate real, with its false-pass bound recomputed from the evidence?
residency_check	Could a cross-tenant cache probe on this model even be interpreted?

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.

tool	question	needs
prereg_check	can this experiment's decision rule come out both ways?	preregister
state_floor	how many states must the system distinguish?	floorgen
gate_count	exactly how many states does removing this check admit?	gatecount
evidence_audit	run every applicable verifier over a tree, aggregate to one verdict	evidence

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 -->

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 <!-- /HONEST-SCOPE -->

<!-- PORTFOLIO -->

The rest of the portfolio

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

Tools

abstain-bench	how often does a verifier pass input it could not check?
evidence	run the whole portfolio over your repo — the weakest leg, never the mean
floorgen	what must your system remember? an exact lower bound
formal-proof-mcp	a proof kernel for your coding agent ← you are here
gatecount	exactly how many states does removing this check admit?
gridlock	certify a wait-for relation cannot wedge
honestbench	measure your CI's escape rate
kvleak	cross-tenant leak scanner
kvprobe	model-substitution detector with a measured FPR
preregister	refuses to seal a plan whose conclusion is already fixed
proof-to-code-drift	fail the build when the proof stops matching
sf-verify	re-derive admission decisions offline
signoff-cert	certificates that carry their own false-pass bound
tokencount	a token count both parties can recompute

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

illusion-bench	how many broken kernels does your oracle admit?
kv-reuse-econ-bench	recompute our economics headline
llm-tenant-isolation-bench	recompute our isolation figures

Datasets

abstain-corpus	32 inputs a verifier must NOT pass
kv-reuse-econ-traces	per-workload reuse accounting + the closed form
kv-tenant-isolation-bench	isolation observations, uninterpretable rows included
llm-precision-fingerprints	precision-labelled logprobs with a negative control

Try it in a browser — no install, no GPU

negative-results-atlas	ten claims we took back
tenant-leak-demo	the residency calculator
wait-for-visualiser	paste a wait-for graph, see the cycle

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. <!-- /PORTFOLIO -->