{"id":183972,"date":"2026-10-23T11:41:12","date_gmt":"2026-10-23T09:41:12","guid":{"rendered":"https:\/\/prohoster.info\/blog\/news\/anthropic-razvivaet-tehniku-dlya-formalnoj-verifikaczii-sushhestvuyushhego-po-pri-pomoshhi-ai"},"modified":"2026-10-23T11:41:16","modified_gmt":"2026-10-23T09:41:16","slug":"anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","status":"publish","type":"post","link":"https:\/\/prohoster.info\/sk\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","title":{"rendered":"Anthropic vyv\u00edja technol\u00f3gie na form\u00e1lnu verifik\u00e1ciu existuj\u00faceho softv\u00e9ru pomocou AI","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Spolo\u010dnos\u0165 Anthropic predstavila v\u00fdsledky experimentov s vyu\u017eit\u00edm AI modelov na form\u00e1lnu verifik\u00e1ciu spo\u013eahlivosti a bezpe\u010dnosti existuj\u00facich projektov. Po\u010das experimentu boli pomocou AI modelov generovan\u00e9 matematick\u00e9 d\u00f4kazy o absencii ch\u00fdb pri pr\u00e1ci s pam\u00e4\u0165ou pre 123 otvoren\u00fdch kni\u017en\u00edc, testovan\u00fdch v prostred\u00ed OSS Fuzz. <\/p>\n
Kontrola sa vykon\u00e1vala na \u00farovni skompilovan\u00e9ho assemblerov\u00e9ho k\u00f3du pre architekt\u00faru RISC-V. Celkov\u00fd objem generovan\u00fdch d\u00f4kazov dosiahol pribli\u017ene 180 mili\u00f3nov riadkov k\u00f3du pre syst\u00e9m verifik\u00e1cie Rocq Prover (pribli\u017ene 600 tis\u00edc riadkov na bin\u00e1rny s\u00fabor s 18 tis\u00edcami RISC-V in\u0161trukci\u00ed). D\u00f4kazy sa vytv\u00e1rali automatick\u00fdm prevodom existuj\u00facich fuzzing testov na form\u00e1lne \u0161pecifik\u00e1cie, po \u010dom AI model Claude dokazoval, \u017ee pri ak\u00fdchko\u013evek vstupn\u00fdch \u00fadajoch do 64 MB v programe nevznikaj\u00fa v\u00fdpadky. <\/p>\n
Po\u010das tvorby d\u00f4kazov AI model dok\u00e1zal odhali\u0165 a pripravi\u0165 opravy pre stovky ch\u00fdb, ktor\u00e9 neboli predt\u00fdm zaznamenan\u00e9 pri fuzzing testovan\u00ed. Medzi nimi boli zisten\u00e9 zranite\u013enosti ved\u00face k prete\u010deniu z\u00e1sobn\u00edka pri spracovan\u00ed ur\u010dit\u00fdch vstupn\u00fdch \u00fadajov (napr\u00edklad CVE-2026-56132 v libexpat), ako aj logick\u00e9 chyby. Okrem toho bol AI model pou\u017eit\u00fd na d\u00f4kaz s\u00faladu implement\u00e1cie algoritmu zlib v jadre Linuxu so \u0161pecifik\u00e1ciou RFC 1950.<\/p>\n
Taktie\u017e bol v jazyku Rust generovan\u00fd interpret\u00e1tor pre podmno\u017einu jazyka Python, pre ktor\u00fa bolo pomocou n\u00e1strojov Verus pripraven\u00e9 form\u00e1lne d\u00f4kazov\u00e9 s\u00falad s semantikou CPython. Na porovnanie spr\u00e1vania s CPython bolo vykonan\u00fdch viac ako 1,7 mili\u00f3na n\u00e1hodne generovan\u00fdch Python programov. V 99,95 % pr\u00edpadov sa v\u00fdsledky vykonania t\u00fdchto programov v novej implement\u00e1cii a v CPython zhodovali, pri\u010dom zisten\u00e9 rozdiely sa uk\u00e1zali ako zn\u00e1me hrani\u010dn\u00e9 pr\u00edpady.<\/p>\n
Proveden\u00e1 form\u00e1lna verifik\u00e1cia zabezpe\u010duje s\u00falad so \u0161pecifik\u00e1ciou, ale \u00faplne nevylu\u010duje vznik bezpe\u010dnostn\u00fdch probl\u00e9mov, preto\u017ee form\u00e1lne nie s\u00fa zoh\u013eadnen\u00e9 rizik\u00e1 sp\u00f4soben\u00e9 probl\u00e9mami s viacer\u00fdmi vl\u00e1knami, dynamick\u00fdm prepojen\u00edm a anom\u00e1lnym spr\u00e1van\u00edm skuto\u010dn\u00e9ho hardv\u00e9ru. K\u013e\u00fa\u010dovou v\u00fdhodou navrhnut\u00e9ho pr\u00edstupu je pr\u00e1ca priamo s bin\u00e1rnymi s\u00fabormi, \u010do umo\u017e\u0148uje ob\u00eds\u0165 potrebu prepisovania existuj\u00faceho k\u00f3du na form\u00e1lne overite\u013en\u00fdch jazykoch. \n Zdroj: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"