Proofborne

The coding agent that proves its work.

Proofborne is a local-first, vendor-neutral coding harness for power users. Its core primitive is a Task Contract backed by a runtime-generated Proof Graph. A model may claim that work is complete; Proofborne only reports verified when every required criterion has passing evidence or an explicit human waiver.

The product mission is Completion Integrity: make every completion claim scoped, falsifiable, bound to the state it observed, and portable enough to review offline. Read the versioned product vision and the decision on claim scopes and assurance.

Status: 0.2.0-alpha.1 release-candidate preparation is in progress. Public JSONL, auth, graph, and proof-bundle schemas are versioned; internal Rust APIs remain unstable until the next minor release.

Testing 0.2.0-alpha.1

The automated installer and proof gates replicate per-platform install, checksum, dead-candidate rejection, doctor, key-free demo, and uninstall flows on the exact candidate commit. The immutable v0.1.0 release passed its cross-platform candidate, nightly isolation, required live-provider, crates.io, and Proof Report gates. This alpha adds proof-carrying OAuth/coding-plan identity, account-aware routing, fail-closed credential transport, and read-only graph/memory UX.

What works in the first vertical slice

• one Rust binary on Windows, Linux, and macOS;
• live interactive terminal UI and machine-readable JSONL mode over one session engine;
• hash-chained event records, SQLite WAL persistence, and content-addressed artifacts;
• task contracts, evidence linking, completion gates, and provider-free semantic offline proof verification;
• policy presets and hash-precondition file edits;
• runtime-owned LSP definition, reference, and diagnostic queries plus 28-language structural AST search and hash-guarded AST rewrites on the current development branch;
• provenance-bound context records and read-only memory_search / memory_get tools with workspace-freshness, supersession, and secret-redaction boundaries on the current development branch;
• deterministic, provider-budgeted context compaction that preserves open obligations, unresolved counterevidence, workspace/authority/side-effect bindings, and fails closed on pinned-context overflow, with versioned crash-recovery receipts on the development branch;
• a versioned P2B Completion Integrity corpus with hidden-oracle repository tasks, missing and stale evidence, long compaction sessions, provenance-visible memory poisoning, fail-closed overflow, and receipt-bound crash recovery; every proof-on/off run publishes machine-readable oracle results, raw events, artifact digests, and offline-verifiable proof bundles;
• a deterministic, runtime-owned model router that filters local provider candidates by capabilities, context, credential availability, pinned cost/latency limits, and stable profile preference; every decision, exclusion, attempt, fallback, and session lock is committed by plan-bound events, evidence, and offline-verifiable receipts;
• provider-neutral OAuth authorization-code + PKCE login for configured coding-plan profiles, structured OS-keychain token lifecycle, account/scope-aware routing, automatic refresh, and provider-specific bearer/header shaping without persisting tokens, raw provider frames, or remote response handles in events or proof material on the development branch;
• versioned proof-carrying delegation and agent-graph contracts with exact criterion decomposition, strict child task/authority subsets, content-addressed leased inputs, isolated concurrent worker workspaces, propagated hierarchical budgets, independent reviewer/adversary gates, atomic sibling fan-in, conflict invalidation, durable recovery, and provider-free offline verification on the development branch;
• hierarchical AGENTS.md, progressive Agent Skills discovery, and brokered MCP tools/resources/prompts over stdio or HTTP;
• ACP v1 stdio sessions, prompt updates, cancellation, load/recovery, and close, including client-provided mcpServers over stdio and Streamable HTTP on the current development branch.

Quick start

cargo build --release
./target/release/proofborne init
./target/release/proofborne run --profile mock --task "Inspect this repository" --auto-contract --jsonl
./target/release/proofborne session list
./target/release/proofborne proof export <SESSION_ID> --output proof.zip
./target/release/proofborne proof verify proof.zip

Coding-plan profiles use the same provider chain as API-key profiles. Configure the provider's OAuth endpoints and public client metadata, then authenticate and inspect only secret-free lifecycle state:

./target/release/proofborne auth login --profile openai-codex
./target/release/proofborne auth status --profile openai-codex --json
./target/release/proofborne auth logout --profile openai-codex

Routing policy is local and optional. Defaults preserve explicit profile/fallback order without requiring prices or latency estimates. Credential-required profiles without a resolved credential remain explicit, excluded candidates, so an eligible fallback can still run; an all-ineligible plan blocks before provider execution. Operators can fail closed on unknown metadata and set hard preflight ceilings:

[routing]
required_capabilities = ["tools"]
min_context_tokens = 32768
max_estimated_cost_microusd = 250000
max_latency_ms = 30000
require_known_pricing = true
require_known_latency = true
required_scopes = ["models.read"]

[providers.primary.routing]
enabled = true
credential_required = true
context_tokens = 128000
expected_latency_ms = 15000

