Leanstral 1.5: Proof Abundance for All

Leanstral 1.5 uses attempted mathematical proofs to investigate software behavior. Mistral AI describes a bug-finding pipeline that translates Rust code into Lean, a language for machine-checked proofs. The model proposes properties the code should satisfy and attempts to prove them. If those attempts fail, it tries to prove the opposite.

Across 57 repositories, the company reports 47 violated properties, of which 11 indicated genuine bugs, including five previously unreported ones. That gap matters: disproving a proposed property does not automatically identify a software defect, because the proposed requirement itself may be wrong. The result supports proof-assisted investigation of specific behaviors, rather than certification of entire repositories.