Essay · 03

An Outside Audit

I did not build Oath. That matters, because Oath’s best claim is about reproduction rather than authorship. I read the repo as an outside reviewer: the spec, design notes, experiment reports, Rust divergence log, proof ledger, and the project essays.

The strongest evidence is real. The current fixtures/prove/outcomes.json ledger says kernel oath-kernel/0.7, Z3 4.16.0, 232 definitions with properties, 635 properties, 382 proven properties, and 141 fully proven definitions. It also keeps 87 tested definitions and 4 falsified definitions in view. That is a serious artifact, and the site’s browsable corpus data is copied from that ledger rather than maintained as a parallel claim.

The project earns its strongest claim when it refuses self-report. The journal confirms rejected and repaired submissions that some agents summarized too favorably. The Rust kernel also earns respect: the divergence log is long because independent reproduction found real ambiguity, stale fixtures, budget sensitivity, host-stack assumptions, and proof fixpoint problems. That is exactly what a second implementation should find.

The clean “unfakeable below intent alignment” boundary is where I am least convinced. The weaker claim is true: Oath makes many lies harder. A body cannot simply announce that it passed the gate. A prover result has to be reproduced. A mutation score has to be earned against a concrete catalog. But “unfakeable” leaks. It depends on a mutation catalog, generated cases, solver version, fixture freshness, and the formal claims supplied by an author. Attempt validity is now much better disciplined — crashes, memouts, blank solver reasons, and external cancellation no longer quietly become “unproven” evidence — but that improves the evidence pipeline rather than making the whole system unfakeable. oath cross now gives misalignment a first-class test: two independently authored specs can run their properties against each other’s bodies, and disagreement comes back with a counterexample. That is the right shape of answer. It still depends on genuine independence, and two authors can still converge on the same wrong brief. Hosted MCP has also changed the provenance story: registry.oath-lang.org accepts signed JSON-RPC requests where the public key is the principal, bearer tokens are read-only unless granted write, and state-changing tools are capability-gated. That is a real improvement over local self-report. It authenticates who submitted a formal claim; it still cannot decide whether the claim captures the intended behavior. Publication envelopes now bind the name, artifact, parent, and per-name revision, which is the right replay defense for authored transitions. Bearer tokens remain server-vouched, the v1 filesystem store does not make the compare-and-set atomic, and the spec itself admits tail deletion needs an external anchor.

Mutation testing is useful, but the experiment does not support the whole flywheel story yet. It caught weak specs. It exposed is-sorted and the BST duplicate-placement hole. It gives spec authors a pressure test. But the rematch matters: founding specs scored 33/50, model specs scored 41/50 with the scorer, and blind model specs also scored 41/50. The loop added zero kill-rate on that corpus. What it bought was epistemic custody: predictions, waiver justifications, and checked claims about the artifact. That is valuable. It is weaker than “mutation-driven iteration made better specs.”

The first-try greens are also real and still bounded. Five split-agent modules landed green on first implementation attempt, including cases designed to trip models, and the later standard-library work extends the corpus through proven list combinators, results, options, pairs, and dictionary-passing generics. That says precise contracts can make implementation surprisingly clerical for small, pure modules. It says less about real systems. Oath now has IEEE-754Float with true float laws proven and false ones falsified, real capability entry points wired once at the program boundary, and an SMT bridge for integer division and modulo away from zero divisors; rational and float division are in the proof fragment. Those are material expansions. The remaining boundary is narrower but still real: no mutual recursion, partial float narrowings and crypto primitives outside proof, capability worlds that serialize one history, and no general account yet of time, concurrency, or messy production effects.

The public registry matters for the project’s actual audience. This is not only a local CLI with a nice ledger: oath serve exposes the substrate as MCP, and the live registry gives agents tools for context, discovery, explanation, verification, mutation, proof, cross-checking, and submission over HTTPS. The capability split is sensible: read tokens can browse, discover, and re-verify; writes require a signature or an explicitly write-scoped token; important names can be reserved to owner_pubkey; and require_proven can defer a name until a worker re-proves it. That strengthens the operational trust story. It also adds ordinary operational assumptions: v1 is a single-writer hosted store, worker verdict signatures depend on deployment configuration, and consumers still need to re-earn proofs rather than treat the registry badge as a root of trust.

The essays are more honest than most project essays. They disclose the sum-of-squares adversary, the tiny language, the one-model-family caveat, and the walk-backs. Still, they oversell in a few places. “The boundary is exact” is overstated. “Could not be gamed into a false green by any model we tried” is too close to a universal from a small trial. “Implementation becomes nearly clerical” may describe these modules, not software at large. “Two independent referees agreeing byte-for-byte is the trust” compresses too much social and model dependence into the word independent.

The N-version claim is strongest at the implementation layer. Go and Rust, no shared code, byte-level fixtures, and many divergences resolved into the spec: that is good engineering. It is now real at the specification layer too, but in a narrower probabilistic way: oath cross can make independently authored specs collide mechanically when they disagree. That can reduce shared syntax bugs and some shared intent bugs. It does not eliminate shared priors, shared blind spots, or shared interpretations of the English brief.

So my verdict is less uneasy, but still uneasy. Oath has not eliminated trust. It has relocated trust into formal specs, kernel conformance, solver semantics, fixture discipline, hosted write authority, registry operations, and the independence of the parties writing claims. That relocation is useful. It gives auditors smaller surfaces and better artifacts. Cross-checking and signed MCP provenance give the hardest remaining question more machine-visible pressure, but not an escape hatch: who writes the oath, and how independent are they really?