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. 232 definitions, 635 properties, 382 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-after
Other
bytes-ok
Other
bytes-prefix
Other
bytes-str
Other
caps-with
Other
check-config
Other
circle
Other
clamp
Numbers
config-has-key
Other
config-key
Other
config-missing
Other
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
gh-by-count
Other
gh-count-of
Other
gh-counts
Other
gh-dedup
Other
gh-drop-final-empty
Other
gh-field
Other
gh-group
Other
gh-group-labels
Other
gh-header
Other
gh-header-line
Other
gh-label-of
Other
gh-line-ok
Other
gh-log-lines
Other
gh-record
Other
gh-refusal
Other
gh-refused-lines
Other
gh-rejected
Other
gh-render-group
Other
gh-render-groups
Other
gh-report
Other
gh-report-main
Other
gh-request
Other
gh-schema
Other
gh-sign
Other
gh-signature
Other
gh-spec-secret
Other
gh-summary
Other
gh-tally
Other
gh-webhook
Other
greet
Strings & records
greet-or-guest
Strings & records
hdr-probe
Other
header-first
Other
header-or
Other
hex-decode
Other
hex-decode-unchecked
Other
hex-digit
Other
hex-encode
Other
hex-nibble
Other
hex-valid
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
json-scoped-string
Other
json-string-value
Other
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
media-type-is
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
no-field-can-inject
Other
one-two-three
Other
or-else
Strings & records
parse-nat
Other
parse-nat-go
Other
path-is
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
record-field
Other
record-is-well-formed
Other
record-under
Other
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
secret-is-usable
Other
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
smi-insert
Other
smi-keys
Other
smi-lookup
Other
smi-merge
Other
smi-values
Other
snoc
Other
sort
Sorting
sort-by
Other
spin
Honest exhibits
str-append
Strings & records
str-bytes
Other
str-code
Other
str-drop
Strings & records
str-eq
Other
str-join
Strings & records
str-len
Strings & records
str-lt
Other
str-map-empty
Other
str-map-has
Other
str-map-insert
Other
str-map-lookup
Other
str-map-merge
Other
str-map-size
Other
str-nub
Other
str-pad-left
Other
str-prefix
Strings & records
str-scalars
Other
str-spaces
Other
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.