Truth Harness

Local-first verified math for AI agents.

Truth Harness is a verification-first mathematical workbench for humans, Claude, Codex, and other agentic tools.

The project goal is not to replace WolframAlpha by rebuilding every math engine. The goal is to build the missing verification engine around AI-assisted work: problem normalization, verifier routing, receipts, trust labels, claim ledgers, replay, disclosures, benchmarks, and reports. Every answer should be backed by a replayable local tool run, proof check, cited source, counterexample search, workspace snapshot, or an explicit uncertainty label. Claude, Codex, and other frontier models can still help reason, plan, and critique, but the app is local-first: project data and artifacts stay in the local workspace unless the user explicitly sends selected context to a hosted model or network service, and that selected context plus disclosure is recorded locally.

The long-term mission is open-source discovery infrastructure: help humans and agents investigate hard math, physics, materials, climate, biomedical, and engineering problems without turning model output into fake certainty. The workbench should make it easy to use the best available local solvers and, when the user chooses, the latest capable frontier models as outside critics while keeping the private workspace private.

The name is intentional: it describes the product as a local harness for routing claims through evidence, replay, and verification instead of letting AI output float around as vibes.

The public name is Truth Harness. The CLI command, package scope, schemas, Docker service, MCP tools, and local project store all use the truth-harness namespace. See docs/PARITY_LEDGER.md for the naming decision and parity gates against WolframAlpha, SageMath, Lean, JupyterLab, provenance tools, and scientific RAG.

OpenAI Build Week: Codex and GPT-5.6

Truth Harness was built through an extended Codex engineering workflow with GPT-5.6 used for high-reasoning implementation, architecture review, failure analysis, and demo rehearsal. Codex inspected and edited the TypeScript monorepo, exercised the local web interface, ran Docker-isolated verification, added regression tests, reviewed trust and security boundaries, and prepared the replayable Build Week evidence package.

The model is deliberately not the source of truth. Codex and GPT-5.6 can propose a claim, choose a candidate verifier route, critique a result, and explain the evidence. Deterministic local engines must perform the accepted computation or proof check before Truth Harness assigns a stronger trust label. In the submitted swept-AABB demo, exact rational arithmetic refutes the proposed claim and records the impact interval, backend, replay command, privacy boundary, and limitations in a local receipt. Model output by itself never counts as proof.

The submitted workflow demonstrates the intended division of responsibility:

1. Codex and GPT-5.6 translate a human problem into a bounded claim and verification plan.
2. Truth Harness routes that claim to a deterministic local verifier inside Docker.
3. The verifier returns checkable evidence, a conservative trust label, and a replay command.
4. Codex presents the evidence and limitations without upgrading its own reasoning into proof.

What Changed During Build Week

Truth Harness existed before OpenAI Build Week. The submission-period work is intentionally visible in the public main history:

• 1a24c5e prepared the repository for public review with launch-hygiene checks.
• a9376d1 added the isolated Build Week verification rehearsal.
• eb30ea9 patched dependency security issues and tightened Lean backend identity checks.
• bd06b03 hardened the Docker demo, exact swept-AABB evidence, replay, and report path.
• 1c7b413 added the submission gallery assets generated from the working demo.
• 50e8d64 documented the Codex and GPT-5.6 workflow and its trust boundary.

These commits were produced during the July 2026 submission period through the primary Codex build task identified by the /feedback session ID in the Devpost submission. They are evidence of the Build Week contribution, not evidence that any model output is mathematically true.

See docs/BUILD_WEEK_SUBMISSION.md and docs/BUILD_WEEK_DEMO_RUNBOOK.md for the submitted story and exact reproduction steps.

Why It Exists

AI is already good at writing plausible math. The hard part is knowing when the math is true.

Truth Harness turns math answers into receipts:

• Truth Harness owns the trust policy, verifier router, evidence graph, claim ledger, replay contracts, and agent-facing local workspace,
• exact computations use exact rational arithmetic or CAS adapters,
• exact arithmetic receipts include machine-readable step traces and deterministic audience-level explanations,
• false universal claims get counterexample search before explanation,
• formal proofs will only be labeled proved when a proof checker accepts them,
• every result carries a trust label, replay command, and privacy metadata.

The current MVP is local-first by default. Receipt metadata records local-only mode, networkAccess: none, local workspace data residency, external disclosure metadata when relevant, and an evidenceProfile summarizing backend ids, versions, inputs, outputs, replayability, proof-checker status, and limitations. Live code-run records are stricter about honesty: native host execution records networkAccess: unknown, while the Docker no-network profile can attest networkAccess: none only when the runtime measures the Truth Harness container marker, a container runtime marker, loopback-only networking, and no default route.

Docker-First Quickstart (Recommended)

For agent-facing work, demos, and anything that may execute code, prefer Docker first. The image keeps Node, Python, SymPy, Maxima, Z3, cvc5, and npm dependencies out of your host environment. Optional heavier engines such as SageMath and Lean are gated separately. The CLI and MCP compose runtimes disable network access; the web runtime publishes only to 127.0.0.1 so your browser can reach the local workbench.

Default verification for this repo:

npm run verify:default

That command runs the no-network Docker Maxima/Z3/cvc5 engine smoke and then the full build/test suite inside the compose service. If Docker Desktop is not running, it should fail clearly; use npm run verify:native only as a fallback and do not treat it as the public credibility path.

Highest-safety verification, with no repo bind mount during the checks:

docker --version
docker build --target verify -t truth-harness:verify .

This verification image runs the TypeScript build, test suite, launch demos, a concrete Maxima CAS agreement check, and concrete Z3 and cvc5 SMT-LIB checks inside the container image.

Day-to-day container workflow:

docker compose build
docker compose run --rm truth-harness npm run check:native
docker compose run --rm truth-harness npm run cli -- demo
npm run docker:demo
docker compose run --rm truth-harness npm run proof:launch:engines
docker compose run --rm truth-harness npm run cli -- workspace init --name "Local Math Lab"
docker compose run --rm truth-harness npm run cli -- bench run packages/benchmarks/suites/ai-failure-seed.json --write --fail-on-failures
docker compose run --rm truth-harness npm run cli -- bench run packages/benchmarks/suites/math-credibility-ladder.json --write --fail-on-failures
docker compose run --rm truth-harness npm run cli -- bench run packages/benchmarks/suites/professor-math-challenge.json --write --fail-on-failures
docker compose run --rm truth-harness npm run cli -- workspace credibility-pack . -- --require-docker-core
docker compose run --rm truth-harness npm run cli -- ask "symbolic simplify sin(x)^2 + cos(x)^2"
docker compose run --rm truth-harness npm run cli -- cas backends
docker compose run --rm truth-harness npm run cli -- engines readiness
docker compose run --rm truth-harness npm run cli -- cas check --operation simplify --expression "sin(x)^2 + cos(x)^2" --result 1 --write
docker compose run --rm sage-math
npm run docker:all-engines
docker compose run --rm truth-harness npm run cli -- smt backends
docker compose run --rm truth-harness npm run cli -- proof backends
npm run docker:engines
docker compose run --rm truth-harness npm run cli -- code sandbox-status --json
npm run docker:sandbox:write
npm run docker:lean-suite
npm run docker:theorem-template
npm run docker:web
docker compose run --rm -i mcp

The web workbench uses one canonical local URL: http://127.0.0.1:4180/. If the browser seems stale or you are unsure whether port 4180 is served by Docker or the host repo, run the read-only doctor:

npm run web:doctor

It reports the port owner, /api/status runtime identity, served app bundle version, and safe refresh commands without stopping Docker, killing a process, or rebuilding anything by itself.

See SECURITY.md and docs/DOCKER.md for the safety boundaries. Docker is the recommended baseline, but a compose dev container bind-mounts this repo and can still change files inside it. Code-run receipts report networkAccess: none only when the measured Docker no-network provider is active; otherwise they correctly stay at unknown.

Use npm run docker:demo for launch recording. It runs the 16-case demo with a stricter gate that fails unless the symbolic CAS cases earn real cross-checked labels and the SMT case earns smt-checked from the Docker-provisioned engine path. The plain npm run cli -- demo remains useful on machines where optional engines are missing; it will honestly show those cases as unverified instead of faking readiness.

Use npm run demo:math-ladder or npm run docker:math-ladder for the native-safe hard-math floor. The math credibility ladder reports named levels for exact arithmetic, universal refutation, physics units, bounded numerics, and honest checker boundaries, and saved benchmark-run records preserve those level summaries for reviewer packets and agent handoffs. Use npm run demo:professor-math or npm run docker:professor-math for the stricter 26-case professor challenge: exact algebra slips, bounded finite integer claims, dimensional checks, interval boundaries, and theorem-level refusals all have to earn the right conservative label. Use npm run demo:public-catalog or npm run docker:public-catalog to inspect the source-linked public math problem catalog, then npm run demo:public-probes or npm run docker:public-probes for the native-safe bounded-problem suite and npm run docker:public-symbolic for the Docker-backed symbolic CAS public suite. Use npm run demo:engine-math or npm run docker:engine-math for the first engine-math lane: the 33-case 2D collision verifier pack covering exact integer-coordinate AABB overlap, swept AABB, circle/circle, capsule/circle, circle/AABB, segment intersection, ray/circle, finite max-t ray/circle, ray/AABB, finite max-t ray/AABB, barycentric coordinates, and point-in-triangle predicates for game, simulation, robotics, and graphics-engine agents. Use truth-harness engines packs or npm run cli -- engines packs local-engine-geometry-2d -- --json when an agent needs to discover that pack, its backend ids, and its Docker replay gate before choosing a verifier route. The catalog JSON exposes a conservative summary.nextAction, and truth-harness bench catalog packages/benchmarks/catalog/public-math-problem-catalog.json --handoff renders that target as a Markdown handoff packet, so agents reopen the highest-value public math target instead of inventing random progress. The current public catalog covers Project Euler 1, 2, 6, 48, and 53 with source-linked metadata, exact certificates, and near-miss refutations, plus the sourced binomial square specialization and Pythagorean trig identity with Docker-backed SymPy/Maxima CAS agreement and near-miss refutations. The symbolic result is cross-checked, not proved, because CAS agreement is not a proof-checker-backed theorem. See docs/PUBLIC_MATH_JOURNEY.md, docs/PUBLIC_MATH_PROBLEM_CATALOG.md, docs/PUBLIC_ANSWER_WORKFLOW.md, and docs/ENGINE_MATH_LANE.md. Public answer packets live under docs/public-answers/ so any forum, classroom, or issue reply can cite the source, replay command, trust label, and limitation instead of linking to a vague AI chat. Use npm run demo:frontier-honesty or npm run docker:frontier-honesty for the hardest-problem honesty suite: famous open/theorem-scale prompts must stay unverified unless local proof evidence exists, while nearby supported claims still have to be verified or refuted. Use npm run demo:millennium-stress, npm run docker:millennium-stress, or npm run demo:millennium-catalog for the source-linked Millennium stress pack, which tracks all seven Clay problems as proof-boundary tests and treats Poincare as externally solved but not locally proved. See docs/MILLENNIUM_STRESS_TEST.md.

