SymCrypt ist Microsofts zentrale kryptographische Bibliothek, die in zahlreichen Produkten und Diensten des Unternehmens eingesetzt wird – von Windows bis zu Azure-Diensten. Mit der zunehmenden Nutzung von Rust für sicherheitskritischen Systemcode stellt sich die Frage, wie formale Korrektheitsgarantien bereits während der Entwicklung – und nicht erst nachträglich – sichergestellt werden können. Microsoft Research präsentiert einen Ansatz, der die Lücke zwischen formalen Kryptographie-Standards (etwa NIST-Spezifikationen) und der tatsächlichen Rust-Implementierung systematisch schließt. Kernidee ist eine kontinuierliche Verifikation direkt im Entwicklungsprozess: Entwickler erhalten Rückmeldung zur formalen Korrektheit, während sie den Code schreiben, ohne auf Geschwindigkeit oder Anpassbarkeit der Bibliothek verzichten zu müssen. Damit geht der Ansatz über klassische Post-hoc-Verifikation hinaus, bei der formale Beweise erst nach Fertigstellung des Codes erstellt werden und Änderungen am Code aufwändige Re-Verifikationen erfordern. Der Fokus liegt auf der Aufrechterhaltung der Verifikation auch dann, wenn sich der Code im Zuge von Weiterentwicklungen ändert – ein häufiges Problem bei lebenden Kryptographie-Bibliotheken. Der Beitrag richtet sich sowohl an Forscher im Bereich formaler Methoden als auch an Praktiker, die sicherheitskritischen Kryptographie-Code in Rust entwickeln und warten.