formal verification made accessible?
A proof assistant for the mathematician.
Start Formalizing
Starling is an interactive theorem prover designed for human intuition, not just programming expertise or automation.
A Language for Insight
Starling enables mathematicians without a background in functional programming to formalize mathematical results. Built on top of Norman Megill's Metamath and inspired by Isabelle/Isar, the Starling language offers readable syntax that is natural to write or think in.