Live · runs in your browser

Paste a definition. Watch the kernel judge it.

This is the actual Oath kernel compiled to WebAssembly — the same gate that runs on the command line. It typechecks your definition, runs every property on 200 deterministic cases, and reports an honest verdict. Then Prove runs the real Z3 solver, also in your browser, to prove a novel definition for all inputs — direct and by induction. Nothing here is mocked. Loading kernel…

Verify is the gate — typecheck, 200 deterministic hash-seeded cases per property, and the termination/confinement analyses — reported as an honest tested. Paste a corpus definition verbatim (like the sort example) and its content hash matches, surfacing that definition's recorded PROVEN. Prove runs the real prover — direct, structural induction, the lemma fixpoint — discharging every obligation to Z3 (the same 4.16.0 the corpus used) compiled to WebAssembly and running in a worker beside the kernel. A proof is valid modulo int64 overflow, and the report says so.