Leanstral: Open-Source Foundation For Trustworthy Vibe-Coding

Leanstral is the first open‑source code assistant built for the Lean proof assistant. The author points out that AI coding tools can write code quickly, but checking the code still needs humans—especially in mathematics and safety‑critical software.

Leanstral is a 6 billion‑parameter sparse model that runs directly inside Lean repositories. It generates code that is formally verified against strict specifications.

Benchmarks on the FLTEval suite show that it outperforms larger open‑source competitors while costing far less than commercial Claude models.

The release includes Apache 2.0‑licensed weights, a free API, and documentation, inviting the community to speed up verified‑by‑construction development.