Proofspec

Claims are cheap. Proofspec makes them executable.

A README, release note, product page, or agent completion message can say more than the evidence behind it. Proofspec turns the important statements in those texts into versioned evidence contracts. It checks those contracts with constrained verifiers, preserves hash-chained receipts, models dependencies between claims, and fails CI when required claims are not actually verified.

It is for maintainers who publish claims about their software and for agent setups that should check a claim before reporting it. It is not a test runner, not a link crawler, and not a fact-checker for prose.

README / release / product claim
              │
              ▼
       proofspec.json
   policies + dependencies
              │
              ▼
  constrained observations
  file · HTTP · Git · npm · manual
              │
              ▼
 receipts + CI gate + reviewer reports
 JSON · Markdown · HTML · Mermaid · SARIF

Proofspec does not declare broad truth. A satisfied verifier proves only the observation you configured. Unknown stays unknown; manual stays manual; a dependency that is not verified blocks the claims built on top of it.

Try it in two minutes

Requires Node.js 20 or newer.

Install the v0.1.0 release artifact from GitHub into a project, then call the local binary with --no-install, which stops with an error instead of downloading anything if the local install is missing:

npm install --save-dev https://github.com/christian140903-sudo/proofspec/releases/download/v0.1.0/proofspec-0.1.0.tgz
npx --no-install proofspec init     # writes proofspec.json with one claim: README.md exists
npx --no-install proofspec check    # exit 0: gate passed · exit 1: a required claim is not verified

In a project without a README.md, the first check prints Proofspec FAIL — my-project and 0/1 verified · 1 failed and exits with 1: the starter claim is not true yet. Add a README.md and run check again to see it pass. The reports (JSON, Markdown, HTML, Mermaid, SARIF) and the receipt ledger land in .proofspec/.

In Claude Code, add the MCP server from the same release artifact. It reads proofspec.json from the project directory:

claude mcp add proofspec -- npx --yes --package=https://github.com/christian140903-sudo/proofspec/releases/download/v0.1.0/proofspec-0.1.0.tgz -- proofspec serve

To try the CLI once without adding a dependency, name the release artifact explicitly:

npx --package=https://github.com/christian140903-sudo/proofspec/releases/download/v0.1.0/proofspec-0.1.0.tgz -- proofspec --help

Last tried on 2026-10-08 in an empty project with an empty npm cache (Node 22, Linux): install, init and the first check took 8 seconds including the download. claude mcp list showed the server as connected; a separate MCP client calling proofspec_check through the same command found the project's proofspec.json.

Related MCP server: Spec Kit Acceptance Gate MCP

Why it exists

README linters check structure. Link checkers check URLs. Transcript auditors compare an agent's words with a repository after the fact. Proofspec occupies a different layer: the project author defines the evidence contract that must travel with a public claim, and the same contract runs locally, in CI, through TypeScript, or as an MCP tool.

A fair comparison: markdown-link-check checks every link in a Markdown file and tells you which ones are dead, without any specification. Proofspec checks only what you configure. In exchange, a claim can require that one specific page answers with status 200 and contains the version the sentence next to the link names; if that claim has severity error, the build fails when either stops being true.

Useful examples:

• “Version 1.4.0 is public on npm” → registry version check.

• “The release page is live” → public HTTP status/content checks.

• “This artifact contains 358 passing tests” → bounded JSON evidence plus an explicit limitation that the manifest does not replay the tests.

• “The published commit is tagged” → Git tag and remote-containment checks.

• “A human approved the usability” → manual evidence that remains unknown, never silently upgraded to external proof.

A specification

{
  "$schema": "https://raw.githubusercontent.com/christian140903-sudo/proofspec/main/proofspec.schema.json",
  "schemaVersion": 1,
  "project": { "name": "example" },
  "claims": [
    {
      "id": "release-visible",
      "statement": "example 1.0.0 is public on npm.",
      "severity": "error",
      "policy": { "mode": "all" },
      "evidence": [
        {
          "id": "npm-version",
          "verifier": {
            "kind": "npm",
            "package": "example",
            "check": { "op": "version_exists", "version": "1.0.0" }
          }
        }
      ],
      "limitations": ["Registry visibility does not establish package quality."]
    }
  ]
}

Editor validation is provided by proofspec.schema.json. Runtime validation additionally rejects duplicate IDs, unknown dependencies, impossible thresholds, and dependency cycles.

Evidence policies and claim graphs

Each claim supports one evidence policy:

dependsOn creates a directed claim graph. A directly verified claim becomes blocked when any dependency is not effectively verified. The configuration validator rejects cycles.

The default gate fails only non-verified error claims. --strict requires every claim, regardless of severity, to be verified.

Verifiers

Proofspec inherits the constrained verifier surface from postcondition-mcp:

There is intentionally no arbitrary shell verifier and no custom authorization header surface.

Reports

proofspec validate [config]
proofspec check [config] --formats json,markdown,html,mermaid,sarif
proofspec explain release-visible [config]
proofspec check [config] --out artifacts/proofspec

• JSON is the canonical machine-readable run report.

• Markdown is designed for release notes and human review.

• HTML is a standalone, escaped, no-index dashboard.

• Mermaid visualizes claim dependencies.

• SARIF exposes non-verified claims to code-scanning interfaces.

Every evidence check creates a Postcondition receipt. The local SQLite ledger is hash chained and revalidated at the end of each run. Reports include a stable digest and redact the configured project-root prefix from observed values.

The repository also checks its own public surface in CI. That self-spec deliberately leaves the subjective usefulness claim as informational and unknown.

