Architecture

Oath Language is a small, auditable kernel around an immutable object store. Every piece exists to make one guarantee: an accepted name points at a definition that has been checked, not merely stored.

The object store

The store is a content-addressed object database. Each object's file name is the SHA-256 of its canonical binary encoding (the "O1" encoding — identity leaves the host language, so two kernels can agree on it exactly). Objects are immutable; names are a separate mutable index that points into the store. Content addressing means there are no namespace wars — names are local, hashes are universal.

The store is trusted because it is checked, not merely because it is content-addressed: an object written straight into the store is re-validated on load, because the typechecker and evaluator are not total on malformed definitions.

The trusted gate

Elaboration turns surface syntax into the canonical AST, resolving names to de Bruijn indices and hashes. The typechecker is bidirectional local synthesis — type arguments may be omitted and are inferred by one-sided matching, never unification of two unknowns — small enough to audit. It also enforces strict positivity on datatypes, so a type that would encode non-termination is rejected at the gate. Only then does the evaluator run each property under a fuel and depth bound.

The prover

The prover translates properties to SMT-LIB and discharges them to Z3. Recursion is handled by induction — structural and lexicographic for shrinking datatypes, and recursion induction for functions that recurse on an integer counter (whose totality a Z3-verified ranking function establishes). The defining equation of a recursive function is asserted as an axiom only when the function is known total, so a non-terminating callee is left uninterpreted rather than admitting a false proof. Proven properties become a lemma library — asserted as axioms in later proofs, composing bottom-up through the hash graph, with relevance filtering so axiom sets are bounded by reachability rather than library size. Z3 "unknown" and timeouts are treated as failure, never as proof.

Integers are unbounded on both sides of the proof: the solver reasons over ℤ, and the kernel's Int is arbitrary precision at runtime too — so a proof carries no "valid modulo overflow" asterisk. Overflow is not a defined answer int64 can't hold; it's an answer we compute. (A compiled program computing 10²⁴ prints the right number, not a wrapped one.)

Rat is ℚ — exact, arbitrary-precision rationals. Decimal literals like 0.1 and fractions like 1/2 are Rat, so 0.1 + 0.2 is exactly 3/10; there is deliberately no Float and no rounding. This is the same lens that made strings structural, pointed the other way. Z3's sequence theory is incomplete, so Str is an inductive datatype proven by induction; Z3's linear real arithmetic is complete, so Rat stays a primitive that translates straight to the Real sort. The payoff is that the algebraic laws IEEE floats violate — associativity, distributivity, exact division-inverse (a/b)*b == a — are proven, not merely tested. Structure where the solver is weak; primitive where it is strong.

Float is the third numeric primitive — IEEE-754 binary64, for bit-level interop with the outside world (opt in with an f suffix, 0.1f). Z3's float theory is complete too, so floats REACH proven: examples/float.oath proves x * 1.0 == x and x + x == x*2 for every float — NaN, ±inf, ±0 included — while 0.1f + 0.2f == 0.3f is falsified, because that sum really is 0.30000000000000004. The kernel refuses to certify a false thing; that is the prover being right, and it is the same property that is proven exact as a Rat. The one subtlety is identity: a content-addressed store needs one canonical form per value, so a Float IS its bit pattern (every NaN canonicalized to one), and structural == is Leibniz equality — NaN == NaN, +0.0 ≠ -0.0 (SMT =), with IEEE's fp.eq kept as a separate opt-in primitive.

The three interconvert explicitly — to-rat, to-float, floor, overloaded by source type. The total, exact directions are provable (Z3 to_real / to_fp / to_int): converting an Int into ℚ and flooring back is a proven identity, and the exact rational 1/10 is proven to round to precisely the 0.1f literal. The narrowings that can fail — Float to Rat or Int on a NaN or infinity — fault at runtime like division by zero, and stay outside the proof fragment.

Two kernels, one spec

oath/ is the Go reference kernel. oathrs/ is an independent Rust kernel, built blind from docs/SPEC.md and the fixtures alone — never the Go source. It passes all six conformance checks, including byte-identical hashes, matching verify transcripts and analyses, and matching proof outcomes. Its independence is preserved deliberately: divergences are fixed in the spec and re-derived by a blind agent, never patched by copying from the reference. Every ambiguity found this way is a recorded spec finding.

The hosted layer

oath serve speaks MCP — over stdio for a local, one-store-per-project setup, or over HTTP for a hosted store. Principals authenticate by an Ed25519 signature over the request body (the principal is the key — unforgeable, no shared secret), with capability-limited bearer tokens as the MCP-client shim (read-only unless granted write). A repoint policy governs what a name may point at — it can require spec/body authorship separation, proven termination, spec-strength floors, reserve a name to a key (owner_pubkey), or defer a name until every property is machine-proven. Objects always store; policy governs only names, so a blocked submission leaves the previous version live.

A reference instance runs at registry.oath-lang.org (deployed from CI; the host is not a root of trust — every proof is re-earned by whoever consumes a definition).

Selecting: the decision package

Finding what satisfies a spec is not the same as knowing whether to use it. oath explain answers the second question: it returns the spec as property content hashes, per-property proof status, spec strength and its freshness, provenance including whether spec and body had independent authors, the exact dependency closure by hash, and — most usefully — the limitations, the recorded reasons not to use an artifact. It is served over MCP as JSON, because the consumer is an agent choosing between candidates.

