The guarantee ladder

A property does not merely pass or fail. It sits on a rung, and the rung is recorded in the definition's metadata. Oath's central discipline is never dressing up a claim as more certain than it is.

The rungs

asserted

The property exists in the signature but has not been checked. It is a claim, nothing more.

tested

The property held for 200 generated inputs. Generation is deterministic — seeded from the definition's own hash — so a tested verdict is reproducible byte-for-byte. Testing can only ever find counterexamples, never rule them out.

proven

The property was translated to SMT-LIB and Z3 held it for all inputs. Datatypes become SMT algebraic datatypes, recursive functions become quantified defining equations, matches become tester/selector chains, records become single-constructor datatypes, and function values are array-encoded — so higher-order properties quantify over all functions and capability properties over all worlds. Recursion is handled by structural induction.

falsified

A counterexample was found. This is a first-class, recorded outcome — a wrong definition is a fact in the store, not a hidden bug. oath build refuses to compile an executable from a falsified oath.

Why the rungs differ, in one exhibit. abs-small passes all 200 test cases and is then refuted by Z3 at an input the generator never draws.

examples/undertested.oath — abs-smalltested · refuted at x = -401

(defn abs-small [] [(x Int)] Int
  (if (< x 0) (- 0 x) x)
  (prop bounded-wrongly [(x Int)]
    (< (abs-small x) 401)))

The standing caveat

Z3 reasons over unbounded integers; the evaluator uses int64. A proof is valid modulo overflow, and the corpus says so. Division and modulo stay outside the proof fragment on purpose: the kernel truncates while SMT-LIB is Euclidean, so a "proof" over division would certify the wrong theorem.

Four dimensions, not one

Alongside property proofs, every definition carries three more verdicts:

Termination. A structural checker proves totality where recursion visibly descends — including lexicographic descent, so merge (which alternates which argument shrinks) is still total. Everything else is honestly termination unproven and fuel-bounded.
Confinement. A capability parameter that is only exercised — never returned, stored, or captured — is verdicted confined. Capability-hoarders are marked ESCAPES.
Spec strength. Mutation testing asks the question "who verifies the specs?" — does a property notice when the body changes? Survivors are printed with their bodies; judged-equivalent mutants can be waived with justification, and waivers report separately from kills.
Provenance. Every put attempt — accepted, falsified, or rejected — is retained in an append-only journal with principal attribution, timestamp, and verifier version.

Verdicts are structure × seed facts. Mutation scores and waivers derive from the definition's hash; they are never carried across an identity change. A fixture is only evidence once you know it was regenerated under the current identity.