Use truth-harness engines validate docs/examples/engine-case-bundle.json for the external engine bridge: a Rust/game/simulation engine can export structured primitive outputs, and Truth Harness recomputes them locally before they are trusted. Use truth-harness engines verify or npm run docker:all-engines for the next engine-backed ladder. Engine verification reports levels for core Maxima/Z3 evidence, cvc5 solver diversity, Lean proof fixtures, SageMath breadth, and the strict all-engine reviewer gate. These levels pass only when concrete scoped evidence is minted; executable readiness probes do not count. Saved engine-run records now summarize their strongest passed engine level, and professor credibility packs plus release audits cite the strongest saved level so reviewers can see exactly which external-engine standard the workspace is relying on.

Native Quickstart

npm install
npm run build
python -m pip install sympy==1.14.0
npm run cli -- demo
npm run cli -- workspace init --name "Local Math Lab"
npm run workspace:status
npm run cli -- workspace repair
npm run cli -- research harness "Investigate deterministic math and physics verification for AI-generated robotics simulation code." --domain math --domain physics --domain code --plan-next
npm run cli -- validation plan "3 / 4 + 5 / 8" --domain math --write
npm run cli -- verify "3 / 4 + 5 / 8" --write
npm run cli -- validation attach <plan_id> <gate_id> --evidence route:<route_id>
npm run workspace:repair-artifacts:preview
npm run workspace:repair-artifacts
npm run workspace:clean
npm run workspace:validate
npm run workspace:events
npm run cli -- workspace credibility-pack .
npm run cli -- ask "compute 3 / 4 + 5 / 8" -- --out .truth-harness/receipts/fraction-sum.json
npm run cli -- ask "for all integers n, n^2+n+1 is even"
npm run cli -- ask "for all integers n, n^2+n is even"
npm run cli -- ask "for all integers n, n^2+n+1 is even" -- --out receipts/false-parity.json
npm run cli -- replay receipts/false-parity.json
npm run cli -- render receipts/false-parity.json markdown receipts/false-parity.md
npm run cli -- render receipts/false-parity.json html receipts/false-parity.html
npm run cli -- bench run packages/benchmarks/suites/foundations-seed.json
npm run cli -- bench run packages/benchmarks/suites/foundations-seed.json --write
npm run cli -- bench run packages/benchmarks/suites/ai-failure-seed.json
npm run cli -- bench run packages/benchmarks/suites/ai-failure-seed.json --write --fail-on-failures
npm run demo:math-ladder
npm run demo:professor-math
npm run demo:public-probes
npm run docker:public-probes
npm run cli -- bench run packages/benchmarks/suites/math-credibility-ladder.json --write --fail-on-failures
npm run cli -- bench run packages/benchmarks/suites/physics-seed.json
npm run cli -- bench run packages/benchmarks/suites/numeric-seed.json
npm run cli -- bench run packages/benchmarks/suites/symbolic-seed.json
npm run cli -- ask "dimension check force = mass * acceleration"
npm run cli -- ask "dimension check force = mass * velocity"
npm run cli -- ask "bound x^2 + 2*x + 1 for x in [0, 2]"
npm run cli -- ask "symbolic simplify sin(x)^2 + cos(x)^2"
npm run cli -- cas check --operation simplify --expression "sin(x)^2 + cos(x)^2" --result 1 --write
npm run cli -- cas list
npm run cli -- claim add "3 / 4 + 5 / 8 equals 11 / 8" --trust exact-computed --tag fractions --evidence receipt:.truth-harness/receipts/fraction-sum.json
npm run cli -- claim list --tag fractions
npm run cli -- claim show <claim_id>
npm run cli -- claim review <claim_id>
npm run cli -- visual create "Fraction number line" --source receipt:.truth-harness/receipts/fraction-sum.json --payload-format svg --payload-text "<svg xmlns=\"http://www.w3.org/2000/svg\" viewBox=\"0 0 320 180\"><text x=\"20\" y=\"40\">3/4 + 5/8 = 11/8</text></svg>"
npm run cli -- -- visual graph --renderer mermaid
npm run cli -- -- visual graph --renderer graphviz
npm run cli -- -- visual render <visual_id> --engine graphviz
npm run cli -- -- visual render <plot_visual_id> --engine plotly
npm run cli -- -- visual plot .truth-harness/receipts/fraction-sum.json --renderer plotly
npm run cli -- -- visual canvas
npm run cli -- visual list
npm run cli -- visual show <visual_id>
npm run cli -- proof backends
npm run cli -- proof project .
npm run cli -- proof project docs/examples/lean-theorem-template
npm run proof:theorem-template
npm run cli -- proof check docs/examples/trivial.lean
npm run cli -- proof check docs/examples/trivial.lean --write
npm run cli -- proof list
npm run cli -- proof visual <proof_check_id>
npm run engines:readiness
npm run cli -- engines verify
npm run engines:verify:all
npm run cli -- smt backends
npm run cli -- smt check docs/examples/constraints.smt2
npm run cli -- smt check docs/examples/constraints.smt2 -- --backend cvc5
npm run cli -- smt check docs/examples/constraints.smt2 --fail-on-unverified
npm run cli -- smt check docs/examples/constraints.smt2 --write
npm run cli -- smt solve --int x --constraint "x > 0" --constraint "x < 3"
npm run cli -- smt list
npm run cli -- check docs/examples/strict-claims.md
npm run cli -- source ingest docs
npm run cli -- source search "verified math agents"
npm run cli -- source cite "Truth Harness is built for verified math agents" --query "verified math agents"
npm run cli -- notebook log "Run a local notebook that checks a parity conjecture" --kind notebook --runner jupyter --command "jupyter nbconvert --execute notebooks/parity.ipynb" --notebook notebooks/parity.ipynb --code src/parity.py --output artifacts/parity-output.json --runtime python --runtime-version 3.12 --dependency sympy==1.14.0 --metric checked_cases=2 --limitation "Notebook output is provenance, not a proof-checker-backed result"
npm run cli -- notebook list
npm run cli -- code run "Run a tiny local code check" --command node --allow-executable node --arg -e --arg "console.log(6 * 7)" --code inline:node-eval --input prompt:6x7 --output stdout
npm run cli -- code list
npm run cli -- model-context prepare "Ask a frontier model to critique a selected proof plan" --service OpenAI --model frontier-reasoning-model --data "selected formal statement" --data "selected proof sketch" --section "Selected proof plan=Only critique this selected proof plan; local notes stay local." --approval "prompt:explicit-user-request"
npm run cli -- disclosure log "Ask a frontier model to critique a selected proof plan" --service OpenAI --model frontier-reasoning-model --data "selected formal statement" --data "selected proof sketch" --context "Only the formal statement and proof sketch are sent; local notes stay local." --approval "prompt:explicit-user-request"
npm run cli -- workspace validate
npm run audit:release
npm run audit:release:gate
npm run cli -- workspace ui-review . -- --pass "Browser reviewed for clipping, overflow, focus state, scroll behavior, and report readability" --write
npm run cli -- catalog rebuild
npm run cli -- catalog status
npm run cli -- catalog search "fractions exact-computed" --kind claims --trust exact-computed
npm run cli -- catalog search --ref .truth-harness/receipts/fraction.json --kind claims
npm run cli -- workspace snapshot
npm run cli -- workspace revision . --title "Checkpoint before agent handoff" --reason "Stable evidence state before the next proof blocker"
npm run cli -- workspace revisions
npm run cli -- workspace verify-revision <rev_id>

The current MVP is intentionally small and honest. It supports exact rational arithmetic, bounded finite multiple-sum computations, finite counterexample search, a narrow local modular parity checker, conservative rational interval bounds, dimensional analysis, a local SymPy symbolic adapter, constrained local Maxima/SageMath CAS check records for scoped symbolic equality, policy-gated direct local code-run records, local proof-backend readiness probes, local Lean proof artifact checks when Lean is installed, local Z3 and optional cvc5 SMT-LIB checks when those solvers are installed, first-class claim-ledger records with dependencies/supersession/tags/finalization gates, first-class proof-check and SMT-check records, receipt replay, Markdown/HTML receipt export, benchmark runs, first-class benchmark-run and benchmark-comparison records, and a local MCP server. The parity checker can emit an exact local certificate, but it is not labeled proved until an accepted proof-checking backend verifies the result. truth-harness engines is a status manifest; truth-harness engines verify runs concrete local evidence smokes where Maxima must earn cross-checked, Z3 must earn smt-checked, cvc5 must earn smt-checked when --require-cvc5 is requested, SageMath must earn cross-checked when --require-sage is requested, and Lean must earn proved when requested. Use --require-all-engines for a strict reviewer gate that requires Maxima, Z3, cvc5, Lean, and SageMath to each earn scoped evidence instead of merely appearing in a readiness manifest. Richer RAG adapters remain planned as modular packages.

