PDD Kit přesouvá kontrolu agentního kódu od řádků ke specifikaci

Microsoft Research a GitHub Next ukázaly prototyp, který převádí záměr vývojáře do specifikace pro Verus a nad Rust kódem vytváří strojově kontrolovaný důkaz. Silnější záruka však platí jen uvnitř přesně popsané hranice důvěry.

Pět tisíc řádků Rustu posloužilo jako zkušební provoz

PDD Kit běží uvnitř plánovacího prostředí Chopin. Nejdřív klade vývojáři otázky, z odpovědí vytvoří čitelnou mapu záměru a formální specifikaci, pak nechá agenta napsat kód i důkaz. Verus s pomocí solveru Z3 rozhodne deterministicky, zda důkaz platí.

Tým postup předvedl na webové aplikaci Pet Store s přibližně 5 000 řádky Rustu. Formálně ověřil přihlašovací logiku a její vazbu na účet i roli. Z původního zadání o 2 větách vzniklo 8 podmínek pro hlavní login flow. Kontrola malého modulu podle autorů obvykle trvá sekundy, u většího kódu minuty.

Člověk má číst smlouvu, ne každý vygenerovaný řádek

Praktická změna spočívá v místě kontroly. Vývojář schvaluje záměr, sporné interpretace a formální specifikaci. Agent píše implementaci i důkaz, ale o jeho platnosti nerozhoduje další model. Rozhoduje Verus v buildu a později v CI.

To může pomoci tam, kde agent vytvoří tolik kódu, že běžný line by line review přestává být reálný. PDD Kit navíc vkládá pro každou podmínku záměrnou chybu. Pokud ji verifier neodmítne, podmínka je příliš slabá a vrací se k opravě.

Důkaz končí u databáze, kryptografie i hodin

Pojem formálně ověřená aplikace by zde přeháněl. Verus dnes ověřuje jen Rust a v ukázce nevidí dovnitř bcrypt, SQL dotazů, podpisu tokenu ani systémových hodin. Vývojář schválil 6 důvěryhodných částí, které kryjí testy, nikoli důkaz. Celá záruka navíc stojí na správnosti specifikace.

Autoři sami PDD Kit označují za research prototype. Ukázka pokrývá přihlašovací logiku jedné aplikace a neposkytuje měření nákladů na dlouhodobou údržbu důkazů v rozsáhlém produktu.

Nasazení v cizím Rust projektu ukáže cenu záruky

Rozhodující bude, zda jiné týmy udrží specifikace při rychlých změnách a zda se hranice důvěry nebude rozrůstat rychleji než ověřená část. Důležitá bude i dostupnost mimo Chopin a podpora dalších jazyků.

Nejlepší první cíle jsou úzké a drahé chyby, například přihlášení, oprávnění nebo platby. Pokud PDD Kit sníží počet regresí bez toho, aby vývojáři začali většinu času vysvětlovat verifieru vlastní program, má nový model review šanci.

Lilithin verdikt

Agent může vyrobit 100 000 řádků za zavřenými dveřmi. PDD Kit chce, aby člověk předem zkontroloval smlouvu a verifier pak nepustil ven kód, který ji poruší.