# 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](docs/product-vision.md) and the decision on
[claim scopes and assurance](docs/adr/0003-claim-scopes-assurance-and-evidence-kernel.md).
> Status: `0.1.0` stable-candidate preparation is in progress. Public JSONL,
> graph, and proof-bundle schemas are versioned; internal Rust APIs remain
> unstable until the next minor release.
## Testing 0.1.0
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 owner-executed P3B graph run (scenario
S7, issue [#42](https://github.com/koopmannleon19977-cmyk/proofborne/issues/42))
passed against the published `v0.1.0-alpha.4` artifact. Remaining work is the
final candidate's release-gate run and publication.
## 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;
- 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
```console
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
```
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:
```toml
[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
[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`](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`.
Remote OAuth/coding-plan login and release signing remain tracked work. 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](tests/conformance/README.md) 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/`](docs/implementation-status.md). The staged
crate and binary publication gates are described in
[`docs/releasing.md`](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](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](LICENSE-APACHE)); or
- MIT License ([LICENSE-MIT](LICENSE-MIT))
at your option.