Skip to main content
Glama
armsteadj1

Proofrail

by armsteadj1
OverviewSchemaSourceRelated ServersDiscussionsAdmin
TypeScript
Local

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

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

Tool

What it does

proofrail_verify

Load the manifest, resolve anchors, run the needed declared commands, rank all claims, return the least-proven packet. run=false scores from cached results without executing. claimIds restricts the set.

proofrail_focus

Return one packet. Defaults to the least-proven claim; claimId picks one. run is auto (reuse cached runs, run only what never ran), never, or always.

proofrail_recheck

Re-run only the commands one claim depends on, re-resolve its anchors, return satisfied and nextLeastProven.

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

kind

checks

strength

command

declared command exits with expect.exitCode (default 0) and output satisfies stdoutIncludes, stderrIncludes, outputIncludes, outputMatches

1.0

test with command

test name appears in the file and the command exits 0; output must mention the name unless the command's exact focusedTest matches

0.9

test without command

test name appears in the file (not executed)

0.6

file-contains

file contains text or matches pattern

0.4

manual

nothing; documents an unverifiable claim honestly

0

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

Available Tools

3 tools
proofrail_focusGet one repair packet (least-proven or a specific claim)A
Idempotent

Return a single repair packet. Without claimId it is the least-proven claim. run="auto" (default) reuses command results cached by an earlier verify/recheck and only runs commands that have never run; "never" never executes; "always" re-runs everything the manifest needs.

ParametersJSON Schema
NameRequiredDescriptionDefault
jevNoAlso ask the configured local Jev command for advisory judgments. Reports "unavailable" when none is configured.
runNo
claimIdNoClaim id to focus on instead of the least-proven one.
projectRootNoProject directory containing proofrail.json. Must be inside a root the server was started with. Defaults to the first allowed root.

TDQS

A3.9/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

The description explains the run modes (auto/never/always) and the reuse of cached command results, which goes beyond what the annotations convey. The annotations already provide idempotent/decent safety hints, and the description adds meaningful execution behavior without contradicting them.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is compact and front-loaded: it states the primary operation first, then the default selection behavior, then the run modes. Every sentence contributes necessary information without padding.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given four optional parameters, no output schema, and the presence of sibling tools, the description covers the core semantics of the tool well, including the least-proven default and run behavior. It does not elaborate on the shape of a repair packet or error cases, but those are not essential for selecting and invoking the tool correctly.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 75%, with run lacking a description; the description remedies this by explaining all three run enum values and their effect. It also clarifies the default behavior when claimId is absent, adding value beyond the schema's field descriptions.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose4/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description states it returns a single repair packet, with a concrete default (the least-proven claim) and an optional claimId override. It does not explicitly contrast itself with the sibling tools proofrail_verify and proofrail_recheck, but the resource and focus are clear enough to distinguish it from them.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description implies when the tool is used by referencing results 'cached by an earlier verify/recheck', which situates it in a workflow. However, it never explicitly says when to choose this tool over proofrail_verify or proofrail_recheck, or when not to use it.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

proofrail_recheckRe-run only what one claim needs and report whether it is now provenA
Idempotent

Re-run just the manifest commands referenced by the given claim, re-resolve its anchors, and return satisfied=true when the claim reaches score 1.0. Also names the next least-proven claim so the loop can continue.

ParametersJSON Schema
NameRequiredDescriptionDefault
jevNoAlso ask the configured local Jev command for advisory judgments. Reports "unavailable" when none is configured.
claimIdYesClaim id from a previous packet.
projectRootNoProject directory containing proofrail.json. Must be inside a root the server was started with. Defaults to the first allowed root.

TDQS

A4/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Beyond the annotations (idempotentHint=true, readOnlyHint=false), the description adds genuinely useful behavior: it re-executes manifest commands, re-resolves anchors, gates success on a specific score threshold (1.0), and returns a follow-up recommendation (the next least-proven claim). It also discloses the advisory Jev behavior via the schema parameter description. It omits failure-mode behavior (e.g., unresolvable anchors), but the core execution semantics are transparent.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Two dense sentences with zero filler. The core scoping claim ('Re-run just the manifest commands referenced by the given claim') is front-loaded, and the second sentence adds only the loop-continuation value. The title also carries distinct meaning rather than echoing the name.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