MCP server

From a clone, build once and point the MCP client at the absolute entry path:

{
  "mcpServers": {
    "proofspec": {
      "command": "node",
      "args": ["/absolute/path/to/proofspec/dist/src/index.js", "serve"],
      "env": { "PROOFSPEC_CONFIG": "/absolute/path/to/proofspec.json" }
    }
  }
}

Without a clone, point npx at the release artifact. Do not use npx -y proofspec serve; that starts the unrelated npm package.

{
  "mcpServers": {
    "proofspec": {
      "command": "npx",
      "args": [
        "--yes",
        "--package=https://github.com/christian140903-sudo/proofspec/releases/download/v0.1.0/proofspec-0.1.0.tgz",
        "--",
        "proofspec",
        "serve"
      ],
      "env": { "PROOFSPEC_CONFIG": "/absolute/path/to/proofspec.json" }
    }
  }
}

The stdio server exposes:

• proofspec_validate

• proofspec_check

• proofspec_explain

• proofspec_render

• resources proofspec://schema and proofspec://example

• prompt audit-public-claims

TypeScript API

After installing the release artifact as shown in Try it in two minutes (not npm install proofspec, which fetches the unrelated registry package):

import { runProofspec, renderReport } from 'proofspec';

const report = await runProofspec('./proofspec.json');
console.log(report.summary.gatePassed);
console.log(renderReport(report, 'markdown'));

CI

- run: npm install --no-save https://github.com/christian140903-sudo/proofspec/releases/download/v0.1.0/proofspec-0.1.0.tgz
- run: npx --no-install proofspec check proofspec.json

Keep --no-install in CI. npm answers its own install prompt with "yes" when it detects CI or a non-interactive shell, so if the install step failed, plain npx proofspec would fetch and run the unrelated proofspec package instead.

Commit the specification, not the generated .proofspec/ ledger. Upload the reports as build artifacts if reviewers need them.

Verify it yourself

git clone https://github.com/christian140903-sudo/proofspec && cd proofspec
npm ci && npm test        # expected: 74 passing (last verified 2026-10-08, Node 22, fresh clone)

The tests cover the configuration schema and its validator (duplicate IDs, unknown dependencies, cycles, impossible thresholds), the three evidence policies and dependency blocking, the default and strict gates, all five report formats including HTML escaping, the receipt ledger and path redaction, the CLI and its exit codes, one real MCP exchange over stdio, the bundled example, and a guard that fails if any Markdown example runs plain npx proofspec. CI runs them on Node 20, 22 and 24.

What they do not cover: no test contacts a real website or the npm registry (HTTP and npm checks are schema-validated here; their network behaviour is tested in postcondition-mcp), CI runs on Linux only, and the summary line that check --strict prints is not asserted (see below).

The repository checks its own README, docs, package metadata and example with Proofspec; CI runs this after the tests:

node dist/src/index.js check proofspec.json --no-write
# expected: Proofspec PASS — Proofspec
#           5/6 verified · 0 failed · 1 unknown · 0 unsupported · 0 blocked

The one unknown is the manual claim that a human has reviewed Proofspec's broader usefulness. It stays unknown on purpose.

Further checks, after npm test has built dist/:

node dist/src/index.js check examples/proofspec.json   # the bundled example
npm run test:coverage                                   # coverage report
npm run smoke:pack                                      # packs the tarball, installs it in a scratch project, runs the CLI, imports the SDK

The example verifies three required claims, reports one honest informational unknown, writes five report formats, and still passes the default gate. Add --strict to require warning and info claims too.

What it does not do

• It does not run your tests or any other command. There is no shell verifier. A claim such as “all tests pass” needs a machine-readable artifact or a published result, and a manifest records a value; it does not replay the tests.

• It does not judge prose. A satisfied verifier proves only the configured observation. Evidence can be precise while the sentence around it is still misleading, which is why limitations are first-class fields and human review still matters.

• It does not turn manual review into proof. Manual evidence stays unknown until it is attested separately.

• It does not provide non-repudiation. Proofspec is a claim-evidence system, not a certification authority. The local hash chain detects receipt modification but is not an externally signed transparency log.

• It observes one moment. HTTP and npm checks see public remote state when they run; file and Git checks see the local machine.

• It is not on npm. The unscoped npm name belongs to an unrelated project (see the warning above).

• Two rough edges in 0.1.0. With --strict, the exit code follows the strict gate, but the summary line still reports the default gate, so it can print PASS and exit with 1; scripts should read the exit code. --no-write skips the report files but still appends receipts to the local ledger.

Read the full security model, limitations, configuration reference, and project origin.

How this was built

Most of the code was written by AI coding agents under my direction. I wrote the specification, set the constraints, decided what to test, reviewed the result and rejected what did not hold. Release decisions and every claim in this README are mine.

The public history starts at the finished 0.1.0 code (two commits on 2026-07-17); the agent sessions behind it are not published. Later changes (October 2026: install path, npx guard, dependency floor, this README) carry a Co-Authored-By: Claude … trailer in the commit history. Proofspec reuses the verifiers and receipts of my package postcondition-mcp; the background is in ORIGINS.md.

Status

0.1.0 · GitHub release (2026-07-17), not on npm · experimental · single maintainer · no known external users · last verified 2026-10-08.

The configuration schema is an early public version; migrations will be documented before incompatible changes. Changes since 0.1.0 are listed under “Unreleased” in the changelog. Please report security issues through the private process in SECURITY.md.

License

MIT © 2026 Christian Bucher