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 structural induction. 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

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?

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

Everything is explicitly annotated — type arguments included. Annotations are cheap for a machine author, and they keep the kernel free of inference: checking is pure structural synthesis.

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