Leanstral von Mistral AI: die KI, die beweist, dass Ihr Code korrekt ist

Am 16. März 2026 hat Mistral AI Leanstral veröffentlicht, den ersten Open-Source-KI-Agenten, der speziell für Lean 4 entwickelt wurde, einen formalen Beweisassistenten, der sowohl in der Mathematik als auch in der Softwareentwicklung verwendet wird. In einem Kontext, in dem sich die Werkzeuge zur Codegenerierung durch KI vermehren, sticht Leanstral durch ein radikales Versprechen heraus: nicht nur Code generieren, sondern mathematisch beweisen, dass er korrekt ist.

Aber warum sollten Sie sich für formale Verifikation interessieren? Wie sind die realen Benchmarks von Leanstral im Vergleich zu Claude und den Open-Source-Modellen? Und vor allem, welche konkreten Anwendungen eröffnet diese Technologie für Unternehmen und technische Teams? Dieser Leitfaden gibt einen Überblick.

Die KI-Agenten zur Codegenerierung (Copilot, Cursor, Claude Code) produzieren in den meisten Fällen funktionsfähigen Code. Aber in kritischen Bereichen (Luftfahrt, Finanzen, Smart Contracts, mathematische Forschung) reicht „scheint zu funktionieren“ nicht aus. Die menschliche Überprüfung von KI-generiertem Code ist teuer, langsam und erfordert seltene Fachkenntnis.

Leanstral schlägt eine Alternative vor: Der Agent schreibt den Code und produziert einen formalen Beweis seiner Korrektheit. Der Lean-4-Compiler fungiert als binärer Verifizierer. Entweder der Beweis kompiliert oder er kompiliert nicht. Keine Grauzone.

Lean 4, entwickelt von Leonardo de Moura (ehemals Microsoft Research), ist sowohl ein Beweisassistent als auch eine funktionale Programmiersprache. Es wird verwendet von Google DeepMind (AlphaProof, Silbermedaille bei der Internationalen Mathematik-Olympiade 2024), Amazon (Verifikation von Cedar) und einer Community von mehr als 10.000 Mitgliedern auf Zulip.

Die Mathlib-Bibliothek, die die Mathematik in Lean formalisiert, zählt mehr als 20.000 Beiträge und hat 2025 Finanzierungen in Höhe von 15 Millionen Dollar erhalten.

Leanstral basiert auf einer Sparse-Mixture-of-Experts-(MoE)-Architektur mit folgenden Eigenschaften:

Das Prinzip ist einfach: Jeder Token aktiviert nur 4 der 128 Expertenmodule. Leanstral profitiert somit von der Wissenskapazität eines Modells mit 119 Milliarden Parametern, aber zu den Inferenzkosten eines Modells mit 6,5 Milliarden. Dieses Effizienzverhältnis von 18x ermöglicht es ihm, drastisch niedrigere Kosten als die Konkurrenz anzubieten.

Im Gegensatz zu generalistischen Modellen, die Text produzieren, der wie Lean-Code aussieht, interagiert Leanstral direkt mit dem Lean-4-Compiler über das MCP-Protokoll (Model Context Protocol). Konkret kann der Agent:

• Die Typen im Lean-Compiler überprüfen

• Beweistaktiken ausführen und die Ergebnisse beobachten

• Die Fehlermeldungen analysieren

• Die Beweise iterativ in einer interaktiven Schleife verfeinern

Diese native Integration ist ein entscheidender technischer Vorteil. Das Modell „rät“ die Beweise nicht, es konstruiert sie im Dialog mit dem Verifizierer.

