En kodefeil som slipper gjennom testingen, kan stanse leveranser eller åpne en vei inn til kundedataene. Anthropic og Theorem rapporterer nå at de har brukt KI til å finne feil, rette koden og bevise matematisk at bestemte feil ikke oppstår i den rettede versjonen, innenfor fastsatte grenser.
For norske bedrifter gir dette en mulighet til å få bedre beskyttelse før programvaren tas i bruk. Leverandøren får sterkere dokumentasjon på at en bestemt retting virker. Men beviset gjelder et avgrenset krav til en bestemt del av koden. Det er ingen garanti for at hele tjenesten er sikker.
Her forklarer jeg hva forskerne har fått til, hvordan et matematisk bevis skiller seg fra en vanlig test, og hva ledelsen bør undersøke før den kjøper programvare med slik dokumentasjon.
Hva har forskerne gjort?
I forskning publisert 22. oktober 2026 beskriver Anthropic hvordan selskapet og Theorem brukte Claude til å bevise at kode oppfylte bestemte sikkerhetskrav. Underveis fant Claude feil, rettet den berørte koden og fortsatte til den kunne lage bevis for kravene som var valgt.
Selskapet rapporterer bevis for 239 testinnganger fordelt på 123 biblioteker med åpen kildekode. Et slikt bibliotek er en samling kode som andre programmer bruker. En testinngang er stedet der et testverktøy sender data inn i koden. Tallene betyr ikke at 123 komplette biblioteker er bevist feilfrie.
Det interessante er sammenhengen mellom å finne feilen, rette den og dokumentere at den rettede koden følger en bestemt regel. Dette er utviklernes egne resultater. Forsøket er ikke en uavhengig måling av gevinster i norske bedrifter.
Hva er forskjellen på en test og et bevis?
En test kjører programmet med utvalgte eksempler. Hvis et program leser disse filene riktig, består det testen. En annen fil kan likevel utløse en feil som testen ikke fanget opp.
Et formelt bevis tar utgangspunkt i en presis regel, for eksempel at bestemte krasj ikke skal oppstå. Beviset viser at regelen holder for alle inndata innenfor de fastsatte grensene. Det forutsetter at den matematiske beskrivelsen av programmet og omgivelsene stemmer. Metoden kalles formell verifikasjon.
KI lager det matematiske argumentet. Et eget kontrollverktøy sjekker om beviset faktisk viser det den valgte regelen krever. Det er noe annet enn å be en språkmodell forsikre om at dens egen kode er trygg. Fagfolk må fortsatt vurdere om regelen og forutsetningene dekker det som er viktig i den faktiske tjenesten.
Et godt bevis besvarer altså ett avgrenset spørsmål grundig. Det besvarer ikke alle spørsmål om programvaren.
Hva er ikke bevist?
Det offentlige arkivet med bevis omfattet 60 testinnganger i 25 biblioteker da det ble kontrollert 26. oktober. Dette er en publisert del av det større forsøket. Bevisene gjelder bestemte kjørbare programfiler og feil som de inkluderte kontrollverktøyene oppdager. De viser ikke at hele biblioteket gir riktige resultater. De utelukker heller ikke at et program fortsetter å kjøre uten å bli ferdig. Bevisene er ikke kontrollert på nytt som del av arbeidet med denne artikkelen.
Det siste har praktisk betydning. En tjeneste som konverterer filer uten å krasje, men aldri blir ferdig, leverer fortsatt ikke det kunden trenger. Å unngå et bestemt krasj, gi riktig resultat og fullføre oppgaven i tide er forskjellige krav.
Forsøket brukte faste programfiler laget for en bestemt prosessortype, RISC-V, og en matematisk modell av Linux. Bevisene bygger på dette oppsettet og på grenser for inndata og minnebruk. En bedrift med andre programfiler eller driftsforhold kan ikke uten videre legge de samme bevisene til grunn.
Slike forutsetninger er en vanlig del av metoden. Det etablerte seL4-prosjektet beskriver sine egne forutsetninger, blant annet om maskinvaren og oppstart av systemet. Dette er et eget arbeid som ikke bekrefter Anthropics resultater. Det viser hvorfor vilkårene må følge med påstanden om hva som er bevist.
Følg én kundefil gjennom tjenesten
Se for deg en hypotetisk norsk produksjonsbedrift som mottar tegningsfiler fra kunder. En leverandør konverterer filene til et format de ansatte bruker når de lager pristilbud. En feil i delen som leser filene, stanser konverteringen og forsinker arbeidet.
Anta at leverandøren tilbyr et bevis for at en bestemt feil ikke kan oppstå i funksjonen som leser filene. Bedriftens tekniske rådgiver må først undersøke om det gjelder filtypene, filstørrelsene, programversjonen og driftsmiljøet som faktisk brukes.
Se deretter på resten av tjenesten. Den skal motta filen, sørge for at bare rett kunde og autoriserte ansatte har tilgang, konvertere den og levere et brukbart resultat. Et bevis for funksjonen som leser filen, dekker ikke automatisk disse andre oppgavene. Det viser heller ikke at tegningen inneholder riktige mål for bestillingen.
Beviset kan likevel fjerne en viktig feilkilde. Ledelsen må forstå forbedringen og sørge for at andre tiltak håndterer risikoen som gjenstår. En avgrenset garanti kan være verdifull uten å bli en garanti for hele virksomheten.
Still leverandøren fem enkle spørsmål
Be om en kort forklaring ved siden av den tekniske dokumentasjonen før dere legger beviset til grunn:
- Hvilken feil er utelukket? Spør hva som fortsatt kan gå galt, også om programmet kan gi feil resultat eller aldri bli ferdig.
- Hvilken versjon gjelder det? Få oppgitt programfilen og dens digitale fingeravtrykk, slik at fagfolkene kan sammenligne den med versjonen som brukes i drift.
- Hvilke forutsetninger gjelder? Kontroller grenser for inndata, avhengigheter og driftsforhold mot bedriftens faktiske oppsett.
- Hvordan er beviset kontrollert? Be om materialet og en praktisk måte å kontrollere det på, eller avtal en uavhengig faglig gjennomgang. Et KI-generert avsnitt som lover god sikkerhet, er ikke nok.
- Hva skjer ved neste oppdatering? Avtal hvem som kontrollerer den nye versjonen og trekker tilbake påstander som ikke lenger er dokumentert.
Spørsmålene er et forslag til hjelp ved innkjøp, ikke en sertifiseringsordning eller et generelt lovkrav. Et lite AS kan bruke en kvalifisert leverandør eller ekstern rådgiver til den tekniske vurderingen. Ledelsen trenger en forståelig forklaring på beskyttelsen den kjøper. Den trenger ikke selv kunne kontrollere de matematiske detaljene.
Undersøk om metoden er verdt å betale for
Begynn med én viktig komponent som behandler filer eller data utenfra, og et krav som lar seg beskrive presist. Bestill en avgrenset vurdering før dere setter i gang et stort prosjekt. Ta med faglig gjennomgang, utviklingsarbeid og vedlikehold av beviset i kostnaden, i tillegg til bruken av KI.
Sammenlign med andre måter å redusere samme risiko på: fjerne en unødvendig filtype, skille filkonverteringen fra viktige systemer, bytte en uegnet komponent eller forbedre dagens tester. Velg ut fra risikoen bedriften er utsatt for, og ressursene den har.
Ikke avvis metoden bare fordi den tidligere krevde for mye spesialistarbeid. En liten undersøkelse kan avklare om bedre dokumentasjon nå er praktisk mulig, mens dagens beskyttelse beholdes. Den kan også vise at et annet tiltak gir mer igjen for pengene.
Ledelsen har ansvar for vurderingen, oppfølgingen av leverandøren og beslutningen om å ta programvaren i bruk. Ved vesentlig risiko eller større investeringer bør styret spørre hvilket problem arbeidet forebygger, hva som fortsatt er uløst, og hvordan dokumentasjonen holdes oppdatert. Styret skal ikke velge bevisverktøy eller godkjenne hver kodeendring.
Bruk artikkelen om dokumentasjon til kundenes sikkerhetskontroll når dere vurderer leverandørens sikkerhetsløfter. Artikkelen om respons før en sikkerhetsoppdatering finnes tar opp feilene som fortsatt krever rask handling. Både bedre forebygging og raskere respons er nødvendig.
Det praktiske spørsmålet er: Hvilken viktig feil har leverandøren bevist at ikke kan oppstå i versjonen vi faktisk skal bruke? Svaret avgjør hvor stor vekt bedriften bør legge på beviset.
Kildene er kontrollert 26. oktober 2026. Produksjonsbedriften og innkjøpsspørsmålene er hypotetiske. Rådene er forfatterens vurderinger. Forskningen beviser ikke at all programvare er sikker. Den KI-genererte illustrasjonen viser grensen for en matematisk påstand, ikke et faktisk bevis fra forskningen.