lean 4
Introducing LeanPort: Bring Proven Lean 4 Modules into Your Go Projects
LeanPort compiles Lean 4 modules and their proofs into a Go package, so ordinary Go code can call logic checked against a stated rule for every input. A six-example tour, from one function to a verified authorization tool.