Mistral AI hat FLTEval eingeführt, ein neues Benchmark, das entwickelt wurde, um die Fähigkeit zu bewerten, Beweise in echten Code-Repositories zu produzieren. Es stützt sich auf das FLT-Projekt (Fermat's Last Theorem) des Imperial College London, geleitet von Professor Kevin Buzzard, ein Formalisierungsprojekt mit 55 Mitwirkenden und finanziert vom EPSRC bis 2029.

Im Gegensatz zum MiniF2F-Benchmark (das isolierte Probleme aus mathematischen Wettbewerben ins Visier nimmt) misst FLTEval die Fähigkeit, formale Beweise in einer realistischen Umgebung mit Imports, Bibliotheksabhängigkeiten und mehrdateilichen Beweisstrukturen zu vervollständigen.

Die Zahlen sprechen für sich:

• Leanstral pass@2 (36 $) übertrifft Sonnet 4.6 (549 $) um 2,6 Punkte, bei 15 Mal weniger Kosten.

• Leanstral pass@2 übertrifft Haiku 4.5 (184 $) um 3,3 Punkte, bei 5 Mal weniger Kosten.

• Leanstral pass@16 (290 $) übertrifft Sonnet um 8 Punkte, zum halben Preis.

• Claude Opus 4.6 bleibt der Marktführer bei roher Qualität (39,6), kostet aber 1.650 $, also 46 Mal mehr als Leanstral pass@2.

Mit nur 6,5 Milliarden aktiven Parametern übertrifft Leanstral Modelle, die 5- bis 6-mal mehr mobilisieren. Qwen3.5 benötigt 4 Versuche und 17 Milliarden aktive Parameter, um 25,4 zu erreichen. Leanstral übertrifft diesen Wert bereits beim zweiten Versuch.

Bugs im DeFi-Code haben in den letzten Jahren Milliarden von Dollar gekostet. Die formale Verifikation ist der Referenzstandard, um zu garantieren, dass ein Smart Contract genau das tut, was er verspricht. Mit Leanstral sinken die Kosten eines formalen Audits drastisch: ein Korrektheitsbeweis für 36 $ statt Hunderten von Dollar bei den proprietären Alternativen.

In Branchen, in denen ein Softwarefehler Leben oder Millionen kosten kann, ist die formale Verifikation kein Luxus, sondern eine regulatorische Pflicht. Leanstral ermöglicht es Entwicklungsteams, das erwartete Verhalten in Lean 4 zu spezifizieren und dann automatisch die Konformitätsbeweise zu generieren. Der Compiler überprüft anschließend, ob der Beweis gültig ist.

Das FLT-Projekt (Formalisierung des großen fermatschen Satzes) und Mathlib veranschaulichen das Potenzial von Leanstral, die formalisierte Forschung zu beschleunigen. Forscher können routinemäßige Beweise an den Agenten delegieren und sich auf die kreativen Aspekte der Forschung konzentrieren.

Einer der von Mistral AI demonstrierten Anwendungsfälle ist die Übersetzung von Beweisen aus Rocq (früher Coq) nach Lean 4, wobei die Semantik und die Notationen erhalten bleiben. Dies erleichtert die Migration akademischer oder industrieller Projekte von einem Ökosystem zum anderen.

Der strategisch wichtigste Anwendungsfall: formal zu überprüfen, dass der von KI-Agenten (Copilot, Cursor usw.) produzierte Code korrekt ist. Leanstral verkörpert die Vision des „trustworthy vibe coding“, bei dem der Mensch spezifiziert, was er will, und die Maschine die Konformität beweist.

Der Befehl /leanstall im Mistral-Vibe-CLI (Version 2.5.0, veröffentlicht am 16. März 2026) konfiguriert den Leanstral-Agenten automatisch. Das ist der schnellste Weg zum Testen.

Der Endpunkt labs-leanstral-2603 ist für eine begrenzte Zeit kostenlos verfügbar. Mistral AI möchte echte Nutzungsrückmeldungen sammeln, um zukünftige Versionen zu verbessern.

Die Modellgewichte werden unter Apache-2.0-Lizenz auf Hugging Face veröffentlicht (mistralai/Leanstral-120B-A6B-2603). Empfohlene Konfiguration: 4 GPUs A100 80 GB oder H100, mit vLLM und Flash Attention. Hinweis: Die Hugging-Face-Seite zeigte zum Zeitpunkt der Veröffentlichung einen vorübergehenden 404-Fehler.

Leanstral wurde ausschließlich für Lean 4 entwickelt. Es ersetzt nicht Ihre generalistischen Codierungswerkzeuge (Copilot, Claude Code, Cursor). Wenn Sie einen Assistenten zum Schreiben von Python, TypeScript oder SQL suchen, ist dies nicht das richtige Werkzeug.

Mit einem FLTEval-Score von 39,6 gegenüber 31,9 für Leanstral pass@16 behält Opus einen signifikanten Vorsprung. Wenn Ihre absolute Priorität die maximale Präzision ist und das Budget keine Einschränkung darstellt, bleibt Opus die beste Wahl. Die Hacker-News-Community hat diesen Punkt übrigens hervorgehoben: Ein speziell für diese Aufgabe trainiertes Modell sollte theoretisch ein generalistisches Modell übertreffen.

Einige Beobachter merken an, dass der Leistungsgewinn von Leanstral sich jenseits von pass@8 zu verringern scheint. Der Übergang von pass@8 (31,0) zu pass@16 (31,9) stellt nur einen Gewinn von 0,9 Punkten bei einer Verdopplung der Kosten dar.

Das Selbst-Hosting erfordert 4 High-End-GPUs (A100 oder H100), was eine erhebliche Hardware-Investition darstellt. Für Teams ohne diese Infrastruktur bleiben die kostenlose API oder Mistral Vibe die zugänglichsten Optionen.

Leanstral füllt eine echte Lücke im Ökosystem. Vor seiner Veröffentlichung beschränkten sich die Optionen für die KI-unterstützte formale Verifikation auf teure proprietäre Modelle (Claude Opus) oder auf generalistische Modelle, die nicht für Lean 4 optimiert sind.

Leanstral positioniert sich an der Schnittstelle dreier Qualitäten: Open Source (Apache 2.0), speziell für das Beweis-Engineering trainiert, und wirtschaftlich. Kein anderes Modell besetzt derzeit diesen Platz.

Für CTOs und technische Verantwortliche, die die formale Verifikation als Bestandteil ihrer Strategie zur Softwarequalität bewerten, stellt Leanstral einen zugänglichen Einstiegspunkt dar. Für Forscher in formalisierter Mathematik ist es ein Beschleuniger. Und für das Lean-4-Ökosystem als Ganzes ist es ein starkes Signal, dass auf formale Beweise spezialisierte KI dabei ist, eine praktische Realität zu werden.

Die wahre Frage ist nicht mehr „Ist die KI-unterstützte formale Verifikation möglich?“, sondern „Wie produktionsreif ist sie?“. Mit Leanstral liefert Mistral AI ein erstes Antwortelement.