Anthropicin mukaan Claude todisti 123 kirjaston turvallisuusominaisuuksia

Anthropic julkaisi tutkimuksen 22. lokakuuta 2026 ja kertoi, että Claude tuotti koneellisesti tarkistetut muodolliset todistukset 239 fuzz-testien aloituspisteen turvallisuusominaisuuksista RISC-V-assemblykoodin tasolla 123 avoimen lähdekoodin kirjastossa yhteistyössä Theoremin kanssa.

Anthropicin mukaan Claude korjasi löytämänsä virheet ja todisti sen jälkeen, että ohjelmat päättyvät aina normaalisti aiheuttamatta muistiturvallisuusvirheitä tai epäonnistuneita assertioita kaikilla alle 64 MB:n syötteillä sekä kaikilla mallinnetuilla Linux-käyttöjärjestelmän vastauksilla ja muistiasetteluilla. Todistuksissa oletetaan, että ohjelma suoritetaan yksisäikeisenä staattisena binäärinä, jolla on kiinteä muistibudjetti, RISC-V-suorittimella Linuxia käyttäen. Anthropicin mukaan todistukset sisältävät noin 180 miljoonaa Rocq-riviä, ja tyypillinen todistus on noin 600 000 riviä, joilla katetaan binäärit, joiden pituuden mediaani on 18 000 RISC-V-käskyä. Yhtiö kertoi, että tiettävästi kyseessä on ensimmäinen laajamittainen hanke, jossa tekoälyä käytetään muodolliseen verifiointiin tuotanto-ohjelmiston assemblykooditasolla.

Osa todistuksista sekä niiden taustalla olevat RISC-V:n ja käyttöjärjestelmän semantiikat julkaistaan GitHubissa. Anthropicin mukaan se julkaisee myös hanketta varten rakennetut luotetut komponentit, jotka eivät vielä ole julkisia, täydelliset todistukset fuzz-testeistä, jotka eivät vaatineet korjauksia, sekä sellaisten fuzz-testien määrittelyt, joita se ei pystynyt todistamaan. Todistukset, jotka voisivat paljastaa korjaamattoman virheen, jätetään julkaisematta.

Fuzz-testeistä muodollisiksi todistuksiksi

Menetelmä muuntaa kunkin kirjaston olemassa olevan, käännettävän fuzz-testin muodolliseksi määrittelyksi, joka ilmaisee yhden säännön: testi ei kaadu millään alle 64 MB:n syötteellä. Määrittely perustuu käännettyihin RISC-V-käskyihin ja Theoremin RISC-V-käskyjoukon sekä Linux-prosessien muodolliseen semantiikkaan, ja Rocq-todistin tarkistaa jokaisen valmiin todistuksen määrittelyä vasten. Anthropicin mukaan tämä jättää kehittäjien luotettavaksi vain kolme osaa: RISC-V:n ja Linux-prosessien muodolliset mallit, täsmälliset teoreemalauseet ja itse Rocq-todistimen.

Anthropic kertoi soveltaneensa tätä prosessia satoihin projekteihin Googlen OSS-Fuzz-aloitteessa, joka tarjoaa jatkuvaa fuzz-testausta siihen soveltuville avoimen lähdekoodin projekteille ja instrumentoi C- ja C++-ohjelmat automaattisesti AddressSanitizer-työkalulla. Työkalu kaataa ohjelman aina, kun muistia käytetään virheellisesti. Päiväyksellä 22. lokakuuta 2026 varustetussa liitteessä esitetään todistettu teoreema kokonaisuudessaan: kaikilla alle 64 MiB:n syötteillä ja kaikilla muistiasetteluilla sen paremmin ASan-instrumentoitu binääri kuin tavallinen binäärikään ei aiheuta muistivirhettä, keskeydy tai käyttäydy mallintamattomalla tavalla, ja molemmat tuottavat identtiset luku- ja kirjoitusjäljet, päättymiskäyttäytymisen ja tiedostojärjestelmän lopputilan.

