Një projekt kërkimor në bashkëpunim me Theorem ka përdorur Claude për të provuar formalisht veti sigurie në 123 biblioteka softuerike me kod të hapur, në nivelin e kodit assembly RISC-V. Sipas autorëve, kjo është përpjekja e parë në shkallë të gjerë për përdorimin e AI në verifikimin formal të softuerit në përdorim në këtë nivel.
Verifikimi formal përdor modele matematikore për të provuar se kodi respekton rregulla të përcaktuara. Historikisht, ai ka kërkuar shumë punë të specializuar: implementimi i kernelit seL4 mori dy vite-person, ndërsa verifikimi i tij formal 20 vite-person. LLM-të po mundësojnë automatizimin e hartimit të këtyre provave.
Claude provoi se programe të caktuara përfundojnë normalisht, pa gabime të sigurisë së memories apo dështime të kontrolleve assertion, për çdo hyrje më të vogël se 64 MB. Garancitë vlejnë brenda kushteve të modeluara: ekzekutim me një thread, binar statik, buxhet fiks memorieje dhe Linux në RISC-V. Ato nuk nënkuptojnë eliminimin e çdo gabimi të mundshëm.
Gjatë hartimit të provave, Claude zbuloi edhe gabime që kishin mbetur të padiktuara për vite, pavarësisht triliona ekzekutimeve testuese. Autorët po publikojnë një pjesë të provave për verifikim dhe ripërdorim, bashkë me semantikën e RISC-V dhe sistemit operativ. Theorem po ofron të njëjtin proces për projekte të tjera me kod të hapur.
Burimi: Hacker News — lexoni artikullin e plotë në anglisht.
