truth-harness

Truth Harness makes Codex show its work: every math claim is routed through local deterministic engines and returned with replayable evidence, exact checks, and an honest trust label.

Comment 1

Inspiration

AI can produce an explanation that looks rigorous while being mathematically wrong. In serious technical work, one false claim can contaminate code, simulations, research notes, and every conclusion built on top of it.

Truth Harness began with a simple question: what if an AI answer were treated as a claim to verify, rather than a conclusion to trust?

The core principle became:

Codex proposes. Local verifiers decide what the evidence earns.

I wanted a system where an AI agent could explore ambitious ideas while deterministic tools checked its important claims, preserved the evidence, and admitted uncertainty when verification was not possible.

I started thinking seriously about this while building a Rust game engine. I wanted agents to help with collision geometry and difficult systems math, but a confident explanation was not enough. I needed every important answer to come with evidence I could inspect and replay. That frustration became Truth Harness.

What it does

Truth Harness is a local-first verification and evidence layer for Codex and other AI agents.

It routes scoped mathematical claims through deterministic engines and returns conservative trust labels such as:

  • exact-computed
  • cross-checked
  • smt-checked
  • refuted
  • unverified
  • proved, only when an accepted proof checker verifies a concrete proof

Each result can include its input, assumptions, backend, exact output, evidence trace, limitations, replay command, and local artifact references.

Truth Harness provides a CLI, MCP server, local API, Docker verification profiles, and a browser workbench. Humans and agents can inspect the same receipts, replay calculations, trace claim dependencies, and generate reports from the recorded evidence.

The Build Week demo tests a real continuous collision problem. A moving box does not overlap a static box at the beginning or end of a frame, so an endpoint-only check concludes that no collision occurred.

Truth Harness checks the entire continuous interval with exact rational arithmetic. It refutes the claim and reports that the collision occurs from (t = 2/5) through (t = 4/5).

The demo is not mocked. The result comes from the local local-swept-aabb2-intersection verifier inside the Docker workflow with network access disabled.

How we built it

I built Truth Harness with Codex as an implementation, architecture, testing, and review collaborator.

More importantly, Truth Harness is designed to work underneath Codex. Codex can propose a claim, call the harness through CLI or MCP, inspect the resulting receipt, correct a refuted step, and continue from an evidence-backed checkpoint.

The project is a TypeScript monorepo with a shared verification core used by every interface.

The core handles:

  • Claim normalization and verifier routing
  • Conservative trust label policies
  • Receipt and evidence generation
  • JSON Schema validation
  • Claim and evidence ledgers
  • Replayable agent handoffs
  • Validation plans and proof obligations
  • Local workspace snapshots
  • Benchmark and release audits

Verification adapters connect the evidence layer to exact arithmetic routines, SymPy, Maxima, Z3, cvc5, Lean 4, and SageMath. Each adapter has an explicit boundary. A symbolic simplification is not treated as a formal proof, and a bounded search is not presented as a universal theorem.

Generated evidence is stored locally under a .truth-harness workspace. Docker services use disabled networking, dropped capabilities, process limits, and narrowly scoped writable storage.

The browser workbench presents the same evidence available through the CLI and MCP server. It is an inspection layer over real receipts, rather than a separate chatbot with hidden reasoning.

Challenges we ran into

The hardest challenge was defining honest trust labels. Computed, cross-checked, and proved are not interchangeable. The system must refuse to make a stronger claim than its evidence supports.

Security was another major challenge. An agent-accessible execution system cannot rely on command denylists or hardcoded privacy claims. Verification needed explicit Docker, network, process, and filesystem boundaries.

Provenance was equally difficult. A correct answer is not enough if nobody can reconstruct how it was produced. Receipts, hashes, schemas, replay commands, validation plans, and reports had to share one consistent evidence model.

The final challenge was making rigorous evidence understandable. The interface needed to serve agents, developers, students, and expert reviewers without hiding limitations or overwhelming users with raw JSON.

The hardest challenge was resisting my own ambition. I wanted Truth Harness to solve every kind of problem immediately, but I learned that credibility comes from narrow claims, conservative labels, and being willing to return unknown.

Accomplishments that we're proud of

Truth Harness now has:

  • 753 passing automated tests across 86 test files
  • A release audit with 21 passing checks and no warnings or failures
  • Real Docker-isolated verification evidence
  • CLI, MCP, API, and browser interfaces over one shared core
  • Conservative proof boundaries that reject unsupported claims
  • Replayable receipts, claim lineage, validation plans, and agent handoffs
  • External engine case validation for Rust geometry predicates
  • Printable reports and teaching packets generated from recorded evidence
  • A working demonstration that catches a realistic continuous collision error using exact arithmetic

I am especially proud that unknown and unverified are treated as valid results. Truth Harness is designed to admit when the available evidence is insufficient.

The moment it felt real was when the same collision claim produced an exact result through Docker, the CLI, the web interface, a local receipt, and a replay command. The model could explain the result, but it could not change what the verifier found.

What we learned

Uncertainty can be a product feature.

A trustworthy system should clearly distinguish a calculation from a proof, a benchmark from a theorem, a simulation from reality, and a source citation from independent validation.

I also learned that the most valuable AI infrastructure may not be another model. It may be the layer that determines when model output deserves to be believed.

Combining Codex with deterministic local tools creates a useful division of responsibility. Codex provides flexible reasoning, planning, and explanation. Truth Harness records what the available evidence can actually support.

What's next for Truth Harness

Next, I want to expand the verified problem catalog, strengthen independent cross-engine agreement, and invite mathematicians and researchers to challenge the trust model.

I also plan to improve formal proof workflows, external reviewer packets, long-running autonomous verification sessions, and integrations with scientific and engineering tools.

The long-term goal is not to promise automatic breakthroughs. It is to create trustworthy infrastructure where humans and AI can explore difficult problems, catch mistakes early, preserve every important step, and know exactly which conclusions have been earned.

Built With

Share this project:

Updates