Liitteen mukaan Claude kirjoitti hankkeen aikana noin miljardi Rocq-riviä, joista noin 180 miljoonaa läpäisi todistimen tarkistuksen. cJSON:n 391-rivinen jäsentimen aloituspiste sai 630 000 rivin todistuksen, kun taas fftw3, johon oli linkitetty 51 000 riviä, sai 480 000 rivin todistuksen. Koska Claude sai korjata koodia ennen todistuksen valmistumista, Anthropicin mukaan korjauksista vähennettiin pisteitä, lisäpisteitä sai sen todistamisesta, mihin syötteisiin korjaus vaikutti, ja korjaukset kirjattiin ja auditoitiin palkkion manipuloinnin ehkäisemiseksi.

Todistusyrityksissä löytyneet virheet

Anthropic kertoo, että todistusyritykset paljastivat satoja virheitä, joista monet olisivat todennäköisesti jääneet fuzz-testaajalta löytämättä. Todistaessaan erään kirjaston aloituspistettä Claude löysi purkuohjelmasta laskurin alivuodon, joka aiheutti rajojen ulkopuolelle kirjoittamisen, mutta vain noin 20 MB:n syötteillä ja yhden harvinaisen, tietynlaisen asettelun yhteydessä. Muita löytöjä olivat kuvanpurkajasta löytynyt rajojen ulkopuolinen luku, joka edellytti 64 MB:n syötettä ja yli 2 GB muistia; rajojen ulkopuolinen luku, joka edellytti tiettyä puhelujonoa kahden saman tiedoston käsittelijän kautta; sekä libexpatista uudelleen löydetty CVE-2026-56132, joka edellytti syvästi sisäkkäistä syötettä.

Claude löysi myös loogisia virheitä, jotka eivät koskaan aiheuta kaatumista. Yksi niistä oli rajoitus siihen, mitä tiedostoja sovellus voi ladata, mutta rajoitusta ei aina valvota. Anthropicin mukaan useisiin laajalti käytettyihin kriittisiin sovelluksiin kohdistuneet verifiointiyritykset paljastivat aiemmin tuntemattoman loogisen virheen, joka oli piilevänä yli vuosikymmenen ajan. Yhtiö kertoi myös löytäneensä laajalti käytetyn PDF-lukijan verifiointiyrityksen aikana yhden viikon aikana yhtä monta tietoturvavirhettä kuin siitä tavallisesti ilmoitetaan vuoden aikana.

Lisäkokeet ja tehokkuutta koskevat havainnot

OSS-Fuzzin lisäksi Anthropic pyysi Claudea laatimaan RFC 1950:stä muodollisen määrittelyn ja todistamaan sen jälkeen, että Linux-ytimen zlib-toteutus vastaa määrittelyä oikein. RFC 1950 on zlib-pakkausmuodon määrittelevä tekninen asiakirja. Claude todisti suoraan x86:lle käännetyn binäärin käyttäen Clauden tuottamaa x86-käskyjoukon muodollista semantiikkaa. Anthropicin mukaan se toisti prosessin puolelle tusinalle muulle laajalti käytetylle kirjastolle ja löysi pieniä, hyödyntämättömiä reunatapauksia koskevia virheitä, joista ilmoitetaan ylläpitäjille. Yhtiö kertoi myös, että x86-semanttiikan tuottaminen paljasti satoja virheitä virallisessa viitedokumentaatiossa ja pienemmän määrän virheitä itse laitteistossa. Semantiikan suorittaminen askel askeleelta voi käynnistää Ubuntu-käyttäjätilan Linux-ytimessä.

