Formal-Methods · AI Beat

04 Jul 2026 · AI Beat Desk

miniF2F Hits the Ceiling

Mistral's Leanstral 1.5 scores 100% on miniF2F and solves 587 of 672 Putnam Competition problems using a 6B-active-parameter MoE. The model saturates the main formal-proof benchmark and finds real bugs in production code — at roughly $4 per Putnam problem versus competitors charging $300.

09 May 2026 · AI Beat Desk

LLMs Know the Raft Paper. They Don't Know Etcd.

SysMoBench, a new benchmark from the Specula team, tests whether LLMs can produce TLA+ formal specifications that accurately model the behavior of real distributed system implementations. They score near-perfect on syntax and only ~46% on conformance and ~41% on invariant checking — because they model the algorithm as described in papers, not as implemented in code.