Kategorie:
Formale Verifikation
Formale Methoden, Proof Assistants und verifizierbare Software.
-
Der Kryptoschrauber lässt den Beweisstempel auf Rust fallen
Im Kryptokeller fällt ein schwerer Stempel auf Rust-Code: Microsoft Research zeigt, wie SymCrypt mit Lean, Aeneas und maschinengeprüften Beweisen aus dem Teststand in die Beweiswerkstatt rollt.
-
Der Beweisautomat hört erst auf, wenn die Schraube wirklich passt
Mistral schiebt Leanstral 1.5 in die Werkstatt: ein offenes Modell für Lean-4-Beweise, Code-Verifikation und die Sorte Geduld, bei der die Prüflampe erst grün wird, wenn das Metall nicht mehr lügt.