Live corpus
The playground is the proof ledger.
This isn't a sandbox with fake data. Every row below is a real definition from the committed Oath store — its content hash is the actual SHA-256 identity, and each verdict is the actual outcome the kernel recorded when it ran oath prove over the corpus. 56 definitions, 207 properties, 134 proven for all inputs by Z3.
Insertion sort, fully proven correct
Authored against the spec of List/length/append — never their bodies. The permutation oath (count preserved) is the strong property: sorted + same-length can both hold for wrong code; sorted + counts-preserved cannot.
(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)))
- Proven by structural induction, discharged to Z3 over unbounded integers.
- idempotent and reverse-invariant go through a four-lemma plan: insert commutativity, the sorted-head no-op, snoc-is-insert, and the sorted-fixpoint theorem.
Standing caveat, kept honest: Z3 reasons over unbounded integers; the evaluator uses int64. Division stays outside the proof fragment on purpose — the kernel truncates while SMT-LIB is Euclidean, so a "proof" would certify the wrong theorem. A proof is valid modulo overflow, and the corpus says so.