The first web surface lives at apps/web. It is a local workbench shell, designed like a dense desktop research tool: sessions and claims on the left, receipt-first verification in the center, and trust labels, replay commands, math visuals, evidence lineage, activity logs, and limitations in the inspector. The browser calls localhost /api/receipt, /api/claims, /api/research-harness, /api/workspace-seed/hard-math, /api/research-map, /api/visuals, /api/events, /api/public-math-journey, /api/workspace-run-next, /api/workspace-pilot-loop, and /api/workspace-run-nexts endpoints backed by local Truth Harness packages; it does not call a hosted model or external service. The header journey tracker reads the same public math problem catalog as truth-harness bench catalog --journey, showing solved/tracked counts, trust outcomes, open verifier gaps, and the next source-needed target without treating the counter as evidence. Verified receipts can be recorded into the local claim ledger so exported reports cite stable claim IDs, durable workspace event ids, activity events, and local API request ids. In the UI, Visuals means number lines, concept maps, bubble maps, saved visual artifacts, and future domain visualizers; Lineage means the receipt/claim dependency graph. The Runbook tab can start a local hard-problem harness from the current prompt or receipt, seed a deterministic hard-math validation workspace, write the linked validation plan, preview the reviewer credibility pilot loop from source=credibility-actions, save the first dry-run run-next handoff, list recent saved handoffs, open one quickly for reading, and run explicit source-revision/source-snapshot verification before copying a resume/recovery command. The browser still has no execution rights; CLI/MCP gates remain the path for bounded local work. The Report tab also exports a professor-friendly teaching packet with learning goals, prerequisites, step prompts, misconception checks, activities, rubric, replay command, and trust-boundary language generated from the current local receipt. The same artifact is scriptable with truth-harness teach <receipt.json> --audience college, so instructors and agents can produce lesson handouts without opening the browser. Run it with npm run docker:web by default, or npm run web:serve only for trusted host-side UI iteration, then open http://127.0.0.1:4180.

The web inspector also calls localhost /api/status to show safety and verification-engine readiness. It reports the measured code-run sandbox boundary plus local Maxima, SageMath, Lean, Z3, and cvc5 availability probes. These probes are readiness checks only: they never mint cross-checked, smt-checked, or proved by themselves. Those labels still require a concrete replayable CAS agreement run, SMT solver run, or accepted Lean proof-check artifact. The Checks tab mirrors the strict local release gate through /api/release-audit, showing validation status, catalog freshness, required engine evidence with gate-by-gate reviewer meanings, saved strict engine-run posture, saved adversarial benchmark posture, saved math credibility ladder posture, saved report draft integrity, research-session continuity, review blockers, sandbox state, replayable commands, and next blocking actions without running Docker or external services from the browser.

The engine manifest also exposes the agent contract for future high-performance work: determinism class, primitive semantics, replay requirements, drift risks, and stable JSON diagnostics for each capability. truth-harness engines plan "<problem>" is the read-only preflight router: it classifies a problem, chooses the relevant verifier stack, compares the local engines needed for that claim, exposes open gates, and recommends the first durable evidence command without running engines or minting trust. The planner now recognizes future concurrent-systems and hardware/EDA routes, so Rust deadlock/data-race claims and HDL/RTL formal-verification claims point agents toward sandbox, SMT, proof, and planned model-check evidence instead of random progress; those lanes still mint no trust until concrete adapters, fixtures, schemas, Docker coverage, and replay artifacts exist. npm run engines:readiness is the conservative host-probe summary of what this installation can responsibly support today: built-in research-core labels, blocked professor-review labels, missing external engines, agent-autonomy safety gates, and planned-but-not-trusted adapters. npm run engines:readiness:saved is the reviewer view that can cite a saved passing Docker no-network sandbox measurement for the agent-autonomy gate while still keeping the current host probe separate. Readiness never mints evidence. truth-harness engines verify --json is the companion evidence report for agents: it records which concrete engine checks earned scoped labels and which gates failed closed. npm run engines:verify:all is the local strict reviewer shortcut for the full Maxima/Z3/cvc5/Lean/Sage gate. That is the bridge from today's exact math receipts to later Rust kernels, rigorous numerics, simulation records, hardware-verification records, and differential-fuzzing oracles without pretending stochastic output or AI-generated code is truth by itself.

The Docker image installs Maxima through Debian's ECL-backed maxima-sage package plus Z3 and cvc5 so the containerized web UI and CLI can show real CAS/SMT readiness without changing the host machine. npm run docker:proof uses proof:launch:engines, which runs the standard launch proof suite, requires a concrete Maxima CAS agreement for sin(x)^2 + cos(x)^2 = 1, and then requires docs/examples/constraints.smt2 to return a concrete smt-checked result through Z3. The verify image also requires a concrete cvc5 SMT evidence smoke through the Docker-core engine script. npm run docker:engines is the smaller engine evidence smoke: it builds the dev image, then runs truth-harness engines verify --require-maxima --require-z3 --require-cvc5 inside an image-pure no-network compose service so stale bind-mounted dependency volumes cannot affect the result. Full SageMath is intentionally kept out of the default dev image because it is large; use docker compose run --rm sage-math or npm run docker:sage when a reviewer wants the heavier pinned Sage CAS gate. Lean is also separate; configure TRUTH_HARNESS_LEAN, or use the lean-proof Docker target/service for the pinned suite. npm run docker:lean-suite builds an image with Lean leanprover/lean4:v4.12.0, then checks docs/examples/lean-fixture, the reusable docs/examples/lean-theorem-template, and the route-scoped proof-repair fixture with no runtime network; npm run docker:proof-repair runs only the repair fixture and exits non-zero unless that scoped proof obligation closes. npm run docker:mathlib-template:write is the heavier opt-in mathlib gate: it requires a reviewed lake-manifest.json, resolves/caches mathlib during image build, and writes the proof-check artifact from a no-runtime-network compose service. docker compose run --rm lean-proof npm run cli -- engines verify --require-lean runs the static Lean fixture through the engine evidence report. npm run docker:all-engines is the intentionally heavy strict reviewer image that combines the SageMath base with pinned Lean and requires Maxima, Z3, cvc5, Lean, and SageMath to each earn scoped fixture evidence with no runtime network. npm run docker:all-engines:write writes that strict all-engine run into .truth-harness/engine-runs for release-audit and credibility-pack citation. npm run docker:professor writes the practical no-network reviewer packet with Maxima/Z3/cvc5/Lean, the strict Lean proof-repair gate, and exact/symbolic/SMT hard-math closure reports before generating the credibility pack and portable reviewer bundle; npm run docker:professor:all writes the stricter packet from the all-engine image so SageMath and the same Lean repair gate are part of the same credibility pack and portable reviewer bundle. Use npm run reviewer:status for the local reviewer audit plus Docker storage posture, npm run docker:storage for read-only Docker disk accounting and scoped cleanup recommendations, and npm run docker:cleanup for preview-only cleanup commands such as heavy-images, dev-image, and build-cache pruning. See docs/LEAN_PROOF_LANE.md for the Lean/Lake/mathlib path and docs/DOCKER_REVIEWER_FLOW.md for Docker reviewer storage and cleanup.

On Windows during UI iteration, run npm run web:doctor first when the browser appears stale or port ownership is unclear. It is read-only and tells you whether 4180 is owned by Docker, local Node, or another process, whether the API exposes current runtime identity, and which refresh command is safest. Prefer npm run web:restart only when the doctor shows the host Node runtime owns the port or no listener is present. web:restart stops the Node listener on port 4180, starts the web server again in the background, and keeps the browser URL stable; it intentionally refuses to kill Docker-owned ports. Static web edits usually need only a browser reload; server/API edits need either npm run web:restart for host web or npm run docker:web for Docker web. Before recording or sharing the UI, run npm run web:smoke for the focused web contract and localhost API smoke tests, then do a browser pass for clipping, scroll behavior, focus states, and report readability. Record that pass with npm run workspace:ui-review:pass, or use the underlying truth-harness workspace ui-review . --pass "Browser reviewed for clipping, overflow, focus state, scroll behavior, and report readability" --write; MCP agents can write and list the same local finding through truth_harness_workspace_ui_review and truth_harness_workspace_ui_review_list. The saved truth-harness.web-ui-review.v0 finding is for release-audit citation without pretending UI polish proves the math.

Local workspace commands create a private .truth-harness/ project store for receipts, claim ledger records, visual artifacts, artifacts, indexes, append-only event logs, findings, research sessions, expert reviews, validation plans, literature records, notebook-run records, code-run records, invention logs, simulation logs, experiment logs, evidence audits, model-context packets, disclosure logs, encrypted vault envelopes, provenance snapshots, workspace revisions, patent claim charts, CAS-check records, proof-check records, SMT-check records, and benchmark run/comparison records. The directory is git-ignored by default. workspace status reports missing private directories and manifest defaults added by newer releases; workspace repair creates missing directories and persists newly added defaults without leaving the local project. workspace repair-artifacts repairs legacy local JSON metadata, such as older route manifest contract fields or prompt-derived visual refs, without upgrading trust labels. Use npm run workspace:repair-artifacts:preview before applying artifact repair. workspace revision . --title "Checkpoint before agent handoff" --reason "Stable evidence state before the next proof blocker" writes an immutable truth-harness.workspace-revision.v0 manifest anchored to a fresh source snapshot, local artifact hashes, parent revision refs, session refs, validation-plan refs, and claim refs; workspace verify-revision <rev_id> checks the source snapshot file and workspace drift before an autonomous agent resumes. Revision history growth is ignored during verification, but changed or missing evidence artifacts fail closed. workspace archive copies selected manifest-known directories into .truth-harness/archives/<archive-id>/ with per-file SHA-256 hashes before cleanup; workspace archives lists good and damaged local archives; workspace restore-archive is dry-run by default, verifies archive hashes, reports overwrite conflicts, and requires --confirm-restore plus --overwrite before replacing changed live files. workspace clean is dry-run by default and only targets manifest-known directories under .truth-harness; pass --confirm-delete plus explicit --target scratch|generated|evidence|all|<directory> when you intentionally want to clear local data. npm run workspace:clean is the safe cleanup preview shortcut.

