Amazon prüft Rust-Code jetzt mathematisch mit Verus

Developing provably correct Rust code with Verus

Rust verhindert viele Fehler, doch "mehr Sicherheit" ist nicht dasselbe wie "tatsächlich korrekt". Verus, ein Open-Source-Programmverifier von Amazon, prüft Rust-Code gegen eine formale mathematische Spezifikation – für alle möglichen Eingaben und weit über klassische Tests hinaus. Entwickler annotieren ihren Quellcode direkt mit Vor- und Nachbedingungen, erhalten Feedback in unter einer Sekunde, und selbst KI-Agenten können Beweise liefern. So lassen sich auch unsichere Blöcke und nebenläufiger Code mit eigenen Locking-Schemata maschinell absichern, etwa in AWS' Nitro Isolation Engine.