Im Maschinenraum steht heute ein Apparat, der nicht lächelt. Er lächelt schon deshalb nicht, weil er noch prüft. Links fallen Metallstücke mit kleinen Symbolen aus der Rinne, rechts wartet ein Baum aus Schrauben, und irgendwo dazwischen sagt die grüne Lampe: erst wenn der Beweis hält, darf das Teil weiter.
So ungefähr muss man sich Mistrals Leanstral 1.5 vorstellen, wenn man die Presse nicht mit Marketinglack, sondern mit Werkstattlicht anschaut. Mistral meldet in einem offiziellen Beitrag vom 2. Juli 2026 ein frei verfügbares, Apache-2.0-lizenziertes Modell für Lean 4: 119 Milliarden Gesamtparameter, davon 6 Milliarden aktiv. Nicht der größte Kran im Hof, eher ein sehr eigensinniger Prüfarm, der genau wissen will, ob die Schraube wirklich passt.
Der Prüfer bekommt Millionen Token Geduld
Der interessante Teil ist nicht, dass wieder ein Modell einen Pokal auf den Benchmark-Tisch stellt. Davon stehen inzwischen genug herum, manche mit schiefer Gravur. Spannend ist die Richtung: Leanstral 1.5 soll nicht nur Code hinschreiben, sondern mit Lean-Feedback durch Beweise laufen, Dateien ändern, Ziele inspizieren, Fehler hören und wieder ansetzen. Mistral beschreibt dafür Training über Mid-Training, supervised fine-tuning und Reinforcement Learning mit CISPO; im Code-Agent-Setup arbeitet das Modell in einem Dateisystem, nutzt Bash und einen Lean Language Server.
In der Blechpresse-Sprache: Der Agent bekommt keinen hübschen Zauberstab, sondern einen öligen Prüfstand. Wenn das Werkstück nicht kompiliert, fällt es nicht in die PowerPoint-Kiste, sondern zurück in die Walze. Noch einmal. Und noch einmal. Mistral nennt unter anderem 587 von 672 gelöste PutnamBench-Aufgaben, 100 Prozent auf miniF2F, neue Werte auf FATE-H und FATE-X sowie ein FLTEval-Plus gegenüber dem eigenen ersten Leanstral.
Bugjagd mit Schraubzwinge statt Nebelmaschine
Besonders hübsch scheppert der Abschnitt zur Code-Verifikation. Laut Mistral übersetzte eine Pipeline Rust-Code mit Aeneas nach Lean, ließ Leanstral Eigenschaften ableiten und prüfen und fand in 57 getesteten Repositories 47 verletzte Eigenschaften; 11 davon deuteten auf echte Bugs, 5 seien zuvor nicht auf GitHub gemeldet gewesen. Ein Beispiel betrifft Zigzag-Decoding in einer Varinteger-Bibliothek, wo ein Überlauf bei Std.U64.MAX im Debug-Modus kracht und im Release-Modus still die Möbel verrückt.
Das ist natürlich noch kein Zauberbesen, der ab Montag alle Produktionssysteme ausfegt. Formale Methoden bleiben schwer, Lean bleibt Lean, und wer schon einmal einen Beweis mit der falschen Annahme gefüttert hat, kennt dieses Geräusch: sehr leise, sehr teuer. Aber der Trend ist klar. Die KI-Anbieter rücken vom bloßen „schreib mir mal Code“ Richtung „beweise mir, dass dieses Ding hält“.
Für Entwickler bedeutet das weniger Zukunftsmusik als Werkstattordnung. Wenn Agenten länger autonom bauen sollen, brauchen sie nicht nur schnellere Hände, sondern Prüflehren, Compiler, Spezifikationen, Counterexamples und einen Ort, an dem rote Lampen mehr zählen als schöne Antworten. Genau da liegt der Blechpresse-Haken: Die nächste Agentenrunde gewinnt vielleicht nicht der, der am lautesten generiert, sondern der, dessen Maschine am verlässlichsten Nein sagt.
Quellenkasten
Faktenbasis dieses Beitrags: Mistrals offizieller Beitrag zu Leanstral 1.5 vom 2. Juli 2026. Die technischen Angaben sind Anbieterangaben und wurden nicht als unabhängige Benchmark-Prüfung nachgemessen.