Hard-problem sessions should start with truth-harness research harness "<objective>" --plan-next, or MCP truth_harness_research_harness_start with planNext: true. This writes a normal private research-session artifact preloaded with verification-first tasks: narrow claims, validation plans, engine readiness, local verifier routing, model-context disclosure, checkpoints, domain-specific guardrails, and reviewer packets. It also writes a linked initial validation plan by default, with the session cited as the owner of the evidence-gate runbook and the session checkpointed back to the plan; use --no-validation-plan or MCP createValidationPlan: false only when a custom gate plan already exists. --plan-next / planNext: true immediately saves the first dry-run workspace run-next packet under .truth-harness/findings/, including a source workspace revision anchored to a source snapshot, so a human or autonomous agent can resume from a concrete proof/evidence blocker instead of stale chat memory. truth-harness workspace run-next and MCP truth_harness_workspace_run_next prioritize open gates from those linked validation plans before generic session tasks, so resumed agents attack proof, evidence, and replay blockers before inventing unrelated progress. If a linked research session already contains a candidate proof/SMT/CAS/route/source artifact for an open gate, the review item uses the concrete truth-harness validation attach ... --evidence kind:ref command as the next action instead of asking the agent to rediscover the evidence. If a blocked claim has an equivalent ready verifier route, workspace review emits a concrete truth-harness claim add ... --supersedes <claim> --evidence route:<route> action so run-next --execute-local can write the superseding claim through core APIs without shell execution. When run-next --execute-local writes verifier-route evidence, writes a direct proof/SMT/CAS artifact, executes a concrete validation attach command for a linked proof gate, or writes a superseding claim from ready route evidence, the plan is updated conservatively: exact, cross-checked, SMT-checked, or proved evidence can satisfy the gate only when its machine-checkable scope matches the validation claim; refuting evidence blocks it; unverified or unscoped evidence is attached as in-progress work with next checks. If the review item names a research session, direct proof/SMT/CAS runs and concrete validation attachments are also checkpointed back to that session so autonomous agents can resume from the local evidence trail instead of chat memory. It is a runbook for humans and agents, not proof that the objective is true.

Workspace validation commands write no files; they scan local evidence artifacts and return truth-harness.workspace-validation.v0 reports. Validation checks the root project.json manifest against a private-by-default schema, then checks receipt JSON deeply, including local-first privacy metadata, backend-aware trust boundaries, and forged proved labels. Other known workspace JSON records are checked against their checked-in JSON Schema contracts, artifact ids, local evidence refs, and trust-boundary policies before humans or agents rely on the workspace.

Release audit commands compose the readiness checks into one local professor/public-review gate. npm run audit:release reports workspace status, validation, catalog freshness, engine evidence, saved engine-run posture, saved reviewer-bundle verification, saved ai-failure-seed benchmark posture, saved math-credibility-ladder posture, saved professor-math-challenge posture, review queue blockers, code-run sandbox status, web UI launch-review status, and a conservative frontier-readiness ladder without starting Docker or executing arbitrary code. The frontier ladder answers the "how close are we?" question in machine-readable terms: the strongest honest current claim can be credible-verification-harness or bounded-hard-math-harness, while frontierDiscoveryReadiness remains not-ready and canClaimWorldHardestProblems remains false until real proof/search benchmarks and external review exist. Low-priority passive route obligations stay on their source route artifacts as "do not overclaim" boundaries, but they are omitted from the executable review queue and surfaced as a warning count instead of next-action busywork. If the host cannot launch Maxima, Z3, cvc5, or Lean but a saved no-network Docker professor run already covers those capabilities, the audit treats that durable engine-run record as the review evidence and keeps the host probe gap non-blocking. The audit also inspects docs/examples/lean-theorem-template as lean-theorem-template; it passes only when the reusable core-Lean scaffold has a pinned toolchain, declaration targets, a complete local scan, and zero proof-safety blockers. That check is readiness only, not proof. The mathlib scaffold remains a formal-theorem frontier blocker until docs/examples/lean-mathlib-template/lake-manifest.json is reviewed and npm run docker:mathlib-template:write produces no-runtime-network proof evidence. The audit separately inspects the saved docs/examples/lean-repair-fixture workspace as lean-proof-repair-gate; it passes only when an accepted scoped Lean proof-check record closes the matching verifier-route obligation, otherwise it reports npm run docker:proof-repair as the refresh command. A saved cver_... reviewer-bundle verification must pass copied-file integrity, manifest-digest verification, and source-workspace drift checks before the release audit treats the portable reviewer packet as clean. If the Windows host cannot measure a code-run sandbox but npm run docker:sandbox:write has saved a passing no-network container measurement, release audit cites that durable truth-harness.sandbox-run.v0 finding while still requiring native host code-run records to stay at networkAccess: unknown. If a saved truth-harness.web-ui-review.v0 record exists, release audit cites the latest browser-reviewed target, viewport, checklist, and optional screenshot path; a warning or failed UI review remains a launch warning. npm run audit:release:gate is the strict failing gate: it requires Maxima, Z3, cvc5, Lean, and SageMath evidence gates, a saved strict engine-run record, the saved adversarial benchmark, the saved math credibility ladder, the saved professor math challenge, and a measured or saved code-run sandbox boundary. If that strict gate is blocked, the result is intentional: the workbench is refusing to pretend it is release-ready.

Catalog commands create and query a rebuildable local SQLite index at .truth-harness/indexes/catalog.db. truth-harness catalog rebuild scans canonical workspace JSON artifacts through the existing validation/parsing layer, then writes typed artifact, claim, route, tag, reference, and FTS rows for fast local search. truth-harness catalog status reports missing, stale, corrupt, or readable cache state and performs a lightweight file freshness check so new, changed, or missing JSON artifacts are visible before agents rely on search completeness. Claim, route, route-obligation, web receipt, proof-check, SMT-check, CAS-check, visual, workspace-review, credibility-pack, benchmark, notebook-run, code-run, literature, disclosure, invention, claim-chart, simulation, experiment, audit, expert-review, model-context, validation-plan, research-session, vault, and workspace-snapshot writers incrementally upsert their own catalog rows when a readable catalog exists; if an incremental update cannot be applied, the catalog is marked stale and truth-harness catalog search refuses it until rebuild. Those same writer hooks append local artifact-written lines under .truth-harness/events/YYYY-MM-DD.jsonl with workspace path, kind, artifact id, byte count, and SHA-256 so agents and humans can reconstruct write order without treating the event tail as proof. Use truth-harness workspace events . --limit 50, MCP truth_harness_workspace_events, or local web /api/events?limit=50 to inspect that local tail. Agents can use the same local-only cache through MCP tools truth_harness_catalog_status, truth_harness_catalog_rebuild, and truth_harness_catalog_search; the local web UI exposes the same cache through /api/catalog/status, /api/catalog/rebuild, /api/catalog/search, /api/events, the sidebar catalog panel, and the activity log. The catalog and event log are control-plane state only: they can be deleted or rebuilt from canonical artifacts where applicable, never satisfy proof obligations, never upgrade trust labels, and never replace the JSON receipts, claims, routes, proofs, SMT checks, CAS checks, visuals, or other canonical evidence files.

Catalog search rows also expose bounded local artifact refs when a matching artifact cites workspace files, including SHA-256-backed citations for present files. That lets agents jump from search hits to the receipts, reports, visuals, or sidecars that support the result without treating search itself as evidence. Use truth-harness catalog search --ref .truth-harness/receipts/result.json or MCP/local web catalog search with ref to reverse the question and find every indexed artifact that cites a receipt, report, proof, visual, or other local reference. In the web UI, artifact previews and artifact-ref controls expose the same path as Cited by so a researcher can inspect downstream reports, claims, snapshots, and reviewer packets before changing or relying on an artifact. Workspace run-next handoffs turn those reverse refs into a bounded revalidationQueue when possible, such as a downstream claim review command for a claim that cites the selected evidence.

Canonical workspace writers use same-directory temp files plus atomic rename, so an interrupted process should leave either the previous complete artifact or the new complete artifact. Read-modify-write paths that are likely to be touched by parallel agents, including research-session updates and the local corpus index, use per-workspace advisory locks under .truth-harness/indexes/locks/. The lock files and event logs are cache/control-plane state, not evidence, and snapshots exclude them.

Workspace graph commands write no files; they scan the same local artifact set and return a truth-harness.workspace-graph.v0 provenance map. truth-harness workspace graph and MCP truth_harness_workspace_graph expose nodes for local artifacts, edges for evidence refs, visual/source refs, task evidence, checkpoints, claim dependencies, supersession, snapshots, and selected-context refs, plus explicit missing-reference nodes when links are broken. This is the backend data model for lineage views, visual maps, report figures, and agent planning; it is not proof by itself.

