Claude formálisan igazolt 123 nyílt forrású könyvtárat

Mi történt?

Az Anthropic Frontier Red Teamje október 22-én publikálta, hogyan használta a Claude-ot formális szoftververifikációra a Theorem nevű céggel közösen (Anthropic). A kiindulópont: az AI ma már könnyen talál és ki is használ bugokat, ezért a tesztelés mellett bizonyítás is kellene arra, hogy a kód hibamentes egy adott szabály szerint.

A formális verifikáció eddig drága műfaj volt. Az Anthropic példája szerint az seL4 kernel megírása két emberévbe került, a verifikálása ennél jóval többe. Ezért eddig főleg kritikus rendszereknél, például repüléstechnikai kódban használták.

Hogyan csinálták?

A Google OSS-Fuzz projektjeinek meglévő fuzz tesztjeiből indultak ki. A könyvtárat és a fuzz tesztet RISC-V binárisra fordították, ebből a Theorem RISC-V és Linux folyamat szemantikájával automatikusan specifikáció lett: a teszt egyetlen 64 MB alatti inputra sem omlik össze. A bizonyítást a Claude írta Rocq-ban, a Rocq kernel ellenőrizte.

• 239 belépési pont 123 OSS-Fuzz könyvtárban, néhány hét alatt.
• Nagyjából 180 millió sor ellenőrzött Rocq-bizonyítás, egy tipikus bizonyítás kb. 600 ezer sor.
• A binárisok medián hossza 18 ezer RISC-V utasítás.
• Az agentek egymás bizonyításait is újrahasznosíthatták, egy kísérletben így 17 százalékkal kevesebb tokent használtak.

A lényeg, hogy a több millió sor bizonyítást senkinek sem kell kézzel átnéznie. Megbízni csak a RISC-V és Linux modellben, a bizonyított tételben és a Rocq ellenőrzőben kell.

Milyen bugokat talált?

Bizonyítás közben a Claude javította is a talált hibákat. Ezek közül sokat egy fuzzer valószínűleg sosem találna meg: például egy kitömörítőben egy számláló alulcsordulása out-of-bounds írást okozott, de csak egy kb. 20 MB-os, ritka felépítésű inputnál. Előkerült egy out-of-bounds olvasás egy képdekóderben (64 MB input és 2 GB feletti memória kellett hozzá), illetve újra megtalálta a libexpat CVE-2026-56132 hibáját is.

Az Anthropic más kísérleteket is leírt: a Linux kernel zlib implementációjáról x86 binárison igazolta, hogy megfelel az RFC 1950-nek. Egy Rustban írt Python interpreternél pedig 1,7 millió véletlen programon 99,95 százalékos egyezést mértek a CPythonnal.

Mit nem jelent?

Az Anthropic maga hangsúlyozza: a formálisan verifikált nem azonos a hibamentessel. A bizonyítások egyszálú, statikus, musl libc-re linkelt RISC-V binárisokra vonatkoznak, miközben a valóságban ezek a könyvtárak többnyire x86-on vagy ARM-on, dinamikusan linkelve futnak. Nem minden belépési pontot igazoltak. Az ASan sem fog meg minden memóriahibát.

Mit kezdhetsz vele?

A bizonyítások egy része, a RISC-V és OS szemantika nyilvános. A Theorem felajánlotta, hogy más nyílt forrású projekteken is lefuttatja a pipeline-t, illetve Claude skillt is kiadott a saját kód verifikálásához. Ha C vagy C++ könyvtárat tartasz karban OSS-Fuzz tesztekkel, érdemes ránézni, mert a fuzz teszt itt egyből specifikációvá válik.