Proofrail

Proofrail is a small stdio MCP server for Claude Code and Codex. After an agent edits code, it asks Proofrail which claim about the code is least proven. Proofrail answers with one compact repair packet: exact source anchors, the proof that is missing, a reproducer, and a done condition. There is no repo-wide "looks good" verdict, only the next specific thing to prove.

Proofrail packet 1/4: percent-rounds-half-up — failing, score 0.00, deficit 2.00
Claim: percent(part, whole) rounds .5 upward, so percent(1, 8) is 13.
Anchors:
  - src/calc.js:15-17 percent
          15| export function percent(part, whole) {
          16|   return Math.round((part / whole) * 100);
          17| }
Missing proof:
  - [command/failed] command "unit": output lacks "percent rounds half up"
    → Make command "unit" produce exit 0 and output including "percent rounds half up".
Reproduce: node --test test/calc.test.js (cwd .)
Done when: all 1 proof for "percent-rounds-half-up" pass and all 1 anchor resolve (score 1.0 on recheck).
Next: Make command "unit" produce exit 0 and output including "percent rounds half up".
Jev: unavailable (no jev command configured (set manifest.jev or PROOFRAIL_JEV_CMD))

How it works

1. The project declares a proof manifest (proofrail.json): the commands Proofrail may run, and a list of claims. Each claim has source anchors and proofs.

2. proofrail_verify resolves every anchor against the current source, runs the declared commands the claims depend on, and scores each claim deterministically.

3. The lowest-scoring claim (weighted) becomes the repair packet.

4. The agent applies the packet's next step, then calls proofrail_recheck with the claim id. Recheck re-runs only what that claim needs and reports satisfied plus the next least-proven claim.

Related MCP server: Infinite Code Next

Install

Requires Node 20 or newer. Proofrail builds itself on install, so it runs straight from GitHub:

npx --yes github:armsteadj1/proofrail --help

Or add it to a project:

npm install --save-dev github:armsteadj1/proofrail

Claude Code

From the project directory:

claude mcp add proofrail -- npx --yes github:armsteadj1/proofrail

Or in .mcp.json at the project root (shared with the team):

{
  "mcpServers": {
    "proofrail": {
      "command": "npx",
      "args": ["--yes", "github:armsteadj1/proofrail"]
    }
  }
}

Claude Code starts MCP servers with the project as the working directory, which becomes Proofrail's allowed root.

Codex

