Every definition is a sealed promise.
Oath Language is an AI-native verified-codebase kernel. Definitions are content-addressed by the hash of their canonical form, carry machine-checked properties inside their identity, and live in an immutable object store. The syntax is disposable — the substrate is the product.
The substrate
Code isn't files and folders — it's an immutable graph of content-addressed objects. Each definition arrives with its specification attached. The kernel typechecks it, runs every property, and only then lets a human-readable name point at it.
(data List [a]
(Nil)
(Cons a (List a)))
(defn length [a] [(xs (List a))] Int
(match xs
((Nil) 0)
((Cons h t) (+ 1 (length [a] t))))
(prop non-negative [(xs (List Int))]
(<= 0 (length [Int] xs)))
(prop cons-adds-one [(x Int) (xs (List Int))]
(== (length [Int] (Cons [Int] x xs))
(+ 1 (length [Int] xs)))))
The s-expression syntax is an input format. It elaborates to the canonical AST and is thrown away; oath get projects a fresh one back for human auditors.
Six invariants
Identity, properties, proofs, capabilities, dependencies, metadata — the six things that make a definition a promise rather than a suggestion.
A definition's name is the SHA-256 of its canonical AST. Rename every variable and the hash is unchanged — binders are de Bruijn indices, so formatting and naming diffs cannot exist.
Every definition carries its specification as part of its signature. The kernel refuses ill-typed code at the gate and runs every property before a name is ever trusted.
Properties climb an honest ladder: asserted → tested with deterministic cases → PROVEN for all inputs by Z3, including recursive functions by structural induction.
Effects are capabilities passed as ordinary parameters — the signature is the authority audit. The kernel proves confinement: a capability that never escapes is verdicted so.
Definitions reference each other by hash, forming an acyclic graph. Verdicts — totality, confinement, proofs — compose bottom-up through it like a lemma library.
Names, docs, and guarantees live beside the object, never inside its identity. The store is an immutable object database; names are a mutable index that points into it.
The guarantee ladder
A property doesn't just pass or fail. It sits on a rung, and the rung is recorded in the definition's metadata. Nothing is dressed up as more certain than it is.
The claim exists in the signature.
Inputs seeded from the definition's own hash — reproducible.
SMT-LIB translation, structural induction for recursion.
A wrong definition is a recorded fact, not a hidden bug.
The exhibits kept on purpose
(defn abs-small [] [(x Int)] Int
(if (< x 0) (- 0 x) x)
(prop bounded-wrongly [(x Int)]
(< (abs-small x) 401)))
Passes all 200 test cases; Z3 refutes it at x = -401, an input the generator never draws. This is why the rungs differ.
(defn spin [] [(x Int)] Int
(spin x)
(prop claims-zero [(x Int)]
(== (spin x) 0)))
Non-terminating. The type system accepts it; the termination checker won't bless it; the fuel bound turns the loop into an honest verdict instead of a hang.
(defn sort [] [(xs (List Int))] (List Int)
(match xs
((Nil) (Nil [Int]))
((Cons h t) (insert h (sort t))))
(prop output-is-sorted [(xs (List Int))]
(is-sorted (sort xs)))
(prop preserves-length [(xs (List Int))]
(== (length [Int] (sort xs)) (length [Int] xs)))
(prop preserves-counts [(x Int) (xs (List Int))]
(== (count x (sort xs)) (count x xs)))
(prop idempotent [(xs (List Int))]
(== (sort (sort xs)) (sort xs)))
(prop sorted-is-fixpoint [(xs (List Int))]
(if (is-sorted xs) (== (sort xs) xs) true)))
Proof, not vibes
Authored against the specs of List, length, and append — never their bodies. The permutation oath is the strong one: count x (sort xs) == count x xs. Sorted output plus same length can both hold for wrong code; sorted plus counts-preserved cannot.
Effects as capabilities
No effect system — a capability is just a record of functions passed as an ordinary parameter. Purity is visible as the absence of capability parameters. Properties quantify over generated simulated worlds, and the kernel proves confinement: a capability that is only exercised — never returned, stored, or captured — is verdicted confined.
(defn greet [] [(net {fetch (-> Str Str)}) (id Str)] Str
(++ "Hello, " (++ ((. net fetch) id) "!"))
(prop same-world-same-answer [(net {fetch (-> Str Str)}) (id Str)]
(== (greet net id) (greet net id)))
(prop never-shorter-than-frame [(net {fetch (-> Str Str)}) (id Str)]
(<= 8 (str-len (greet net id)))))
Trust by reproduction
The Go reference kernel and an independent Rust kernel — the second built blind from the specification and fixtures alone, never the Go source. They agree on every hash, every verdict, and all six conformance checks. When identity is a hash, no server has to be trusted; a definition is verified by reproducing it.
The normative kernel and CLI. Typechecker, evaluator, prover, mutation tester, content-addressed store, MCP server.
An N-version implementation from SPEC.md + fixtures only. Every ambiguity it surfaced is a recorded spec finding.
Byte-identical hashes, verify transcripts, analyses, and every proof outcome must match across both kernels, on every change.
The playground is the real verified corpus — 56 definitions with their actual content hashes and Z3 verdicts. Nothing mocked.