Toisessa kokeessa Claude rakensi Rustilla tulkin suurelle Pythonin osajoukolle ja osoitti Verus-verifiointityökalulla, että se noudattaa akateemisessa artikkelissa määriteltyä CPythonin semantiikkaa. Teknisessä liitteessä todetaan, että tulkin kaikki 17 tasoa verifioitiin. Todistettu teoreema kuuluu: ”Aina kun tulkki palauttaa tuloksen, se on sama kuin formaalisen semantiikan määräämä tulos.” Anthropic kertoi empiirisestä testauksesta, jossa testattiin 1,7 miljoonaa satunnaisesti luotua Python-ohjelmaa ja havaittiin, että toiminta vastasi CPythonin toimintaa 99,95 prosentissa testeistä. Seitsemästä tarkoituksella lisätystä virheestä viisi jäi satunnaistestauksessa havaitsematta, mutta kaikki seitsemän rikkoivat todistuksen.

Tehokkuuden mittaamiseksi Anthropic rakensi 36 pientä verifiointitehtävää pienentämällä todellisia OSS-Fuzzin sisääntulopisteitä. Näin syntyi ohjelmia, joissa oli 283–2 491 käskyä ja joiden syötteet oli rajattu 64 tavuun; AddressSanitizer korvattiin noin 100 käskyn ”mini-ASan”-suoritusympäristöllä. Anthropic kertoo, että Opus 5.5 todistaa puolet tehtävistä noin 40 prosenttia vähemmillä tokeneilla kuin Opus 5. Anthropic kertoo myös, että agentit, jotka saivat kopioida toistensa todistuksia jaettuun työtilaan, tarvitsivat 17 prosenttia vähemmän tokeneita kuin yksin työskennelleet agentit. Osa agenteista onnistui tehtävissä, joissa ne olivat aiemmin epäonnistuneet yksin, ja yksin työskennelleet agentit eivät saaneet kahta todistusta valmiiksi. Yhtiön mukaan sama todistusten uudelleenkäytön vaikutus näkyi laajassa mittakaavassa OSS-Fuzz-työssä: agenttiryhmät kopioivat valmiita todistuksia ja muokkasivat niitä, koska kunkin todistuksen sisällöstä suuri osa käsittelee yhteistä C-suoritusympäristöä ja AddressSanitizerin alustuskoodia.

Ilmoitetut rajoitukset ja OSS Verify -ohjelma

Anthropicin mukaan todistukset eivät tarkoita, että kirjastoissa ei olisi virheitä: jäljellä olevat virheet voivat sijaita luotetuissa komponenteissa tai jäädä todistusten soveltamisalan ulkopuolelle. Todistukset kattavat yksisäikeiset, staattisesti linkitetyt RISC-V-binäärit, jotka on linkitetty musl libc -kirjastoon, kun taas useimmat käyttäjät käyttävät näitä kirjastoja x86- tai ARM-arkkitehtuurilla ja linkittävät ne dynaamisesti glibc-kirjastoon. Lisäksi AddressSanitizer ei havaitse kaikkia muistiturvallisuuteen liittyviä virheitä. Yhtiö kertoi odottavansa näiden rajoitusten muuttuvan hallittaviksi mallien kehittyessä.

Theorem tarjoaa saman prosessiketjun maksutta ehdot täyttäville avoimen lähdekoodin projekteille OSS Verify -ohjelmansa kautta. Ohjelmaan liitytään tekemällä vetopyyntö, joka lisää ohjelman repositorioon tiedostot project.yaml, Dockerfile ja build.sh. Theoremin mukaan se arvioi projekteja OSS-Fuzzin kaltaisin perustein ja asettaa etusijalle laajalti käytetyn kriittisen infrastruktuurin. Theoremin mukaan ylläpitäjät saavat Rocq-todistuksen, jonka Rocq-ydin tarkistaa ja joka osoittaa, ettei mikään fuzz-kohde kaadu millään enintään 64 MiB:n kokoisella syötteellä. Todistustyön aikana löydetyistä virheistä ilmoitetaan ylläpitäjille yksityisesti sähköpostitse, eikä ilmoittamiselle ole määräaikaa. Todistusten tuottaminen voi kestää useita päiviä. Theoremin etenemissuunnitelman tavoitteena on verifioida koko Nix-ekosysteemi, mukaan lukien kriittinen infrastruktuuri, kuten glibc, OpenSSL ja cURL.