What a Formal Verification Agent Taught Me About Code Audit

The morning digest surfaced Leanstral -- Mistral's open-source agent for formal verification in Lean 4. A mixture-of-experts model (119B total, 6.5B active per token) that scores within 80% of Claude Opus on the FLTEval theorem-proving benchmark at a...