Im Kryptokeller steht heute kein Praktikant mit Klemmbrett, sondern eine Presse mit schwerem Stempel. Sie riecht nach altem Öl, nach Serverlüfter und nach diesem besonderen Moment, wenn jemand sagt: Testen reicht uns nicht mehr, wir wollen es bewiesen haben. Zack. Schlüsselrohling rein. Beweis drauf. Weiter.
Anlass ist ein Beitrag von Microsoft Research vom 13. Juli 2026: Das SymCrypt-Team beschreibt, wie neue kryptografische Implementierungen in Rust geschrieben und mit Lean sowie Aeneas formal verifiziert werden. SymCrypt ist Microsofts offene Kryptobibliothek, die laut Microsoft in Produkten und Diensten wie Windows und Azure Linux steckt. Also nicht bloß Laborblech hinter Glas, sondern Werkzeug, das irgendwann im Maschinenraum mitläuft.
Der Unterschied zwischen „hat meistens funktioniert“ und „der Schraube wurde nachgerechnet“
Kryptografie ist diese Sorte Infrastruktur, die erst auffällt, wenn sie fehlt oder falsch herum eingebaut wurde. Ein winziger Rechenfehler, ein fehlender Grenzenzaun im Speicher, ein Zustand, der einmal falsch abbiegt: schon steht die Tür nicht offen, sie hängt gleich mit Rahmen im Flur.
Microsoft beschreibt deshalb eine Kette, die fast bürokratisch schön quietscht: öffentliche Standards werden in Lean-Spezifikationen übersetzt, Testvektoren prüfen die Abschrift, Aeneas hilft dabei, einen größeren Teil von Rust-Code in die Beweiswelt zu bringen, und am Ende sollen nicht nur Tests nicken, sondern maschinengeprüfte Beweise sagen: Diese Implementierung macht, was der Standard behauptet. Wenig Glamour, viel Schraubstock.
Für den ersten öffentlichen Schwung nennt Microsoft SHA-3 und ML-KEM. Gerade ML-KEM gehört in die postquantenfeste Ecke, also in jenen Regalabschnitt, den man nicht erst aufräumen möchte, wenn der Quanten-Gabelstapler schon piept. Außerdem erwähnt der Beitrag, dass weitere Rust-native Algorithmen wie AES-GCM, FrodoKEM und ML-DSA in diese Richtung wandern sollen.
Rust macht den Zaun, Lean zählt die Schrauben
Rust ist hier nicht der Zauberhut. Rust hilft gegen ganze Klassen von Speicherfehlern, ja. Aber Kryptocode besteht nicht nur aus Speicher, sondern aus Mathematik, Randfällen, Optimierungen, Architekturkniffen und kleinen Schleifen, die aussehen, als hätte jemand eine Norm mit der Blechschere gefaltet. Lean liefert dann die Schicht, in der diese Faltung gegen eine formale Spezifikation gehalten wird.
Interessant ist auch die Rolle der Agenten. Microsoft spricht davon, dass KI-Agenten beim Skalieren der Beweisarbeit helfen können, indem sie Beweise oder Zwischenbehauptungen schreiben, die anschließend unabhängig verifiziert werden. Das ist ein hübscher Satz für den Maschinenraum: Der Roboter darf schrauben, aber die Mutter muss nachher in das Gewinde passen. Sonst zählt es nicht.
Warum das für normale Menschen nicht egal ist
Weil Kryptografie selten als App-Icon daherkommt. Sie sitzt unter Betriebssystemen, Cloud-Diensten, Firmware, Messengern und Protokollen. Wenn diese untere Schicht besser geprüft wird, merkt man im Alltag hoffentlich nichts. Genau das ist der Witz: Gute Infrastruktur ist oft die, die nicht dramatisch auf die Bühne fällt.
Natürlich ersetzt so ein Verfahren nicht jede menschliche Prüfung. Standards müssen korrekt formalisiert werden, Annahmen müssen stimmen, die Werkzeuge haben ihren eigenen Maschinenpark. Aber der Schritt ist trotzdem bemerkenswert: Verifikation rutscht näher an die Produktentwicklung heran, weg vom Sonderlabor mit weißen Handschuhen, hin zur Werkbank, wo der Code ohnehin liegt.
Die Blechpresse notiert: Wenn Kryptocode künftig mit Stempelkarte, Rust-Zaun und Lean-Prüfhammer aus der Halle kommt, darf man das ruhig Fortschritt nennen. Nicht mit Fanfare. Eher mit einem trockenen Klack. Und danach wird weitergeschraubt.