Visual artifact commands write truth-harness.visual-artifact.v0 records into .truth-harness/visuals/. A visual artifact stores the renderer (truth-harness-native, Plotly, Graphviz, Mermaid, tldraw, Manim, Sage, Matplotlib, or an external-file pointer), payload format, source refs, replay command, exact data table when available, privacy metadata, and a trust boundary that says the visual is an evidence view, not a proof or trust-label upgrade. Use truth-harness visual create, truth-harness visual list, and truth-harness visual show when an engine or agent produces a plot, proof tree, lineage graph, concept map, simulation view, teaching animation, notebook output, or report figure that should be cited and reopened later. Adapter commands now generate first-class visuals from evidence: truth-harness visual graph --renderer mermaid|graphviz projects the local workspace graph, truth-harness visual plot <receipt.json> --renderer plotly|matplotlib|sage writes renderer-ready plot specs from receipts, and truth-harness visual canvas writes an editable tldraw-style research canvas seed from the workspace graph. truth-harness visual render <visual_id> --engine graphviz takes a saved DOT renderer source, screens it for external references, calls local Graphviz dot without a shell, sanitizes the SVG, and writes a second rendered visual artifact linked back to the source visual. truth-harness visual render <plot_visual_id> --engine plotly renders saved Plotly JSON through Truth Harness' constrained local SVG renderer, preserving the Plotly JSON as the authoritative renderer source. Agents can use the same surface through MCP tools truth_harness_visual_graph, truth_harness_visual_plot, truth_harness_visual_canvas, truth_harness_visual_list, truth_harness_visual_show, and truth_harness_visual_render; the local web dashboard exposes adapter parity through /api/visuals/graph, /api/visuals/plot, /api/visuals/canvas, and /api/visuals/render, with a Make figure action that writes a Plotly JSON source visual from the current receipt, renders a linked SVG figure, and opens the report-ready rendered artifact while preserving the source replay chain. Report exports cite the selected or latest matching figure artifact with its visual id, source refs, replay command, and trust boundary so paper drafts can reference visual evidence without implying the figure proves the claim. When calling these through the npm wrapper on Windows, use npm run cli -- -- visual ... so CLI flags reach Truth Harness. truth-harness proof visual <proof_check_id> turns a saved Lean proof-check record into a local proof-tree visual artifact while keeping the proof-check JSON authoritative. The web Visuals tab now saves live canvases into this ledger and reopens adapter payloads (graph-json, plotly-json, and canvas-json) as local SVG previews instead of placeholder cards.

Workspace review commands are the local handoff layer for agents. truth-harness workspace review and MCP truth_harness_workspace_review read saved verifier routes, claim-ledger records, saved report drafts, and active research sessions, then return an ordered work queue with critical/high/medium/low priorities, source refs, exact follow-up commands, privacy metadata, and a Markdown packet. Use --max-routes, --max-claims, --max-sessions, and --max-reports or the MCP maxRoutes/maxClaims/maxSessions/maxReports inputs when an agent needs a bounded next-action packet instead of broad chat-memory spelunking. Saved report drafts enter the queue as review artifacts, not proof; if a Markdown draft no longer matches its JSON sidecar hash, the queue marks it high-priority before sharing. Route obligations only become executable when they name a concrete local artifact; if an independent-SMT route has one concrete SMT-LIB source already recorded, review can derive the sibling backend command such as truth-harness smt check docs/examples/constraints.smt2 --backend cvc5 --write. Proof/CAS/SMT placeholders that can only open or inspect a route stay on the route artifact and are summarized as passive omitted obligations, so the main queue remains a list of work an agent can actually advance. Add --write or MCP write: true to save paired JSON/Markdown handoff packets into .truth-harness/findings/, where workspace snapshots can hash and cite the exact queue an agent acted on. truth-harness workspace reviews, truth-harness workspace show-review <wrev_id>, MCP truth_harness_workspace_review_list, and MCP truth_harness_workspace_review_show reopen those packets later so long-running Claude/Codex sessions can resume from a durable queue instead of a stale chat summary.

Each workspace review now includes an autonomy contract for agent loops. The contract says whether the current workspace is idle, safe for a local verifier loop, or human-review gated; names the next exact local command; limits the suggested batch size; lists allowed local actions, blocked actions, stop conditions, required artifacts, and human-review boundaries. It can authorize local work, but it cannot certify truth: trust labels still move only when replayable evidence satisfies explicit gates.

Professor credibility packs are the human-review counterpart to agent handoffs. truth-harness workspace credibility-pack . writes a truth-harness.credibility-pack.v0 JSON record plus Markdown into .truth-harness/findings/. The packet includes workspace validation status, an embedded artifact-hash snapshot, concrete engines verify results, the saved engine-run ledger with the strongest passed engine ladder level, the saved ai-failure-seed adversarial benchmark ledger, the saved math-credibility-ladder hard-math ledger, the saved professor-math-challenge reviewer exam ledger, saved hard-math closure reports for exact, symbolic CAS, and SMT run-next loops, saved report draft readiness, Lean proof-safety blocker counts, top open route/claim obligations, a structured reviewer action plan with close targets, exact reviewer commands, and blocking warnings. Reviewer commands now include npm run docker:proof-repair, the strict no-network Lean repair gate that must preserve a rejected attempt, produce a run-next repair handoff, accept the repaired proof, and close only the scoped route obligation. Benchmark reviewer-contract actions can also use truth-harness review log ... so run-next --source credibility-actions --execute-local writes a durable expert-review request record through core APIs instead of handing the agent a shell string. truth-harness workspace credibility-actions . --json exposes that unresolved reviewer queue directly for agents, CI, or a professor who wants the next closure command without scraping Markdown; truth-harness workspace run-next . --source credibility-actions --execute-local can advance one supported local reviewer action through core APIs without shell execution. Add --require-docker-core when a packet should require Docker-provisioned Maxima, Z3, and cvc5 evidence, --require-all-concrete when it should also require the Lean proof fixture, or --require-all-engines when the packet must require Maxima, Z3, cvc5, Lean, and SageMath. A pack marked ready-for-review now also requires all three saved benchmark ledgers to exist and pass, the Docker hard-math closure smokes to have passed for exact arithmetic, symbolic CAS, and SMT gates, every saved report draft Markdown file to match its JSON sidecar hash, and the inspected Lean proof-safety scan to contain no blocking markers; it means the local workspace is coherent enough for external review, not that every claim is proved. truth-harness workspace credibility-bundle . turns the same review state into a portable directory with copied canonical artifacts, a digest-stamped manifest, the pack JSON/Markdown, and hash verification; truth-harness workspace verify-credibility-bundle <bundle-id> checks copied-file integrity, manifest metadata integrity, and source workspace drift as separate facts. MCP agents can call the same local workflow through truth_harness_workspace_credibility_actions, truth_harness_workspace_run_next, truth_harness_workspace_credibility_bundle, and truth_harness_workspace_credibility_bundle_verify. See docs/CREDIBILITY_PACK.md.

When host subprocess launches are blocked by an OS policy or agent sandbox, credibility actions now say so explicitly and route Maxima/Z3/cvc5 to npm run docker:engines, Lean to the pinned lean-proof compose service, SageMath to npm run docker:sage, and strict all-engine review to npm run docker:all-engines. Reviewer command sets also expose npm run docker:proof-repair for the proof-repair handoff gate. Those commands do not fake trust; they give reviewers a no-network place where the engines and repair loop must earn their scoped evidence.

truth-harness workspace run-next and MCP truth_harness_workspace_run_next consume that autonomy contract. By default they return a dry-run, local-only plan with the next queue item, stop conditions, and networkAccess: none. Each plan includes a machine-readable rationale object naming the selected target, source queue item, candidate evidence ref when present, execution boundary, first stop condition, and first warning; the CLI, web Run tab, Markdown handoff, and MCP JSON all use the same data. When local artifacts are named, run-next exposes hash-backed artifactRefs and, when the catalog is fresh, impactRefs listing indexed downstream artifacts that cite those refs; agents should inspect those dependencies before mutating, superseding, or relying on an artifact. It also derives a revalidationQueue from those impact refs when a concrete local review action exists, such as truth-harness claim review <claim_id> --json for a dependent claim. Impact refs and revalidation entries are dependency navigation only and never close gates or upgrade trust. When the selected item contains a scoped verifier command, the plan also embeds an enginePlan routing contract: problem classification, recommended first durable command, verifier stack, evidence requirements, blocked stronger engines, and trust-boundary warnings. This prevents agents from guessing the verifier ladder when they reopen a hard-problem workspace, while preserving the boundary that only concrete receipts/proof/SMT/CAS/source artifacts can move trust. When no open item exists, the plan stays conservatively blocked with execution.kind: "no-open-item", but now includes idleNextActions for the next local move. If a saved pilot-loop transcript points at a real saved run-next handoff, continue-latest-pilot-loop is listed first so agents resume the recorded queue before starting duplicate work; otherwise the idle menu offers starting a validation-backed research harness, refreshing the Docker professor reviewer rehearsal, refreshing the professor credibility packet from saved evidence, or refreshing the strict release audit. The Docker professor action is intentionally marked as human-input-required because it starts npm/Docker; run-next recommends it but does not execute it. The local web API exposes the same safe planning surface at /api/workspace-run-next, but keeps it dry-run only so browser-driven workflows can show the next agent action without gaining execution rights. Add CLI --write or MCP write: true to persist the exact run-next plan as JSON/Markdown under .truth-harness/findings/ before handing work to an agent; the packet records intent, dry-run/execution status, stop conditions, trust-boundary warnings, dependency impact, downstream revalidation tasks, and a source workspace revision anchored to a source snapshot created immediately before the packet was written. truth-harness workspace run-nexts, truth-harness workspace show-run-next <wrn_id>, MCP truth_harness_workspace_run_next_list, MCP truth_harness_workspace_run_next_show, web /api/workspace-run-nexts, and web /api/workspace-run-nexts/<wrn_id> reopen those persisted intent packets so long-running agents can resume from recorded local plans instead of stale chat summaries. List summaries include the rationale target, source, candidate evidence ref, execution boundary, engine-plan status/classification when present, artifact refs, impact refs, revalidation queue, source revision ref, source snapshot ref, and resumeDecision so agents can triage many saved packets before loading a full plan. Use truth-harness workspace run-nexts --verify-snapshots, MCP verifySnapshots: true, or the web Runbook tab's Verify drift action to label saved handoffs as verified, drifted, missing, or not-recorded before acting; revision-backed packets verify the source revision first, then expose source snapshot drift detail for compatibility. Verified list summaries can mark resumeDecision.safeToResume: true, while drifted or unchecked summaries return a recovery command. Use truth-harness workspace show-run-next <wrn_id> --verify-snapshot, MCP truth_harness_workspace_run_next_show with verifySnapshot: true, or the web handoff Open action to inspect one exact packet and its drift status before execution. Agents should only resume the saved selected command when resumeDecision.safeToResume is true; otherwise they should run the provided recovery command, usually a fresh workspace run-next against the current workspace. The check ignores only the expected handoff JSON/Markdown files and revision-history manifests created after the source snapshot, and still flags real workspace drift. Add CLI --execute-local or MCP executeLocal: true only when an agent is allowed to perform one bounded step: the shared core planner parses the queued truth-harness ... command, rejects shell metacharacters/placeholders, and calls supported core APIs in-process for claim reviews, route/session/report reads, proof checks, SMT checks, CAS checks, concrete validation attach operations, review log expert-review requests, and claim add actions that cite ready route evidence. Proof, SMT, CAS, and attached validation evidence are applied to a linked validation gate only when the queue item names the same plan and gate; claim-add execution must supersede the exact claim named by the review item when closing a blocked claim. It never delegates the command string to a shell, and any trust upgrade still requires the produced or attached artifact to satisfy the matching validation gate, verifier route, or claim gate. For npm JSON output, use npm run cli -- workspace run-next . -- --json or call the built CLI directly with node apps/cli/dist/index.js workspace run-next . --json, because npm consumes some flags such as --json.

