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. 164 definitions, 416 properties, 339 proven for all inputs by Z3.

This is the ledger of what's already proven. To run your own definition through the real kernel — live, in your browser — try it →

elaborate
s-expr → canonical AST
hash
SHA-256 of the O1 encoding
typecheck
bidirectional synthesis
test
200 seeded cases
prove
Z3, all inputs
abs
Numbers
abs-small
Honest exhibits
all
Other
any
Other
append
Lists
bad-reverse
Honest exhibits
bytes-ok
Other
circle
Other
clamp
Numbers
contains
Lists
count
Lists
count-append
Other
count-by
Other
count-matching
Other
drop
Lists
drop-while
Other
e-div
Numbers
e-mod
Numbers
echo-handler
Other
embed-add
Numeric conversions
excluded-witness
Other
f-double
Floats
f-mul-id
Floats
f-scale-inv
Other
f-tenths
Floats
fib
Other
filter
Other
find
Other
first-or
Other
flat-map-option
Other
flatten
Other
foldl
Other
foldr
Other
full-name
Strings & records
greet
Strings & records
greet-or-guest
Strings & records
header-first
Other
hex-decode
Other
hex-digit
Other
hex-encode
Other
hex-nibble
Other
hmac-kat-rfc4231-2
Other
i-contains
Intervals
i-hull
Intervals
i-intersect
Intervals
i-overlaps
Intervals
index-of
Other
init
Other
initials-or
Strings & records
insert
Sorting
insert-by
Other
int-embed
Numeric conversions
is-none
Other
is-some
Other
is-sorted
Sorting
join-with
Strings & records
kv-get
Worlds & state
kv-put
Worlds & state
last
Other
length
Lists
lengths
Lists
list-eq-by
Other
main-echo
Programs & capabilities
main-fetch
Programs & capabilities
map
Lists
map-empty
Map (native-compiled)
map-err
Other
map-has
Map (native-compiled)
map-insert
Map (native-compiled)
map-keys
Map (native-compiled)
map-lookup
Map (native-compiled)
map-merge
Map (native-compiled)
map-option
Other
map-result
Other
map-size
Map (native-compiled)
map-values
Map (native-compiled)
max-by
Other
max2
Numbers
maximum
Other
merge
Sorting
mi-insert
Map (native-compiled)
mi-keys
Map (native-compiled)
mi-lookup
Map (native-compiled)
mi-merge
Map (native-compiled)
mi-values
Map (native-compiled)
min-by
Other
minimum
Other
one-two-three
Other
or-else
Strings & records
parse-nat
Other
parse-nat-go
Other
pow
Other
product
Other
q-drop
Queue
q-peek
Queue
q-push
Queue
q-to-list
Queue
range
Other
rat-add
Rationals
rat-floor
Numeric conversions
rat-mul
Rationals
rat-recover
Rationals
rename-key
Worlds & state
replicate
Other
req-body
Other
req-headers
Other
req-method
Other
req-path
Other
req-received-at
Other
reverse
Lists
reverse-onto
Other
rle-decode
Run-length coding
rle-encode
Run-length coding
rle-expand
Run-length coding
rot
Programs & capabilities
rot-f
Programs & capabilities
rot-h2
Programs & capabilities
rot-h3
Programs & capabilities
rot-hl
Programs & capabilities
safe-get
Worlds & state
set-add
Set (native-compiled)
set-elems
Set (native-compiled)
set-empty
Set (native-compiled)
set-inter
Set (native-compiled)
set-member
Set (native-compiled)
set-size
Set (native-compiled)
set-union
Set (native-compiled)
shout
Strings & records
show-int
Other
show-nat
Other
si-insert
Set (native-compiled)
si-inter
Set (native-compiled)
si-member
Set (native-compiled)
si-union
Set (native-compiled)
sign
Numbers
singleton
Other
snoc
Other
sort
Sorting
sort-by
Other
spin
Honest exhibits
str-append
Strings & records
str-bytes
Other
str-drop
Strings & records
str-join
Strings & records
str-len
Strings & records
str-prefix
Strings & records
str-split
Strings & records
str-split-join
Strings & records
str-take
Strings & records
sum
Lists
swap
Other
t-flatten
Trees
t-insert
Trees
t-member
Trees
t-size
Trees
take
Lists
take-while
Other
tenth-f
Numeric conversions
third-f
Other
unwrap-or
Other
webhook
Other
within-window
Other
zip
Other
zip-with
Other

Insertion sort, fully proven correct

sort
proven · total
sha2568ed4b7e956f376fb0f06f5a72f90e76be50ddb02da09045ea9bb8f8dafeb2760

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.

sort
(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)))
7 / 7 properties proven · Sorting
provenoutput-is-sorted
provenpreserves-length
provenpreserves-counts
provensnoc-is-insert
provensorted-is-fixpoint
provenidempotent
provenreverse-invariant
  • 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.