LeanPort Brings Formally Verified Lean 4 Decision Logic Into Go Applications

LeanPort is a small tool that lets developers write decision logic and proofs in Lean 4 and then consume the result from Go as an ordinary package. It targets small but consequential functions, such as authorization checks, whose edge cases tests may miss, since formal proofs cover every input in the modeled domain. The workflow splits into a maintainer path that checks proofs and generates a C/cgo bridge with an idiomatic Go API, and a consumer path where downstream builds need only Go and a C toolchain. The generated files are committed to the repository and treated as build output rather than hand-edited code. The project's example is an authorization policy for a command-line tool, where access depends on facts like authentication, admin status, and resource ownership.