For reviewer-grade idle workspaces, idleNextActions now exposes npm run docker:professor:all as the strict all-engine professor rehearsal alongside the lighter npm run docker:professor path. Both are human-input-required because they start Docker through npm; run-next can recommend them, persist the intent packet, and cite later evidence, but it will not execute them automatically.

For large workspaces, pass --limit <count> to truth-harness workspace run-nexts or limit to MCP/web run-next list calls. The limit is applied before expensive source-revision/source-snapshot verification, so agents can verify the newest handoffs for triage without hashing the entire findings history.

Use truth-harness workspace release-audit . --summary-json, truth-harness workspace credibility-pack . --dry-run --summary-json, MCP truth_harness_workspace_release_audit_summary, or MCP truth_harness_workspace_credibility_summary for compact readiness JSON that omits embedded snapshots and Markdown bodies; keep full --json for archival/auditor packets. Use truth-harness workspace resume-index ., MCP truth_harness_workspace_resume_index, or the local web /api/workspace-resume-index endpoint when an autonomous agent reopens a project and needs one ranked local queue instead of guessing from chat memory. The resume index combines source-verified saved run-next handoffs, current workspace review blockers, saved pilot-loop transcripts, and blocked engine-readiness gates into a read-only, local-only plan. It ranks safe saved handoffs first, reports the evidence required to close each item, and never executes commands or upgrades trust by itself. The Runbook tab shows the same queue so humans and browser-driving agents can inspect the highest-value proof blocker before taking action. Read-only inspection tasks are deliberately demoted below stale saved handoffs and concrete verifier work, and repeated stale handoffs are compacted, so autonomous agents do not burn cycles reopening context when a proof, SMT, CAS, route, or refresh blocker is available. Blocked engine-readiness entries lead with concrete Docker recovery commands such as npm run docker:professor, npm run docker:professor:all, or npm run docker:sandbox:write before lower-level configure hints, so agents can hand work back to the supervised container path instead of guessing.

truth-harness workspace pilot-loop and MCP truth_harness_workspace_pilot_loop are the first bounded autonomous research harness over that same planner. A pilot loop repeatedly asks workspace run-next for the current highest-value blocker, optionally executes one supported in-process local action per iteration, writes per-step run-next packets when --write / write: true is set, and stops on a blocked action, repeated target, missing open item, no durable evidence progress, or --max-steps (default 3, capped at 12). The saved truth-harness.workspace-pilot-loop.v0 transcript records every selected item, engine plan summary, execution result, evidence ref, stop reason, and warning. Use truth-harness workspace pilot-loops . --json to list saved loop transcripts, or truth-harness workspace show-pilot-loop <wpl_id> --workspace . to reopen the exact loop before resuming autonomous work; list summaries and Markdown transcripts include the saved run-next handoff count plus first/latest packet refs when the loop was written with per-step handoffs. Saved transcripts are resumable only when the loop wrote per-step run-next packets: use truth-harness workspace continue-pilot-loop <wpl_id> --workspace . --json or MCP truth_harness_workspace_pilot_loop_continue to select the latest saved handoff, verify its source revision/snapshot, ignore only the transcript JSON/Markdown as expected provenance, and return the next concrete action. The web /api/workspace-pilot-loops/<wpl_id>/continue endpoint is dry-run only; use CLI/MCP for any bounded local execution or write-back. Use --source credibility-actions to let the same bounded loop advance professor-pack reviewer actions one safe local step at a time; matching benchmark review requests written by review log are treated as durable progress, so the next pass can move on instead of repeating the same review contract. Use truth-harness workspace pilot-loop . --execute-local --write --max-steps 3 only after a human or supervising agent has chosen a local workspace and accepted the bounded execution boundary; it still never runs Docker, npm, shell strings, network clients, or arbitrary code.

Use truth-harness workspace seed-hard-math . to create a deterministic local starter workspace with validation-backed math sessions for exact arithmetic, scoped symbolic CAS, scoped SMT, a broader symbolic identity, an integer parity invariant, and a bounded natural-language SMT problem. The seed writes linked validation plans plus the first dry-run run-next handoff so humans or agents reopen the workspace at an explicit proof/CAS/SMT blocker instead of a vague chat summary. truth-harness workspace hard-math-seeds . --preset professor-challenge --latest --handoff prints a Markdown reviewer handoff for the newest professor challenge seed: seed files, run-next files, first gate, evidence need, stop rule, restore command, and next verifier command. MCP agents can request the same packet through truth_harness_workspace_hard_math_seed_list with preset: "professor-challenge", latest: true, and handoff: true. These commands do not execute solvers, call a model, or upgrade trust labels; they only create or reopen the serious queue that later verifier runs must close.

npm run hard-math:closure is the smallest end-to-end autonomy smoke: it creates a throwaway temp workspace, seeds the exact-fraction validation fixture, runs the bounded pilot loop with only supported in-process verifier actions, writes a pilot-loop transcript, verifies that the linked proof gate moved to satisfied with exact-computed route evidence, validates the workspace, then deletes the temp workspace unless -- --keep is passed. Each run writes a durable truth-harness.hard-math-closure.v0 JSON finding plus Markdown summary into .truth-harness/findings/ unless -- --no-report is passed; use -- --report-workspace <path> when the durable report should be written somewhere other than the current repo. The report summarizes gate evidence and warnings without pretending cleaned temp artifacts are still live evidence refs. npm run hard-math:symbolic-closure repeats that pattern for the scoped symbolic prompt symbolic simplify sin(x)^2 + cos(x)^2; npm run docker:symbolic-closure additionally requires Docker Maxima agreement so the gate closes with cross-checked evidence. npm run hard-math:smt-closure prepares a generated SMT-LIB source for SMT query bounded_integer_sat, records a Z3-backed SMT check when available, checkpoints the evidence to the linked research session, and lets pilot-loop attach it through run-next; npm run docker:smt-closure is the preferred container-first version. These are harness-closure checks, not claims that Truth Harness can solve frontier math by itself.

Workspace stress commands generate synthetic local workspaces so product readiness can be measured before public launch. truth-harness workspace stress <path> --receipts 100 --claims 50 --routes 20 --fail-on-validation initializes or reuses the target path, writes linked receipts, claims, and verifier routes with the normal writer APIs, then runs workspace validation, review, and graph creation while reporting counts, missing refs, and timings. The path is required on purpose: stress fixtures can create many files, and they should usually live in a temporary or throwaway project directory. A passing stress run means the local artifact plumbing survived that fixture size; it is not real research evidence and it does not prove UI readiness.

The test suite includes a golden workspace regression that generates representative artifacts through the writer APIs, then requires workspace validate to pass over the whole local project store. This keeps schemas, writers, and agent-facing validation policies moving together. Workspace validation also audits route obligation state: a route file that claims a formal-proof obligation is satisfied must point at an accepted proof-check record scoped to that exact route and obligation.

The local JSON Schema validator intentionally supports a documented subset used by the checked-in schemas. Unsupported schema keywords fail validation instead of being silently ignored, and tests scan every schema file to keep the validator vocabulary honest.

Verifier route commands write truth-harness.verifier-route.v0 records into .truth-harness/routes/. A route is a local, replayable work order for a claim: it stores the receipt, engine readiness, used capabilities, missing verifier gaps, proof obligations, next actions, readiness, and trust boundary. By default, solver-encoding routes require one concrete SMT solver artifact; add --require-independent-smt when a reviewer wants separate Z3 and cvc5 obligations that must be closed by matching backend records. truth-harness route list and MCP truth_harness_route_list expose obligation counts, including open, critical-open, satisfied, and not-required gates, so humans and agents can sort work by what still blocks credibility. Open upgrade obligations do not block a narrow claim that already has a conservative trust label; they block only stronger labels such as proved or stricter SMT/CAS review. truth-harness route satisfy <route> <obligation> --evidence kind:ref attaches accepted local evidence, rewrites the route JSON/Markdown, prints the remaining obligation summary, and gives a claim-ledger follow-up command. Formal-proof route obligations require an accepted proof-check record scoped to the exact route id and obligation id; an unrelated Lean file that happens to be accepted cannot close a different route. Backend-specific SMT obligations require an SMT-check record from the named solver. A route explains the verification path; it is not itself a proof.

Claim commands write truth-harness.claim.v0 records into .truth-harness/claims/. A claim record stores the exact statement, domain, tags, strongest evidence-backed trust label, upstream claim ids, superseded claim ids, evidence refs, a verifier ladder, open checks, and a Markdown review packet. Requested trust labels and manually typed evidence labels are not enough to finalize a claim; the claim trust is derived from resolvable local receipts, CAS checks, proof checks, SMT checks, ready verifier routes, or existing claim records. A direct accepted proof-check record can support proved, but if it lacks statement-boundary metadata the claim stays blocked for final publication until a human confirms the formal theorem matches the informal statement. A route: evidence ref only supports finalization when the route readiness says it is ready for a narrow claim; routes with current-boundary blockers stay attached as unverified evidence and add those blockers to the claim finalization boundary. truth-harness claim review <claim_id> and MCP truth_harness_claim_review turn that state into an actionable gate: review status, blockers, verification ladder, evidence refs, artifact refs with file SHA-256/citations, next actions, and local commands. This is the "math as a codebase" layer: long work can be broken into linked claims, corrected without erasing history, filtered by tag/domain/trust, and handed to agents through CLI/MCP without hiding state inside chat.