For a tool with no output schema, the description compensates by naming the key return elements (satisfied=true at score 1.0, the next least-proven claim). The three parameters are fully documented in the schema, including the projectRoot constraint. Minor gaps remain — response shape beyond 'satisfied', and error behavior when a claim cannot reach score 1.0 — but the description is largely complete for its complexity.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is 100%, so the baseline is 3 and the description need not restate parameters. The description does add light semantic linkage ('given claim' → claimId, 'configured local Jev command' → jev), but no parameter-level detail beyond what the schema already provides. That is exactly the baseline case.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description states a specific verb ('re-run'), a precise resource ('manifest commands referenced by the given claim'), a defined success criterion ('satisfied=true when the claim reaches score 1.0'), and a distinguishing scope ('only what one claim needs'). The title reinforces the 'recheck one claim' scope, which clearly separates it from siblings proofrail_verify and proofrail_focus.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Usage context is implied rather than explicit: the word 'just' contrasts with broader verification, and 'so the loop can continue' hints at an iterative workflow. However, no sibling is named, and there are no when-to-use vs. when-not-to-use conditions or explicit alternatives. The agent must infer the decision boundary from the scoping language.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

proofrail_verifyVerify claims and return the least-proven repair packetA
Idempotent

Load proofrail.json, resolve every anchor, run the manifest-declared commands the claims depend on, score every claim deterministically, and return the ranking plus one compact repair packet for the least-proven claim (anchors, missing proof, reproducer, done condition). Set run=false to score from cached command results without executing anything.

ParametersJSON Schema
NameRequiredDescriptionDefault
jevNoAlso ask the configured local Jev command for advisory judgments. Reports "unavailable" when none is configured.
runNoExecute the declared commands (default true). false uses cached results; dynamic proofs without a cached run report not-run.
claimIdsNoRestrict verification to these claim ids.
projectRootNoProject directory containing proofrail.json. Must be inside a root the server was started with. Defaults to the first allowed root.

TDQS

A3.8/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations already indicate non-read-only, non-destructive, and idempotent behavior. The description adds that it executes manifest-declared commands and scores deterministically, and that run=false skips execution. This adds behavioral context beyond annotations.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is a single, dense sentence that front-loads the core action and appends the run=false caveat. It is efficient with no filler.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

The description covers the main behavior, the return format (ranking plus repair packet with components), and the run=false option. Given the tool's complexity and lack of output schema, it is reasonably complete, though it could detail the ranking structure more.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The schema covers all four parameters with descriptions, and the description repeats the run=false behavior without adding new information. With 100% schema coverage, the description adds no extra semantic value, so baseline 3 applies.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states it loads proofrail.json, resolves anchors, runs manifest-declared commands, scores claims deterministically, and returns a ranking plus one repair packet. This is a specific verb and resource, and it distinguishes from typical tools by describing the full verification pipeline.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines2/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description provides no guidance on when to use this tool versus proofrail_focus or proofrail_recheck. It only mentions the run=false option for using cached results, which is a parameter behavior, not a tool-selection guideline.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Tool Schema Changelog

Recent tool additions, removals, and schema changes observed during successful MCP inspections.

  1. 3 tool updatesv0.1.0
    • First observedproofrail_focus
    • First observedproofrail_recheck
    • First observedproofrail_verify
Deploy Server
One endpoint for every MCP toolRayrun runs every MCP server behind one URL and holds the credentials. Each call is decided per client, tool, and argument, then recorded.ray.runAd

TDQS

A4.1/5.0

Scored across 3 tools

Disambiguation4/5

The three tools share a common domain (proof verification) and the verify/focus tools both produce repair packets, but their purposes are distinct: verify scores all claims, focus returns a single repair packet, and recheck re-runs for a specific claim. The descriptions clarify the differences, though the overlap between verify and focus could cause occasional misselection.

Naming Consistency5/5

All tools follow the same pattern: proofrail_<verb> (verify, focus, recheck). The naming is consistent snake_case with a clear prefix, making the tool set predictable and easy to navigate.

Tool Count5/5

Three tools is a well-scoped number for this domain—each tool serves a distinct role in the verification workflow (overall scoring, targeted repair, and incremental re-checking). No unnecessary bloat, and all three earn their place.

Completeness4/5

The toolset covers the core lifecycle: verify for full evaluation, focus for repair guidance, and recheck for confirming fixes. Minor gaps exist (e.g., no explicit tool for updating the manifest or listing all claims), but agents can work around them using the existing tools and the repair packet details.

Maintenance

ActivityMaintained
ResponsivenessNo issues

Resources

Related MCP Connectors

Related MCP Servers