Smart contract verification
Verity Lang
Write or import smart contracts, prove their properties in Lean, and compile them toward the EVM through verified compiler layers.
Built for the work
Shared with everyone
Formal verification in Lean exposes gaps in the tooling. We build what we need to get past them, then open-source it for others doing the same work.
Lean verification infrastructure
turbo-lean
Incremental verification and counterexample triage for Lean 4. Re-check what changed and give proof-search agents a tighter feedback loop.