agentic-proofkit

README

agentic-proofkit

Reusable CLI and JSON proof infrastructure for spec-to-proof workflows in software repositories.

agentic-proofkit helps repositories validate structured requirements, bind requirements to proof routes, plan selective checks, admit receipt-shaped evidence, render human views, and give coding agents bounded next-action packets without copying verifier logic between projects.

Current Repository State

Surface	State
Source repository	Declared in package metadata; provider visibility is a live GitHub fact
Current layer	Public-source workflow; release evidence is version-specific
Runtime implementation	Go CLI with npm and Python wrapper packaging
Package release	Scoped npm release channel configured; exact version and registry identity are owned by npm and GitHub Release artifacts
Public-source provenance	Claimed only for a version whose release assets, registry identity, and checksum manifests are artifact-closed
License	MIT

Install

The canonical registry identity is npm:

npm install --save-dev --save-exact @research-engineering/agentic-proofkit

Pre-1.0 releases may contain owner-declared breaking changes, so npm consumers must retain the exact saved version instead of replacing it with a version range.

The canonical local invocation resolves only the already-installed dependency:

npm exec --offline -- agentic-proofkit help

npm remains the release-authority toolchain because release proof records npm registry identity, dist.integrity, dist.shasum, npm pack, and root-only registry install evidence. A bare agentic-proofkit command is valid when the package manager, script runner, or activated environment has already placed the installed binary on PATH; it is not the canonical copy-and-paste route. Equivalent exact-tarball Bun execution has not been admitted, so this README does not claim a Bun execution route.

Python consumers use the Python package as a runner wrapper over the same Go CLI, not as a Python SDK. Python projects should still treat CLI/JSON records, exit codes, and package metadata as the public contract.

Supported binary targets are macOS 13 or later on arm64 or x64. Linux manylinux 2.17 or later is supported on arm64 or x64. Windows is unsupported. The Python runner requires Python 3.9 or later and wraps the same Go CLI; it is not a Python SDK.

After an exact Python package version is available from an admitted channel, use one complete package-manager chain:

python -m pip install agentic-proofkit==<version>
python -m agentic_proofkit help

or:

uv add --dev agentic-proofkit==<version>
uv run agentic-proofkit help

These conditional commands do not claim that any current version is available on PyPI.

Project Boundary

agentic-proofkit is intended to provide reusable proof-workflow mechanics for repositories that want explicit requirements, proof bindings, deterministic reports, and bounded guidance for coding agents.

Proofkit does not own a consuming repository's product requirements, native witness execution, receipt authenticity, proof freshness, merge admission, rollout, deployment, or production readiness.

How It Works

Proofkit has two related but separate loops:

• an authoring loop for turning observations into candidate invariants and repo-owned specifications;
• a proof loop for admitting those specifications, binding them to evidence, and producing derived views or bounded next actions.

The loops are separate because generated observations are not product truth. Only the consuming repository can promote a candidate invariant into an admitted requirement.

Proof Loop

flowchart TB
    subgraph Repo["Consumer repository authority"]
        Requirements["Requirements and invariants"]
        Bindings["Proof bindings and witness commands"]
        Execution["Native test and CI execution"]
        Decision["Owner decision"]
    end

    subgraph Proofkit["Proofkit reusable mechanics"]
        Admission["Admit and normalize JSON"]
        Graph["Build proof graph"]
        Planning["Plan selected checks"]
        Receipts["Admit receipt-shaped evidence"]
        Views["Render derived views"]
        Packets["Emit bounded agent packets"]
    end

    Requirements --> Admission
    Bindings --> Admission
    Admission --> Graph
    Graph --> Planning
    Planning --> Execution
    Execution --> Receipts
    Receipts --> Decision
    Graph --> Views
    Graph --> Packets
    Views --> Decision
    Packets --> Decision

The core invariant is separation of authority. The consuming repository owns what the product must do and which native checks prove it. Proofkit owns the reusable mechanics: admitting structured inputs, preserving provenance, checking proof-binding shape, planning bounded verification, rendering derived views, and returning agent-readable next-action packets.

The diagram keeps the rendering syntax intentionally simple for GitHub README compatibility. Requirements, bindings, witness commands, native execution, and final decisions stay in the consumer repository. Proofkit outputs are admitted reports, plans, views, receipts, or agent packets; they do not become product truth unless the consumer explicitly admits them.

Invariant Authoring Loop

For a repository with no specification, Proofkit can guide an agent through three explicit starting modes:

flowchart TB
    Start["Code, docs, tests, issues, and maintainer intent"] --> Mode["Choose trust mode"]
    Mode --> Fresh["Fresh authoring mode"]
    Mode --> Baseline["Code baseline mode"]
    Mode --> Audit["Code audit mode"]
    Fresh --> Contract["Owner-authored product contract"]
    Baseline --> Observations["Caller-owned capability observations"]
    Audit --> Observations
    Observations --> Seeds["Candidate invariants and requirement seeds"]
    Seeds --> Review["Owner review and promotion"]
    Review --> Specs["Repo-owned requirements.v1.json"]
    Contract --> Specs
    Specs --> Obligations["Proof obligations"]
    Obligations --> Evidence["Proof bindings and test inventory"]
    Evidence --> Admission["Proofkit admission and coverage"]

