PDD Kit soll AI-generierten Full-Stack-Code formal verifizieren
TL;DR
AI-Agenten erzeugen inzwischen mehr Code, als Menschen realistisch Zeile für Zeile prüfen können. Microsoft Research stellt deshalb PDD Kit vor: Das System übersetzt die Absicht eines Entwicklers in eine formale Verus-Spezifikation und prüft, ob der erzeugte Code diese für alle Eingaben erfüllt. Wo formale Beweise unpraktisch sind, kommen Tests zum Einsatz. Entwickler prüfen damit stärker die gewünschte Funktion und weniger jede einzelne Codezeile.
Nauti's Take
Für kleine Teams ist der erste Test eine kleine, kritische Funktion mit präziser Spezifikation. Prüft, welche Eigenschaften PDD Kit tatsächlich beweist, wo Tests einspringen und ob der zusätzliche Aufwand für Verus und Spezifikationen den manuellen Review messbar reduziert.
Quellen