Monogate

Monogate is a workbench for EML, a single-operator math language where every expression reduces to one primitive function. Write kernels with contracts, compile them to multiple targets, and have Lean verify your theorems automatically. The platform includes an interactive electronics lab for hands-on hardware courses, a compiler available via pip, and reproducible examples you can run locally.

Designed for researchers and engineers working with formal verification, the system lets you write mathematical specifications, generate optimized code for different platforms, and check proofs in Lean 4. The maker reports building it with Claude and Grok, combining 36 hours of development with empirical results including a 108-node machine-precision implementation of sin(x).