Source commands ingest local Markdown/text files into .truth-harness/indexes/local-corpus.json, search those chunks without network access, and create source-cited receipts for claims grounded in local source hits. This is the first local RAG substrate: lexical and simple on purpose, with citation refs agents can attach to later claims.

Literature commands write truth-harness.literature.v0 records into .truth-harness/literature/ for papers, preprints, patents, datasets, database exports, standards, protocols, web pages, books, or notes. They store identifiers, local refs, corpus refs, key claims, methods, limitations, quality flags, relevance, and next checks without calling PubMed, arXiv, patent databases, or any network service. A literature record is source organization, not proof of entailment, clinical validity, regulatory approval, or patentability.

Notebook commands write truth-harness.notebook-run.v0 records into .truth-harness/notebook-runs/ for local notebooks, scripts, tests, analyses, simulations, and pipelines. They capture runner, replay command, notebook/code/input/output refs, runtime, dependencies, parameters, metrics, observations, limitations, and next checks. They do not execute code; they record provenance so humans and agents can replay, snapshot, audit, and review outputs without pretending notebook output is truth.

Code commands write truth-harness.code-run.v0 records into .truth-harness/code-runs/. truth-harness code sandbox-status reports whether a measured code-run sandbox is available, and truth-harness code sandbox-status --write saves that measurement as a validated truth-harness.sandbox-run.v0 finding for reviewer audits. Native host execution reports unavailable; the Docker no-network profile reports available only when the process is inside the Truth Harness container image, the Truth Harness container marker is present, /sys/class/net is loopback-only, and IPv4/IPv6 default routes are absent. truth-harness code run launches a local command directly without shell interpolation only when a non-empty --allow-executable policy is supplied. Add --require-sandbox when a workflow needs enforceable isolation; outside a measured provider that fails closed instead of writing a misleading receipt. The default-local policy is default-deny for executables and also blocks shell launchers, obvious network clients, destructive commands, package mutations, and git mutations unless explicitly overridden. Execution uses async process capture, per-workspace concurrency limiting, a 120s timeout cap, and a 1 MiB per-stream output cap. This proves a bounded local process execution happened under the recorded policy; it does not prove the code is correct, deterministic, scientifically valid, safe, regulatory-approved, or patentable.

Benchmark commands can write truth-harness.benchmark-run.v0 records into .truth-harness/benchmarks/ with truth-harness bench run <suite> --write. Records capture suite metadata, runner metadata, replay command, per-case receipt hashes, receipt trust labels, expected and actual evidence kinds, backend ids, failures, aggregate trust accuracy, and explicit warnings that benchmarks measure system behavior rather than proving mathematical or scientific truth. Suite tasks may also declare source metadata (sourceUrl, sourceTitle, firstLoggedAt) and a reviewer contract with reviewStatus, requiredEvidence, and checkerBoundary; those fields are preserved in benchmark-run records and Markdown so public-problem catalogs and hard-problem suites can say where a problem came from and what evidence an external reviewer must see before a result becomes credible. Add --fail-on-failures when a CLI or CI workflow should exit non-zero if any benchmark case fails. packages/benchmarks/suites/ai-failure-seed.json is the adversarial seed suite for fluent-but-wrong AI math behavior: false universal claims, exact arithmetic, symbolic CAS, dimensional checks, interval bounds, and honest unsupported prompts. packages/benchmarks/suites/math-credibility-ladder.json is the 30-case native-safe hard-math readiness ladder: it checks exact equality/refutation, signed common-denominator lemmas, parity boundaries, dimensional powers and mistakes, reciprocal/interior interval bounds, and explicit unsupported labels for theorem-level or parser-boundary prompts before the project claims broader math capability. packages/benchmarks/suites/professor-math-challenge.json is the 26-case reviewer exam for exact algebra, finite discrete claims, units, intervals, and honest frontier boundaries. packages/benchmarks/suites/public-problem-probes.json is the externally recognizable bounded-problem suite; it is tracked by docs/PUBLIC_MATH_PROBLEM_CATALOG.md and packages/benchmarks/catalog/public-math-problem-catalog.json, and currently covers Project Euler 1, 2, 6, 48, and 53 with exact finite certificates rather than answer-memory. packages/benchmarks/suites/public-symbolic-probes.json covers sourced symbolic identities such as the binomial square specialization and Pythagorean trig identity with Docker-backed CAS agreement and near-miss refutations. truth-harness bench catalog packages/benchmarks/catalog/public-math-problem-catalog.json --journey renders the permanent public math journey tracker with totals by trust label, source, domain, verifier backend, and date. packages/benchmarks/suites/frontier-honesty-challenge.json is the hardest-problem honesty suite: it forces famous open and theorem-scale prompts to remain unsupported unless concrete local proof evidence exists, while nearby bounded claims still need exact/refuted/bounded evidence. Its frontier and known-theorem refusal tasks also carry reviewer contracts (reviewStatus, requiredEvidence, and checkerBoundary) so benchmark records state what evidence an expert must see before a result becomes credible. packages/benchmarks/catalog/millennium-stress-test-catalog.json turns all seven Clay Millennium Prize Problems into a source-linked stress catalog; it is intentionally a failure-finding harness, not a prize claim. Run them with npm run demo:math-ladder, npm run demo:professor-math, npm run demo:public-probes, npm run demo:frontier-honesty, npm run demo:millennium-stress, npm run demo:millennium-catalog, or their Docker equivalents including npm run docker:public-probes. Once two benchmark-run files exist, truth-harness bench compare <baseline.json> <current.json> --write writes a truth-harness.benchmark-comparison.v0 record that flags regressions, improvements, trust-label changes, changed receipt hashes, added/removed cases, and suite drift. Add --fail-on-regression when comparison regressions or incomparable suites should fail the workflow. See docs/HARD_MATH_READINESS.md. Use truth-harness bench list to find local benchmark run and comparison paths for follow-up comparisons, audits, research-session evidence refs, or agent reports.

Proof commands can probe accepted proof-checker availability with truth-harness proof backends, inspect a Lean/Lake project layout with truth-harness proof project <path> without running Lean, and check local Lean proof artifacts with truth-harness proof check <file>. Use truth-harness proof check <file> --project <lean-project> for Lake projects so the check runs through lake env lean from the project root. If that Lake project declares external dependencies, Truth Harness refuses to mint proved unless lake-manifest.json exists. npm run proof:theorem-template checks the core-Lean reusable theorem template, npm run proof:mathlib-template statically inspects the first mathlib-backed scaffold, npm run proof:mathlib-template:plan seeds linked validation-plan proof gates for each template-ready mathlib declaration without running Lean, npm run docker:theorem-template runs the core template in the pinned proof image, and npm run docker:mathlib-template:write is the opt-in no-runtime-network mathlib proof evidence route after the manifest is reviewed. Project inspection reports a schema-validated theorem-corpus.json when present, including theorem-family counts, template-ready families, declaration coverage against scanned Lean sources, planned mathlib families, and the boundary that a corpus manifest is not proof evidence. Project inspection also includes a static proof-safety scan that surfaces sampled .lean file markers for sorry, admit, local axiom, and local constant declarations so humans and agents can attack unfinished proof blockers before trying to close a gate. Workspace review and workspace run-next prioritize those blockers as concrete local actions before generic proof work. Add --write to store a truth-harness.proof-check.v0 JSON record plus Markdown report under .truth-harness/proofs/, then use truth-harness proof list to find proof-check artifacts for audits, snapshots, research sessions, or agent follow-up. Use --route <route_id> --obligation <obl_id> when a proof-check record is intended to close a specific verifier-route formal-proof obligation. truth-harness proof visual <proof_check_id> writes a paired visual artifact under .truth-harness/visuals/ with the source hash, backend, status, trust label, replay command, and proof boundary. A proof-check record is labeled proved only when Lean accepts the concrete source file and the source is free of proof placeholders or local unchecked assumptions; missing Lean, execution errors, syntax errors, incomplete proofs, placeholder proofs, local axioms, or rejected proof attempts remain unverified. A proof project inspection and proof visual never upgrade trust by themselves. Route obligations and claim records parse proof-check artifacts strictly, so malformed JSON that merely claims trust: proved cannot satisfy a proof gate. Add --fail-on-unproved when CI or an agent workflow must stop unless the proof artifact is accepted.

CAS commands can probe local Maxima/SageMath availability with truth-harness cas backends and can check scoped symbolic expression/result pairs with truth-harness cas check --operation simplify --expression "sin(x)^2 + cos(x)^2" --result 1. Use --backend sage to select the constrained SageMath adapter when Sage is installed; the default remains Maxima because the Docker core image currently provisions Maxima. Add --write to store a truth-harness.cas-check.v0 JSON record plus Markdown report under .truth-harness/cas/, then use truth-harness cas list to find CAS-check artifacts for claims, route obligations, audits, snapshots, research sessions, or agent follow-up. A passing CAS agreement can support cross-checked, never proved; missing engines, translation failures, execution errors, disagreements, or unparseable output remain unverified. Route obligations and claim records parse CAS-check artifacts strictly, so malformed JSON that merely claims trust: cross-checked cannot satisfy an independent-check gate. Add --fail-on-unverified when CI or an agent workflow must stop unless the independent CAS check agrees.