Mode	Use when	Result
Fresh authoring	No existing code or specification is accepted as product truth	Owner-authored behavior statements that remain candidates until admitted as repository requirements
Code baseline	Current behavior is accepted as the starting contract	Candidate requirements and bindings that preserve current behavior until owners review them
Code audit	Current behavior may be wrong or incomplete	Untrusted observations and questions that must be promoted by a repository owner before becoming requirements

In all three modes, generated records remain candidates until the consuming repository admits them as repo-owned requirements, proof bindings, and witness plans. Proofkit can structure and validate candidate packets, but it does not extract complete behavior from arbitrary source code, invent product policy, or make generated invariants authoritative by itself.

Start Here

Use the CLI help route before reading source:

npm exec --offline -- agentic-proofkit help
npm exec --offline -- agentic-proofkit adopt plan --mode fresh --repo-root .
npm exec --offline -- agentic-proofkit help adopt plan
npm exec --offline -- agentic-proofkit help repo-profile-admission
npm exec --offline -- agentic-proofkit repo-profile-admission --help

Command-specific help is derived from the private command descriptor table and does not read stdin. The full machine-readable command inventory remains proofkit/cli-contract.v2.json; the human route map is docs/proofkit-contract-map.md.

adopt plan is the read-only front door. It inventories only a fixed catalog of recognized files at the explicit repository root, validates all arguments before filesystem access, and returns candidate-authoring tasks. It does not infer a stack, parse arbitrary source semantics, generate requirements, write files, or execute evidence. --stack is an optional caller-selected hint and cannot change the selected trust mode.

Repository state	Minimal first route	Stop condition
Fresh repository with no specification	adopt plan --mode fresh --repo-root .	Stop before writing files or inventing requirement meaning
Current code is intentionally accepted as the initial baseline	adopt plan --mode code-baseline --repo-root .	The flag is a caller declaration, not evidence that the code is correct; stop before promoting candidate observations
Current code must be audited before it becomes a contract	adopt plan --mode audit-from-code --repo-root .	Stop at explicit observations, owner questions, and candidate-only records
Legacy repository has local proof infrastructure	migration-parity-admission, then migration-plan	Stop before deleting local proof owners without parity evidence
A change set needs bounded checks	changed-path-set, optional impact, then selective-gate-plan and selective-gate-evidence	Stop on unknown scope, missing routes, or stale receipts
An agent needs only one specification subtree	requirement-context-compose --repo-root . --input context-catalog.json, then requirement-context-slice	Stop before treating a bounded slice as complete repository truth
A human needs semantic navigation, comparison, or traceability	requirement-browser-server --view workspace --serve over an admitted workspace input	Browser output, annotations, diff, and graph remain derived and non-authoritative

JSON commands default to readable output. Agents can request the same JSON value with lower transport overhead by placing the process option before the command:

npm exec --offline -- agentic-proofkit --json-layout compact requirement-context-slice --input slice-input.json

First Valid Input

The following marker-bounded record is a complete minimal requirement-source input. Its example IDs, paths, owner, invariant, and non-claims are caller-replaceable examples, not Proofkit-owned product meaning.

npm exec --offline -- agentic-proofkit requirement-source-admission --input -

{
  "schemaVersion": 1,
  "sourceId": "example.requirements",
  "specPackagePath": "docs/specs/example",
  "overviewPath": "docs/specs/example/overview.md",
  "requirementsPath": "docs/specs/example/requirements.v1.json",
  "nonClaims": [
    "This example does not approve merge or release."
  ],
  "requirements": [
    {
      "requirementId": "REQ-EXAMPLE-001",
      "ownerId": "example.owner",
      "invariant": "The example owner must replace this sentence with an admitted product invariant.",
      "claimLevel": "blocking",
      "riskClass": "medium",
      "proofBindingRefs": [
        "proofkit/requirement-bindings.json"
      ],
      "nonClaimRefs": [],
      "nonClaims": [
        "This example does not execute or authenticate a native witness."
      ],
      "lifecycle": {
        "state": "active",
        "replacementRequirementIds": [],
        "evidenceRefs": []
      },
      "deferral": null,
      "updatePolicy": {
        "reviewOwnerId": "example.owner",
        "requiresImpactDeclaration": true,
        "requiresProofBindingReview": true
      }
    }
  ]
}

Use secret-scan only when the caller provides an explicit file inventory with content. It is a dedicated secret-like text detector for admitted inventory records; it does not traverse the repository, validate credential liveness, or replace provider secret scanning.

For TypeScript consumers that want a small wrapper instead of hand-written child-process code:

npm exec --offline -- agentic-proofkit json-report-cli-adapter-source --language typescript --format json

The generated adapter remains caller-owned after materialization. It must be reviewed, pinned to the installed package, and kept behind the same CLI/JSON contract; it does not become a separate public SDK or proof authority.

Need	Owner
Human orientation	This README
Adoption and release-channel model	ADOPTION.md
Vulnerability reporting boundary	SECURITY.md
Explicit boundary denials	NON_CLAIMS.md
LICENSE	MIT license

Non-Claims

This README is a human landing page. It is not a CLI contract, release proof, package publication claim, security audit, or consumer readiness claim. CLI and package behavior are owned by their source, tests, machine-readable contracts, and release evidence, not by this overview.