Tutorials
Learn the substrate by doing. Each walkthrough runs real commands against the committed store and shows the actual output — start at the top for a path from “what is a verdict?” to “find proven code by what it does.”
The guarantee ladder
asserted → tested → proven → falsified, and mutation testing — how much a verdict actually means, on real definitions.
Numbers you can trust
Int (no overflow), exact Rat, IEEE Float — and the same 0.1 + 0.2 == 0.3 proven for one and falsified for the other.
Names aren't identity
put, hashes, repointing — why a name collision can never silently change what your code computes.
Writing and proving a function
Author str-append from scratch, state its laws, watch Z3 prove them, and check the spec is actually tight.
A compiled circle calculator
Read a radius, print the area over exact rational π, compiled to a native binary — the whole stack in one program.
Finding proven code by what it does
The four find modes end to end — by example, by a fresh spec, by proof, and by the e-graph — with no name trusted.