-
Notifications
You must be signed in to change notification settings - Fork 1
Home
MesTTo edited this page Jun 19, 2026
·
2 revisions
LeaTTa is a Lean 4 formalization of Hyperon's minimal MeTTa interpreter, the small "assembly language" that the rest of MeTTa is built on, together with a machine-checked metatheory layer.
The textbook-style treatment is the LeaTTa book. It covers the object language, the interpreter, the type system, the metatheory, the operational semantics and its correspondence to the kernel, and the blockchain angle. Start there.
- The book: https://mestto.github.io/LeaTTa/
- Repository and README: https://github.com/MesTTo/LeaTTa
- Install and run: INSTALL.md
This wiki has two pages. Everything conceptual is in the links above.
See the Developer Guide for the Lean toolchain, libraries, and proof machinery to use when contributing to LeaTTa.