Add to ~/.codex/config.toml (or the project's .codex/config.toml):

[mcp_servers.proofrail]
command = "npx"
args = ["--yes", "github:armsteadj1/proofrail"]

Or from the CLI:

codex mcp add proofrail -- npx --yes github:armsteadj1/proofrail

Restricting roots

By default the only allowed root is the server's working directory. Pass --root one or more times to allow other directories; every projectRoot a tool call passes must be inside an allowed root.

{ "command": "npx", "args": ["--yes", "github:armsteadj1/proofrail", "--root", "/abs/path/to/repo"] }

Tools

All three accept projectRoot and jev (see below). Results carry a text rendering plus structuredContent with the same data as JSON.

Suggested agent loop:

verify → apply packet.next → recheck(claim) until satisfied → verify again

The manifest

proofrail.json at the project root (or .proofrail/manifest.json). A JSON Schema ships in schema/proofrail.schema.json. The full example is in examples/tiny-calc.

{
  "$schema": "node_modules/proofrail/schema/proofrail.schema.json",
  "version": 1,
  "commands": {
    "unit": { "cmd": "node", "args": ["--test", "test/calc.test.js"], "timeoutMs": 60000 }
  },
  "claims": [
    {
      "id": "divide-rejects-zero",
      "statement": "divide(a, 0) throws a RangeError instead of returning Infinity.",
      "weight": 2,
      "anchors": [{ "file": "src/calc.js", "symbol": "divide" }],
      "proofs": [
        { "kind": "command", "command": "unit", "expect": { "exitCode": 0, "outputIncludes": "divide by zero throws" } },
        { "kind": "test", "file": "test/calc.test.js", "name": "divide by zero throws", "command": "unit" },
        { "kind": "file-contains", "file": "src/calc.js", "pattern": "throw new RangeError" }
      ],
      "reproducer": "node --test test/calc.test.js",
      "done": "A test named \"divide by zero throws\" exists and passes."
    }
  ]
}

Commands

commands.<name> is the only place executables come from. Each has cmd, args, optional cwd (must stay inside the root), env, timeoutMs (default 120 s, max 10 min), and maxOutputBytes (default 64 KiB, max 1 MiB).

A command that intentionally selects exactly one test may declare focusedTest:

{
  "cmd": "npx",
  "args": ["vitest", "run", "src/example.test.ts", "-t", "handles invalid input"],
  "focusedTest": { "file": "src/example.test.ts", "name": "handles invalid input" }
}

focusedTest must exactly match a test proof that references the command. When it does, exit 0 proves that test even if the reporter omits its full name (for example, Vitest's 1 passed, 83 skipped summary). Without focusedTest, the existing rule remains: the command output itself must mention the exact test name. A generic green command therefore cannot certify an unreported test.

Anchors

An anchor is file plus one of:

• symbol: a declared name. Proofrail recognises common declaration forms in JavaScript, TypeScript, Python, Go, Rust, Ruby, Java, and C#, and finds the block end by braces or indentation.

• pattern: a regular expression; the first matching line is the anchor.

• lines: an explicit [start, end] range.

Anchors resolve to file:start-end with a short numbered snippet. An anchor that no longer resolves after a refactor drags the claim's score down, which is how stale claims surface.

Proofs

Scoring and ranking

Every claim gets a deterministic score in [0, 1]:

proofScore   = Σ strength(passed proofs) / Σ strength(all proofs)     (0 if no proofs)
anchorFactor = resolved anchors / declared anchors                     (0.5 if none declared)
score        = proofScore × anchorFactor
deficit      = weight × (1 − score)

Claims are ordered by deficit descending, then status (failing, unproven, pending, partial, proven), then unresolved anchor count, then non-passing proof count, then claim id. The first claim is the packet. Same inputs always produce the same packet.

Safety model

• Only manifest commands run. Tool inputs carry claim ids and a project root, never command strings. Commands are spawned with shell: false and a fixed argument vector, so nothing in the manifest or tool input is shell-interpreted.

• Root boundary. Files and command working directories are resolved against the project root and rejected if they escape it lexically or via symlink. The project root itself must be inside a root the server was started with.

• Bounded execution. Every command has a timeout (SIGTERM then SIGKILL) and an output cap. Truncation is reported, not hidden.

• Read-only. Proofrail writes nothing. The manifest is trusted the way package.json scripts are: review it like code.

• Harness protocol variables (for example NODE_TEST_CONTEXT) are scrubbed from child environments so spawned test runners behave normally.

Optional Jev adapter

Proofrail can attach advisory judgments from TypeSafe's Jev to each packet. Proofrail never calls the network itself. Configure a local command; Proofrail writes one TypeSafe System One request to its stdin and expects the API-shaped response on stdout:

{ "model": "jev-latest", "state": { "claim": {}, "anchors": [], "proofs": [] },
  "questions": { "proof_covers_claim": { "type": "noul", "instructions": "...", "criteria": {} },
                 "anchors_match_claim": { "type": "noul", "instructions": "..." },
                 "best_repair": { "type": "choice", "instructions": "...", "criteria": {} } } }

Response: { "answers": { "<id>": { "type": "noul", "noul": 0.8 } | { "type": "choice", "choice": "add_or_fix_test", "confidence": 0.9 } } }.

Configure it either in the manifest:

"jev": { "cmd": "node", "args": ["scripts/jev-bridge.mjs"], "timeoutMs": 15000, "model": "jev-latest" }

or with environment variables, which take precedence: PROOFRAIL_JEV_CMD, PROOFRAIL_JEV_ARGS (JSON array), PROOFRAIL_JEV_TIMEOUT_MS, PROOFRAIL_JEV_MODEL.

Pass jev: true to a tool to consult it. The packet's jev field is one of:

• { "status": "unavailable", "reason": ... } when nothing is configured or it was not requested;

• { "status": "error", "reason": ... } when the command fails, times out, prints invalid JSON, or omits an answer;

• { "status": "ok", "answers": ... } with the answers exactly as returned.

Proofrail never fabricates Jev output, and Jev answers never change the deterministic score. They are advice next to it.

CLI

The same engine is available without MCP, useful in CI or for trying a manifest:

proofrail validate [dir]                       # parse the manifest
proofrail verify   [dir] [--no-run] [--json]   # exit 1 while any claim is unproven
proofrail focus    [dir] [--claim id] [--run auto|always|never]
proofrail recheck  <claimId> [dir]             # exit 0 once satisfied
proofrail [--root dir]...                      # stdio MCP server (default)

Development

npm install
npm test               # builds, then runs the Node test suite (unit + CLI + stdio MCP smoke)
npm run schema         # regenerate schema/proofrail.schema.json from the zod schema
node dist/cli.js verify examples/tiny-calc

CI runs the suite on Node 20, 22, and 24 across Linux and macOS, checks the schema is current, and installs the checkout the way npx github: does.

License

MIT