Everything in it is derived from recorded state, so a definition cannot look better than its evidence. tested is distinguished from proven. Absent mutation evidence is reported as UNMEASURED rather than as a zero score, because “unknown” and “weak” are different claims. Waived mutants are listed with their justifications, so a caller judges the reasoning rather than trusting the number.

The corpus supplies its own argument for why this exists. A spec query for the involution law returns two candidates: reverse, proven 2/2 with 3/3 spec strength, and bad-reverse, which is falsified. Both satisfy the queried property. Search alone cannot separate them; the decision package does, in a form an agent can act on.

Campaign identity: evidence, not assertions

A mutation score of 3/3 answers “how many” and never “out of which mutants, under which policy”. Evidence without a reproducible identity for the computation behind it is an assertion with numbers attached — so a score is attached to the digest of a campaign description: the artifact, the kernel (evaluation semantics decide whether a mutant is caught), the mutant generator revision, the execution budget (a survivor at 60 cases may be a kill at 600), and the waiver policy and set — because waivers count toward the score, so adding one changes the number without changing the code.

A consumer compares digests rather than reasoning about version strings and dates. Equal means MEASURED: the score was produced under the campaign now in force. Different means STALE — authentic evidence, for a reproducible campaign other than the current one. Not false, not expired, and never presented as current.

The registry computes these scores; it never accepts one from a publisher. A client-supplied mutation score would be exactly the publisher-asserts model this substrate replaces. The encoding is normative (SPEC §11), so an auditor can reconstruct a description and check the digest instead of trusting that some hex string is the right one.

Publishing: trust by reproduction

The registry layer needs no trusted server. oath export packs a definition's transitive closure into a single file publishable on any dumb host; oath import refuses any byte that doesn't hash to its name, gate-checks in dependency order, and re-verifies every function locally. Proofs are re-earned, never imported. A registry is just a directory of bundles; all trust lives in the importer.

Discovery: finding proven code by what it does

A registry is only useful if you can draw proven code from it instead of rebuilding — and that means discovery keyed on meaning, not on names (the one non-authoritative layer). It falls out of content-addressing: properties are content-addressed too. A property is stored as (binders, body) with the function as self and de Bruijn binders, so a pure law like commutativity has one canonical hash wherever it appears — “which proven definitions satisfy this spec?” is a hash lookup, not a search.

oath find exposes four name-free modes: by example (who shares a law with this def?), by a fresh spec you write (self is the sought function), matched up to operand types (Int and Rat commutativity match), and — because a property is portable — by proof-implication: append your spec to each same-signature definition and prove it, so commutativity written (== (self b a) (self a b)) still finds + even though its AST differs. One invariant runs through all of it, and guards the eventual e-graph: the discovery layer draws edges over the hash graph; it never touches identity. Semantics is a view, not a redefinition.

Compiling to executables

oath build compiles a definition's dependency closure to a standalone native binary. The provenance gate is the point: an executable is a proof-carrying artifact, or it isn't built — oath build refuses a falsified definition. Compiled programs shed the fuel and depth bounds (those are verification semantics); what they keep is provenance.

The compiler is where the "prove over the structural model, run over a native representation" split happens. A type is proven in whatever form makes it provable — a string is an inductive datatype of codepoints, so its laws discharge by ordinary induction — but at runtime that same value compiles to a native representation: a Str becomes a Go string, not a linked list of boxed characters. Set and Map — distinct types over the sorted-list model they are proven against — likewise compile to native Go hash maps, turning membership and lookup into O(1) operations while the proofs keep reasoning about the sorted list. The two are kept honest by a differential gate — the compiled program must produce exactly what the interpreter does — so the native representation can never quietly disagree with what was proven. The fast execution path and persistent maps for efficient functional updates are the remaining work.

There are two entry protocols. A CLI entry is (-> (List Str) Str), invoked once with argv. A handler is (-> Request Response), invoked per request by the host — so oath build emits a program that serves HTTP. Ingress is deliberately a protocol rather than a capability: a capability is outbound authority a program holds and could misuse, which is why confinement checking exists, but being called is not authority. The host owns the socket, TLS, routing and lifecycle; the artifact stays a pure function of the value it is handed, and inherits every existing gate unchanged.

Either protocol may take a leading capability record. Capabilities are wired with genuine implementations exactly once, at the program boundary — fetch becomes a real HTTP GET, emit a real append to a sink — and everything below that line received authority as an ordinary argument and was verified against every simulated world before the real one arrived. The compiler refuses an entry that is falsified, unverified, or whose capability the confinement checker marks ESCAPES: a program that stores or returns its capability never receives the real one.

The boundary adapter normalizes as little as it can. A request body crosses as raw bytes — (List Int), one Int per byte, deliberately not Str, which is a codepoint list that would corrupt any byte above 0x7F inside the type, where nothing downstream could recover it. That matters because signatures are computed over bytes. Time enters the same way: received-at is a field of the request, supplied once at the boundary, not an ambient clock — so a handler stays deterministic and the property generator quantifies over it for free.

The worked example is webhook: it verifies an HMAC-SHA256 signature over the raw body, rejects a stale timestamp, and emits the validated event — proven properties for the logic, and exactly one trusted component. The crypto primitives sit outside the provable fragment on purpose, because modelling SHA-256 in an SMT solver is not useful even where it is possible, and an axiomatization invented for the purpose would establish facts about the axiomatization rather than about the algorithm. Naming that boundary precisely is worth more than pretending it is not there.