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 induction — structural and lexicographic for shrinking datatypes, and recursion induction for functions that recurse on an integer counter (proving measure laws like length (replicate n x) == n).

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.

(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, and the evaluator now matches it: Int is arbitrary precision, so a proof carries no modulo overflow asterisk. Integer division and modulo still stay outside the proof fragment on purpose — the kernel truncates toward zero while SMT-LIB integer division is Euclidean, so a "proof" over Int division would certify the wrong theorem. Rational and float division are different: Rat is exact ℚ over the Real sort (so (a/b)*b == a is genuinely proven), and Float is IEEE-754 over the Float64 sort — both theories are complete, so both reach proven. The nuance for floats is that fewer laws are true: x*1.0 == x proves, but 0.1f + 0.2f == 0.3f is falsified — not for any weakness of the prover, but because it is false. That is the prover being right, and it is categorically different from the recursion fragment, where a true property bails to tested because the solver can't reason about it.

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 — and a Z3-verified ranking function proves it for integer-counter recursion, where the counter is not a shrinking datatype (replicate, range, the count inside rle-expand's Run). Genuinely non-terminating or unanalyzable recursion 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.