While Lean is primarily known for theorem proving, I believe its dependent-types and formal verification features make it the ideal target for AI Agents to generate provably correct code [0].

Lean-pq uses FFI to bind to libpq, but leverages Lean’s type system to move database errors from runtime to compile-time:

- Compile-time SQL Validation: Uses Lean’s macro system to check SQL strings against your schema during the build. Misspelled columns or type mismatches cause a build failure.

- Monadic Permission Tracking: An effect-tracking monad distinguishes between Read-Only and Read-Write operations. You can statically guarantee a function won't modify the DB: def getUser (id : Int) : DB .ReadOnly User.

- Zero-Overhead FFI: Battle-tested libpq performance with Lean 4 ergonomics.

The goal is to eliminate runtime surprises—syntax errors, permission violations, and null-mismatches—at the compilation phase. I’d love to hear feedback from anyone exploring Lean 4 for systems programming.

Project: https://github.com/typednotes/lean-pq

[0] https://ngrislain.github.io/projects/2026-3-12-dont-vibe--pr...