[providers.primary.routing.pricing]
inputMicrousdPerMillionTokens = 3000000
outputMicrousdPerMillionTokens = 15000000

Prices are immutable local micro-USD ceilings per one million tokens, not live provider quotes. Unknown or over-budget candidates are excluded before provider execution.

The mock provider is deliberately deterministic. A runtime-only auto-contract cannot prove a coding task and therefore ends blocked before mutation when no task-specific verifier can be constructed; it never returns task-scoped verified or exit code 0. Use a confirmed contract plus runtime verification for a proof-bearing task.

For a complete guarded edit with a failing-then-passing test, use examples/provable-edit. It demonstrates the actual sequence read → hash-precondition patch → runtime test → proof gate without an API key.

Current alpha boundary

This repository implements the end-to-end vertical slice and the public proof core. Same-session crash recovery pins the event cursor, exact model catalog and route plan, provider/model authority, step ceiling, verification plan, workspace state, side-effect watermark, compaction controls, and the latest receipts/history-prefix commitment. Untouched pending tool calls may continue, but ambiguous in-flight work, partial provider streams, and terminal failed routing receipts are never replayed; a changed catalog, capability set, authority, policy, or routing budget fails closed and requires a new run.

Delegated work is never an authority shortcut. A coordinator freezes the child contract, provider/model identity, allowed action classes, workspace lease, starting generation, and hard budget before execution. The child runs in a separate filesystem copy containing only leased paths. Only an independently authorized reviewer session with successful, path-matching read evidence can approve a handoff. Merge rechecks the exact persisted plan, handoff, and unused approval before touching the parent, rolls back partial writes, and invalidates the delegation if the parent generation or reviewed changes drift. P3B composes those lifecycles into a runtime-owned DAG. Every parent criterion has one worker owner and every worker has separate reviewer and adversary gates. Dependency-ready nodes execute in bounded waves; overlapping sibling write scopes are rejected before execution, the persisted graph deadline cancels in-flight nodes without resetting on recovery, approved fan-in is one generation-checked transaction, and every scheduler transition and typed receipt is hash-chained for recovery and proof export. Bind a versioned parent-independent template with proofborne graph plan --out <OUTSIDE>/plan.json, then use the Rust SessionEngine::run_agent_graph API or proofborne graph run --plan <OUTSIDE>/plan.json. Provider-neutral OAuth/coding-plan login is implemented in the current alpha; release attestation remains enforced by the candidate workflow. Docker uses a pinned image, an explicit workspace mount, and no network by default; requested Docker network access needs an interactive per-run approval. Additional read-only host mounts are deliberately rejected in v0.1. If Docker is required but unavailable or invalidly configured, the runtime fails closed; auto and host are explicitly labeled policy-enforced, not sandboxed.

ACP-provided MCP credentials remain ephemeral: environment and header values are added to the runtime redactor but are not written to ACP session metadata, events, JSONL, or proof bundles. The persisted, secret-free tool-authority hash binds recovery to the declared server descriptors and discovered tool definitions. A changed authority or an ambiguous in-flight network action blocks recovery; Proofborne does not replay that call. Client attachments require both proofborne acp --allow-client-mcp and an exact alias (or *) in policy.mcp_allow. ACP advertises modern HTTP support only when that operator gate is enabled and explicitly reports legacy SSE as unsupported.

The versioned conformance corpus captures adversarial completion, freshness, tampering, recovery, approval, fallback, and redaction expectations. Its structural validator and deterministic runtime-backed semantic gate run in CI. The development branch also runs scripts/validate_acp_mcp.py against the real ACP subprocess and Rust MCP fixture to check lifecycle, cancellation, secret redaction, JSON-RPC-only stdout, and no-replay recovery. These are internal conformance gates, not an external benchmark or a production-release claim.

Architecture, configuration, proof layout, compatibility, and the exact shipped/next boundary are documented under docs/. The staged crate and binary publication gates are described in docs/releasing.md.

Trust model

Proofborne v0.1 proves that captured evidence is internally consistent and that the declared completion gate was applied. It does not prove mathematical correctness, capture activity outside its tool boundary, or defend against a compromised host that can rewrite both the evidence and verifier. See THREAT_MODEL.md.

Proofborne does not currently claim mathematical correctness, remote attestation, complete sandboxing, or superiority over another harness. “Best”, “safest”, and “revolutionary” remain ambitions until reproducible comparisons support a narrower public statement.

Project principles

1. Runtime facts outrank model prose.
2. No hidden fallback after side effects.
3. Host policy is never marketed as a sandbox.
4. Secrets never belong in project configuration or proof exports.
5. Compatibility comes from open protocols, not proprietary harness coupling.

License

Licensed under either of

• Apache License, Version 2.0 (LICENSE-APACHE); or
• MIT License (LICENSE-MIT)

at your option.