Anthropic ve spolupráci s Theorem využil Clauda k opravám chyb a vytváření formálních důkazů pro 239 testovacích vstupních bodů ve 123 open-source knihovnách projektu OSS-Fuzz. Podle firmy práce zabrala několik týdnů. Výsledkem jsou důkazy, že vybrané testy za stanovených podmínek nespadnou pro žádný vstup menší než 64 MB, nikoli pouze úspěšné prověření mnoha vzorků.
Z fuzzovacích testů vznikly matematické specifikace
Základem postupu byly existující fuzzovací testy. Anthropic je převedl na matematické specifikace popisující chování zkompilovaných instrukcí RISC-V. Dokazované tvrzení se vztahovalo na všechny vstupy pod stanovenou velikostní hranicí: test při jejich zpracování nesmí spadnout. Namísto zkoušení dalších konkrétních vzorků tak Claude dostal za úkol vytvořit důkaz pro celý vymezený prostor vstupů.
Podle Anthropicu vzniklo přibližně 180 milionů řádků důkazů v systému Rocq. Typický důkaz měl kolem 600 000 řádků, zatímco medián délky ověřovaných binárních programů dosahoval 18 000 instrukcí RISC-V. Při převodu strojového kódu do matematického modelu projekt využíval formální popis instrukcí RISC-V a linuxových procesů od Theorem.
Claude nalezené chyby opravoval a pokračoval v dokazování
Pokusy o důkaz podle Anthropicu odhalily stovky chyb. Výzkumníci nastavili postup tak, aby Claude nemusel při každém nálezu čekat na člověka: mohl upravit kód, nechat z opravené verze znovu vytvořit specifikaci a pokračovat v dokazování jejího splnění.
Jako konkrétní příklad firma popisuje podtečení čítače v kopii dekompresoru. Chyba vedla k zápisu mimo vyhrazenou paměť, ale projevila se jen u vstupů kolem 20 MB s určitým vzácným uspořádáním. Podle autorů by ji běžné fuzzování obtížně zachytilo, protože zpravidla mění malé vstupy, obvykle omezené na 1 MB.
Důkazy mohou zachytit i funkční vlastnosti
Nepřítomnost pádu může podle Anthropicu dokazovat také správnost určité funkce, pokud ji test kontroluje asercí. U komprese LZO například test požaduje, aby po kompresi a následné dekompresi vznikl původní vstup. Porušení této podmínky vyvolá pád, takže důkaz nepřítomnosti pádu zahrnuje i tuto vlastnost.
Při ověřování cpp-httplib musel Claude podle firmy vyřešit také riziko přetečení zásobníku při rekurzi v destruktoru std::set. Hloubka této rekurze závisí na maximální hloubce stromu. Součástí práce proto byl důkaz přímo nad strojovým kódem, že algoritmus vyvažování červeno-černého stromu v libc++ udržuje jeho hloubku logaritmicky omezenou.
Platnost vymezuje prostředí i rozsah testů
Anthropic vztahuje důkazy na všechny modelované odpovědi Linuxu a všechna modelovaná rozložení paměti. Předpokladem je však jednovláknový, staticky linkovaný program s pevným paměťovým rozpočtem na procesoru RISC-V. Ověřované binární soubory používají musl libc, zatímco běžné nasazení těchto knihoven využívá také procesory x86 či ARM a dynamické linkování s glibc.
Firma zároveň vymezuje rozsah uvnitř samotných knihoven: neověřovala všechny jejich vstupní body a AddressSanitizer nezachytí všechny chyby paměťové bezpečnosti. Ani prověření všech vstupních bodů by nemuselo zahrnout například mrtvý kód. Další chyby mohou vzniknout v programu, který knihovnu nesprávně používá.
Samotné důkazy podle Anthropicu kontroluje Rocq, takže prakticky nevyžadují ruční revizi. Vývojář ale stále musí důvěřovat formálním modelům procesoru a linuxových procesů. Stejně podstatné je přesné znění dokazovaných vět a správnost kontroloru důkazů Rocq.
Opus 5.5 a sdílení důkazů snížily spotřebu tokenů
Anthropic z kódu OSS-Fuzz sestavil také 36 malých ověřovacích úloh pro porovnání modelů. V tomto testu podle firmy Opus 5.5 dokončil důkazy u poloviny úloh s přibližně o 40 % menším počtem tokenů než Opus 5.
V dalším experimentu firma umožnila agentům přebírat důkazy ostatních prostřednictvím sdíleného pracovního prostoru. Oproti samostatné práci pak podle Anthropicu spotřebovali o 17 % méně tokenů. Někteří agenti navíc dokončili úlohy, u nichž při předchozím samostatném pokusu neuspěli.
Zveřejněné důkazy a přístup pro další projekty
Anthropic zveřejňuje dosud neveřejné důvěryhodné komponenty vytvořené pro projekt a úplné důkazy Rocq pro testy, které nevyžadovaly opravy. Součástí zveřejněných materiálů jsou také specifikace některých testů, které se prokázat nepodařilo. Důkazy schopné odhalit dosud neopravenou chybu v open-source softwaru firma nezveřejňuje.
Theorem nabízí spuštění stejného ověřovacího postupu i dalším open-source projektům. Zároveň zveřejňuje Claude skill, který má vývojářům pomoci začít s ověřováním vlastního kódu.
