Proofspec

Claims are cheap. Proofspec makes them executable.

Proofspec turns the important statements in a README, release, product page, or agent completion message 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.

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.

Why this 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.

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.

Related MCP server: stillos-notary-mcp

Quick start

Requires Node.js 20 or newer.

The v0.1.0 source release is available now. Until the npm registry publication is visible, install the smoke-tested release artifact directly from GitHub:

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

Or run the included example from a clone:

npm install
npm test
node dist/src/index.js check examples/proofspec.json

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.

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

The stdio server exposes:

• proofspec_validate

• proofspec_check

• proofspec_explain

• proofspec_render

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

• prompt audit-public-claims

TypeScript API

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 proofspec check proofspec.json

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

Trust boundary

Proofspec is a claim-evidence system, not a certification authority. A local hash chain detects receipt modification but is not an externally signed transparency log. Evidence can be precise while the prose around it is still misleading, which is why limitations are first-class fields and human review still matters.

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

Development

npm install
npm test
npm run test:coverage
npm run smoke:pack

MIT licensed. Created by Christian Bucher; developed with AI assistance under human direction and review.