Mistral AI vydal Leanstral 1.5, volně dostupný model pod licencí Apache-2.0 zaměřený na formální verifikaci kódu. Model má 119 miliard parametrů, z nichž je vždy aktivních pouze 6 miliard. Leanstral 1.5 dosahuje na benchmarku PutnamBench 587 vyřešených úloh z 672 a saturuje test miniF2F na 100 %. V praxi model odhalil 5 dříve neznámých chyb v 57 testovaných open-source repozitářích. Trénink probíhal ve třech fázích: mid-training, supervised fine-tuning a reinforcement learning s metodou CISPO. Model je k dispozici na Hugging Face a prostřednictvím bezplatného API. Cena za vyřešení jedné Putnamovy úlohy činí zhruba 4 dolary, zatímco u srovnatelných nástrojů jako Seed-Prover přesahuje 300 dolarů.
