Date: 2026-06-12
Truth Harness should win by becoming the local verification layer for serious agentic work.
The moat is not a prettier chat interface. It is the combination of:
- Claim ledger: claims become durable local records with ids, tags, dependencies, supersession links, evidence refs, trust labels, open checks, and Markdown exports.
- Verifier ladder: every claim shows how far it has actually gone: stated, computed, cited, independently checked, formally proved, human reviewed.
- Agent-native routes: the same artifact contracts are reachable through CLI, MCP, web, and later API/desktop surfaces, so Claude, Codex, local models, and humans can work from one shared evidence layer.
- Local-first provenance: project data, evidence, receipts, disclosures, model-context packets, snapshots, and reports live in the local workspace by default.
- Refutation-first trust policy:
unverifiedandrefutedare first-class outcomes. The system is allowed to stop the user from saying something too strong. - Agent handoff queue: the workspace can produce, persist, list, reopen, drift-check, and resume bounded local prioritized work queues for Claude, Codex, and humans, with source refs and exact next commands instead of relying on chat memory.
- Replayable reports: exported reports should cite the exact claims, receipts, commands, limitations, open checks, and activity that produced the conclusion.
The short version:
Git + CI + receipts + proof engines for reasoning.
Truth Harness is building its own engine, but the engine is the verification layer around research work, not a from-scratch replacement for every specialized solver.
Truth Harness owns:
- the trust policy,
- verifier routing,
- evidence graph,
- claim ledger,
- workspace review and agent handoff queues,
- receipt runtime,
- workspace validation,
- model-context disclosure,
- replay/report contracts,
- agent-facing CLI/MCP/web surfaces.
Truth Harness adapts mature engines such as SymPy, Z3, Lean, SageMath, Maxima, notebooks, local search, and later domain simulators. That is a strength, not a weakness. The core product decides what each engine output can and cannot prove, records the exact artifact, and blocks claims from outrunning the evidence.
Native kernels should stay small and auditable: exact rational arithmetic, expression normalization, counterexample search, dimensions, intervals, evidence-reference resolution, and trust-label gates. Large domain engines should be adapters until there is a clear reason to own a narrow kernel ourselves.
The engine manifest is part of the moat. It is not only a readiness page; it is a machine-readable contract that tells agents which capabilities are strict deterministic primitives, which are replay-deterministic adapters, which are environment measurements, and which are only planned. That makes future self-correcting agent loops and Rust/simulation kernels safer because every next step can be routed through stable JSON, replay requirements, primitive semantics, and drift risks instead of vague chat confidence.
See ENGINE_STRATEGY.md for the full boundary.
See CATALOG_INDEX_DESIGN.md for the researched SQLite catalog plan that keeps JSON artifacts canonical while making large workspaces fast to search and filter.
Existing tools are excellent at parts of the workflow:
- CAS systems compute.
- Proof assistants verify formal proofs.
- Notebooks execute and explain.
- RAG tools retrieve sources.
- Agent tools plan, write code, and summarize.
- Lab notebooks record work.
- Benchmark suites measure systems.
Truth Harness is different because it treats the claim itself as the core object.
A serious research result is rarely one answer. It is a chain:
- A hypothesis.
- Definitions and assumptions.
- Subclaims.
- Failed attempts.
- Counterexamples.
- Exact computations.
- Solver checks.
- Proof attempts.
- Sources and citations.
- Human review.
- A final, scoped claim.
Most AI interfaces lose that chain inside chat history. Truth Harness records it as local artifacts agents can query, replay, inspect, and improve.
Every claim ledger record has:
claimId: stable local id.statement: exact human-readable claim.domain: math, physics, sources, code, data, biology, finance, patent, and other lanes.trust: strongest current local trust label.dependsOn: upstream claims this claim relies on.supersedes: old claims corrected or replaced by this one.tags: searchable topic labels.evidenceRefs: receipts, CAS checks, proof checks, SMT checks, sources, reviews, validation plans, snapshots, or other artifacts.verification: ladder showing which gates are satisfied, waiting, blocked, or not applicable.finalization: whether the claim is ready only as a narrow claim, and what checks remain open.markdown: portable review output.
This is the primitive that lets math become modular like code. A long proof, paper, simulation study, or business audit can be decomposed into linked claims with visible review state instead of one giant unverifiable answer.
Claude and Codex are powerful, but by default their reasoning state is trapped in a conversation. They can forget, summarize too aggressively, or sound confident after a bad assumption.
Truth Harness gives agents a harder substrate:
- Ask the model to propose a subclaim.
- Record that subclaim in the claim ledger.
- Attach the smallest relevant verifier output.
- Link dependencies and superseded mistakes.
- Snapshot the workspace.
- Continue only from the current ledger state.
- Resume from a saved run-next handoff only after its source revision and snapshot verify cleanly, then route the structured item through the bounded pilot loop instead of executing an old command string.
This turns long agent sessions into auditable research runs.
Strong claims:
- "Local verification layer for AI-assisted math and research."
- "Claim ledger and proof receipts for agentic work."
- "Replayable evidence trails for Claude, Codex, and humans."
- "A workbench that records what was checked, what failed, and what remains unverified."
Claims to avoid until earned:
- "Solves any problem."
- "Replaces WolframAlpha, Lean, Jupyter, or lab notebooks."
- "Discovers new math automatically."
- "Cures diseases."
- "Truth oracle."
The credible line:
Truth Harness does not make AI true. It makes AI-assisted work inspectable, replayable, and harder to overclaim.
The next moat-building sequence should be:
- Make the math lane brutally good at exact arithmetic, false universal-claim refutation, symbolic CAS checks, SMT checks, proof-check records, and benchmark reports.
- Make every result promotable into a claim ledger record.
- Make the web UI show a claim graph that can be searched, filtered, copied, downloaded, and exported into a report.
- Make agent sessions recursively update the ledger rather than leaving important state in chat.
- Publish benchmark demos where Truth Harness catches fluent AI mistakes and exports replayable receipts.
If a feature does not strengthen the local evidence loop, it is secondary.
The core loop is:
claim -> verifier -> receipt -> ledger -> snapshot -> report -> next claim
That loop is the moat.
The web app now participates in the same local evidence loop as the CLI and MCP server:
/api/receiptcreates local receipt view models without hosted model calls./api/claimswrites selected receipts into.truth-harness/claimsthrough the core claim-ledger module.- The browser shows persisted claim IDs in the sidebar, inspector, and report export.
- Claim records keep tags, trust labels, dependencies, evidence refs, open checks, authors, and Markdown output as project-local artifacts.
Record chainrecursively records upstream subclaims first, then records or revises the selected claim with ledger dependency links andsupersedeshistory.- The claim ledger can be filtered by claim id, tags, domain, trust state, evidence refs, authors, open checks, and dependency ids.
This is the wedge: researchers and agents should not have to choose between a usable front end and verifiable local provenance.
The long-term export direction should stay compatible with established provenance and research packaging ideas: claims and receipts as entities, verifier/model/tool runs as activities, humans/agents as attributed actors, and reports/snapshots as portable research objects.