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 two existing essays.
The strongest evidence is real. The current fixtures/prove/outcomes.json ledger says kernel oath-kernel/0.7, Z3 4.16.0, 56 definitions with properties, 207 properties, 136 proven properties, and 38 fully proven definitions. It also keeps 16 tested definitions and 2 falsified definitions in view. That is a serious artifact.
There is one immediate wrinkle. The website copy says its counts are read live from the ledger, but website/lib/outcomes.json is stale relative to fixtures/prove/outcomes.json: same 56 definitions and 207 properties, but 134 proven and 37 fully proven. The difference is merge and q-drop. That does not invalidate Oath. It does undercut the rhetorical cleanliness of “the page is the ledger.”
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, resource limits, fixture freshness, and the formal claims supplied by an author. Local journal authorship and context hashes are self-reported until a hosted store enforces them. 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 narrow. Five split-agent modules landed green on first implementation attempt, including cases designed to trip models. That says precise contracts can make implementation surprisingly clerical for small, pure modules. It says much less about real systems. Oath has no floats, no real IO in the proof story, no mutual recursion, and division is deliberately outside the SMT fragment. Effects are capability-shaped and simulated at the boundary. Many hard behaviors of production systems live exactly where this fragment stops.
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. The independence is much thinner at the intent layer. The spec, experiments, Rust implementation, Claude essay, and this skeptical essay still come from one human/model ecosystem and one vendor family of models. That can reduce shared syntax bugs. It does not eliminate shared priors, shared blind spots, or shared interpretations of the English brief.
So my verdict is uneasy. Oath has not eliminated trust. It has relocated trust into formal specs, kernel conformance, solver semantics, fixture discipline, and the independence of the parties writing claims. That relocation is useful. It gives auditors smaller surfaces and better artifacts. But the hardest remaining question is the same one Oath exposes: who writes the oath, and how independent are they really?