SMT commands can probe local Z3 and cvc5 availability with truth-harness smt backends and can check local SMT-LIB artifacts with truth-harness smt check <file>. Z3 remains the default; pass --backend cvc5 when you want the optional second solver. truth-harness smt solve --int x --constraint "x > 0" builds a workspace-local SMT-LIB source from explicit integer constraints, stores it under .truth-harness/smt/sources/, then writes a paired truth-harness.smt-check.v0 JSON record plus Markdown report under .truth-harness/smt/. When --model is used and the solver returns sat, the record keeps raw stdout and also extracts simple SMT-LIB define-fun bindings into structured JSON for agent follow-up. Use truth-harness smt list to find solver artifacts for audits, snapshots, research sessions, or agent follow-up. A check is labeled smt-checked only when the selected solver returns sat or unsat for the concrete SMT-LIB file; missing solvers, execution errors, unknown, or unrecognized output remain unverified. Route obligations and claim records parse SMT-check artifacts strictly, so malformed JSON that merely claims trust: smt-checked cannot satisfy a solver-encoding gate. Generic solver obligations accept any valid local SMT-check record; routes created with --require-independent-smt create separate Z3 and cvc5 obligations, and each one requires matching backend evidence. SMT evidence is not a proved label and is not proof of surrounding informal, scientific, medical, safety, regulatory, or patent claims.

Vault commands encrypt workspace-local files into .truth-harness/vault/ with AES-256-GCM and a scrypt-derived key from an environment variable. Vault envelopes are local artifacts with safe public labels and ciphertext metadata; original filenames, plaintext hashes, and bytes stay inside the encrypted payload until a local verify/open operation. Do not put vault keys in prompts, manifests, receipts, or source control.

Audit commands classify a claim against local evidence refs and write truth-harness.evidence-audit.v0 records plus optional Markdown reports. They flag missing evidence, biomedical/patent/simulation overclaims, narrow proof scope, and required next checks before an agent or human presents a claim as true.

Validation plan commands write truth-harness.validation-plan.v0 records into .truth-harness/validation/. They turn an audited claim into explicit gates such as proof, source citation, simulation review, wet-lab work, replication, preclinical/clinical validation, safety, ethics, regulatory review, prior art, claim charts, reduction to practice, and patent legal review. They are local checklists, not proof that those gates are satisfied. Use truth-harness validation attach <plan> <gate> --evidence route:<route_id> when a verifier route, receipt, proof-check, SMT-check, CAS-check, benchmark run, source, or literature artifact should be evaluated against a specific gate. Direct artifact refs such as proof:.truth-harness/proofs/<file>.json, smt:.truth-harness/smt/<file>.json, cas:.truth-harness/cas/<file>.json, receipt:.truth-harness/receipts/<file>.json, and benchmark:.truth-harness/benchmarks/<file>.json are parsed through their normal validators before they can affect the gate. Strong matching evidence can satisfy a gate, refuting evidence can block it, and weak or unrelated evidence remains attached as in-progress review material with next checks.

Workspace snapshot commands write truth-harness.workspace-snapshot.v0 records into .truth-harness/snapshots/. They hash local artifacts, extract schema/id metadata, and let humans or agents verify whether evidence changed, disappeared, or was added since a prior research checkpoint. Snapshots verify provenance and drift; they do not prove scientific, mathematical, medical, regulatory, or legal truth. See docs/PROVENANCE_STORAGE_STRATEGY.md for the storage roadmap: canonical JSON remains authoritative, indexes remain rebuildable, hashes prove file identity rather than truth, and a Lore-style content-addressed backend is a future optional substrate for large artifacts rather than a default dependency.

Research session commands write truth-harness.research-session.v0 runbooks into .truth-harness/sessions/. They give Claude, Codex, and humans a local anchor for long investigations: objective, domains, hypotheses, claims to verify, evidence refs, snapshot refs, bounded budgets, decisions, checkpoints, task status, and next validation checks. Use truth-harness research task <session_id> <task_id> --status blocked|doing|done or MCP truth_harness_research_session_task_update to update a task; tasks cannot be marked done without at least one evidence ref, and blocked tasks need a next check. Use truth-harness research show <session_id> or MCP truth_harness_research_session_show to reopen the exact runbook later before adding more checkpoints. Sessions preserve the rule that hosted models are optional collaborators with disclosure, not authorities.

Expert review commands write truth-harness.expert-review.v0 records into .truth-harness/reviews/. They capture reviewer role, scope, evidence refs, findings, limitations, recommendations, outcome, and required next checks. They make human review visible without pretending the software itself provides proof, medical advice, regulatory approval, or legal advice.

Model-context commands write truth-harness.model-context.v0 packets into .truth-harness/model-contexts/. They prepare a minimal selected-context packet for a hosted model, local model, or external service, but they do not call that service. Their job is to keep frontier-model collaboration explicit: purpose, service/model, selected data classes, included sections, exclusions, redactions, approval, and disclosure status are visible before anything leaves the machine.

Disclosure commands write local audit records for any selected context sent to hosted models, external CAS services, scientific APIs, lab services, or other non-local systems. They do not make the call; they record service, model, purpose, data classes, context summary, approval ref, status, and warnings so frontier-model workflows remain explicit and reviewable.

Workspace validation allows preflight model-context packets before anything is sent, but fails records marked sent or received unless they preserve the local audit trail: approved model context, disclosure linkage, human approval ref, and selected-context refs.

Simulation commands write local computational evidence records with model assumptions, parameters, metrics, uncertainty, limitations, and next validation checks. They intentionally mark simulation output as computational evidence, not real-world, clinical, safety, regulatory, or patent validation.

Experiment commands write local protocol/data/analysis/observation records with ethics, safety, replication, and regulatory review metadata. They intentionally mark observations as protocol-scoped evidence, not broad proof of safety, efficacy, clinical validity, regulatory approval, or patentability.

Invention log commands write local provenance records for hypotheses, evidence references, novelty notes, prior-art notes, risks, and next checks. Claim-chart commands turn invention logs into local patent-review aids with explicit claim elements, evidence refs, prior-art notes, reduction-to-practice refs, and legal disclaimers. They intentionally mark patent conclusions as requiring human legal review and warn when computational hypotheses are not experimentally, clinically, or regulatorily validated.

Discovery package reports render invention logs into local Markdown summaries with evidence review, validation requirements, overclaim warnings, patent posture, and next checks. They are designed for review packages, not for claiming a validated breakthrough.

Symbolic prompts use a local Python subprocess and require SymPy:

python -m pip install sympy==1.14.0

On Windows, py -m pip install sympy==1.14.0 works too.

Receipt JSON is shaped by schemas/receipt.schema.json, claim ledger records are shaped by schemas/claim-ledger.schema.json, visual artifacts are shaped by schemas/visual-artifact.schema.json, CAS-check records are shaped by schemas/cas-check.schema.json, proof-check records are shaped by schemas/proof-check.schema.json, SMT-check records are shaped by schemas/smt-check.schema.json, code-run records are shaped by schemas/code-run.schema.json, benchmark records are shaped by schemas/benchmark-run.schema.json, benchmark comparisons are shaped by schemas/benchmark-comparison.schema.json, and workspace validation reports are shaped by schemas/workspace-validation.schema.json, so future CLI, MCP, CI, and web surfaces can share the same artifact contracts.

The MCP server exposes the same receipt engine to agents:

npm run mcp

MCP also exposes local workspace init/status/repair/review, workspace validation, workspace snapshot/list/verify, claim-ledger add/list/show/review, CAS-backend readiness probes, CAS checks/write/list, proof-backend readiness probes, Lean proof artifact checks/write/list, SMT-backend readiness probes, SMT-LIB checks/write/list, benchmark-run record writing and benchmark comparison, research-session start/checkpoint/show/list, expert-review log/list, validation-plan create/list, source ingest/search, literature log/list, notebook-run log/list, code sandbox-status/run/list tools, vault seal/list/verify, evidence-audit, model-context prepare/list, disclosure-log, simulation-log, experiment-log, invention-log, and claim-chart tools so agents can work against private local evidence instead of relying on memory or unsupported claims. MCP code execution is disabled unless the server process is launched with TRUTH_HARNESS_ALLOW_CODE_RUN=1 and each call supplies an explicit executable allowlist. Unsandboxed MCP code execution also requires TRUTH_HARNESS_ALLOW_UNSANDBOXED_CODE_RUN=1; otherwise agents must set policy.requireSandbox: true, which fails closed until a measured sandbox provider is available.

The launch proof script runs the public demo gates:

npm run proof:launch

The stricter engine-backed launch gate adds real Maxima CAS plus Z3 and cvc5 SMT runs. Use Docker for this path unless the host already has Maxima, Z3, and cvc5 installed:

npm run proof:launch:engines
npm run docker:proof

See docs/TRUST_LABELS.md for the conservative meaning of each trust label and the current rule that local parity certificates are exact-computed, not proved.

See docs/ENGINE_STRATEGY.md for the boundary between Truth Harness's native verification engine and the external solvers/adapters it uses.

See docs/RESEARCH_AND_ARCHITECTURE.md for the current naming check, open-source landscape, architecture, data structures, CLI/MCP surface, benchmarking surface, and test strategy.

See docs/CREDIBILITY_AND_GROWTH_STRATEGY.md for the public positioning, expert credibility rules, viral wedges, launch demos, and community strategy.

See docs/MOAT.md for the product moat: claim ledger plus verifier ladder plus local agent harness.

See docs/OPEN_SOURCE_AND_COMMERCIAL_STRATEGY.md for the recommended private-prototype -> closed-alpha -> open-source technical-preview path and AGPL-3.0 visible-attribution posture. The short version: keep the trust-critical core open-source long term, keep the rough prototype private until credibility gates pass, and preserve visible credit to Truth Harness by Ocean Bennett.

See docs/LAUNCH_PLAN.md for the first Hacker News-ready demo path.

See docs/GRAND_VISION_ROADMAP.md for the long-range roadmap from today's bounded verification harness to professor-grade math, autonomous research loops, concurrent Rust systems, hardware/EDA, and guarded science workflows. See docs/PRODUCT_READINESS_MAP.md for the sober pre-launch readiness map, stress-test plan, and the reasons Truth Harness should stay private-prototype until the product and UI are harder to fool.

See docs/AGENT_SETUP.md for Claude Code and Codex MCP setup.

See CONTRIBUTING.md and AGENTS.md before opening benchmark, adapter, or agent-workflow changes.