Quickstart

The kernel is dependency-free Go. You need Go ≥ 1.25 and z3 on your PATH (brew install z3) for proofs.

Build

shell

git clone https://github.com/miclip/oath-lang
cd oath-lang
cd oath && go build -o oath . && cd ..

Put your first definition

put elaborates the surface syntax to the canonical AST, typechecks it, stores the object, and runs every property before the name is trusted.

shell

./oath/oath put examples/list.oath   # elaborate → typecheck → store → verify
./oath/oath ls                       # names, hashes, guarantees
./oath/oath get reverse              # human projection of a definition
./oath/oath eval '(reverse [Int] (Cons [Int] 1 (Cons [Int] 2 (Nil [Int]))))'

Watch a wrong definition get caught

bad_reverse returns its input unchanged. Its involution property passes — a lesson about weak specs — but the append law falsifies it, and the kernel prints a counterexample and records the definition as FALSIFIED.

shell

./oath/oath put examples/bad_reverse.oath

Prove it for all inputs

prove translates properties to SMT-LIB and asks Z3 to hold them for every input — including recursive functions, by induction (structural, lexicographic, and recursion induction for integer-counter recursion). Proven properties become a lemma library for later proofs.

shell

./oath/oath put examples/sort.oath
./oath/oath prove sort               # discharge insertion sort's correctness to Z3

Compile it to a native binary

build lowers a definition's dependency closure to a standalone native executable — but only if it's proof-carrying; it refuses a falsified or unverified entry point. Proven over the structural model, run over a native representation (a Str is a codepoint datatype for proofs, a Go string at runtime), kept honest by a differential gate against the interpreter.

shell

./oath/oath build main-echo -o echo   # entry: (List Str) -> Str, proof-carrying
./echo one two three                  # runs native — no fuel or depth bounds

The agent interface

Three verbs turn the store into what an AI author actually consumes — queries and transactions instead of files.

shell

./oath/oath context sort append --budget 500   # spec-only slice: signatures,
                                               # props, guarantees — never bodies
./oath/oath put --json examples/sort.oath      # machine-readable verdicts
./oath/oath dependents append                  # reverse dependency query
./oath/oath mutate length                      # spec strength: do the properties
                                               # notice mutations of the body?
./oath/oath explain reverse                    # decision package: evidence,
                                               # provenance, and the LIMITATIONS
./oath/oath explain reverse --json             # same, for an agent to consume

The MCP server (oath serve) exposes all of this over stdio, so any agent session can mount the substrate as native tools. The repo's .mcp.json registers it for Claude Code automatically.

The surface syntax

Every binder is annotated; type arguments may be omitted and are inferred. Annotations are cheap for a machine author, and checking stays bidirectional local synthesis — no full inference, no unification of two unknowns.

a full definition

(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))))