{"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\/cs\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","title":{"rendered":"A nthropic vyv\u00edj\u00ed techniky pro form\u00e1ln\u00ed ov\u011b\u0159ov\u00e1n\u00ed st\u00e1vaj\u00edc\u00edho softwaru pomoc\u00ed AI","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"

Spole\u010dnost Anthropic p\u0159edstavila v\u00fdsledky experiment\u016f vyu\u017e\u00edvaj\u00edc\u00ed AI modely pro form\u00e1ln\u00ed verifikaci spolehlivosti a bezpe\u010dnosti ji\u017e existuj\u00edc\u00edch projekt\u016f. B\u011bhem experimentu byly pomoc\u00ed AI model\u016f generov\u00e1ny matematick\u00e9 d\u016fkazy absence chyb p\u0159i pr\u00e1ci s pam\u011b\u0165ov\u00fdmi prostory pro 123 otev\u0159en\u00fdch knihoven, testovan\u00fdch v infrastruktu\u0159e OSS Fuzz. <\/p>\n

Ov\u011b\u0159en\u00ed prob\u00edhalo na \u00farovni zkompilovan\u00e9ho assemblerov\u00e9ho k\u00f3du pro architekturu RISC-V. Celkov\u00fd objem vygenerovan\u00fdch d\u016fkaz\u016f \u010dinil p\u0159ibli\u017en\u011b 180 milion\u016f \u0159\u00e1dk\u016f k\u00f3du pro syst\u00e9m verifikace Rocq Prover (asi 600 tis\u00edc \u0159\u00e1dk\u016f na bin\u00e1rn\u00ed soubor s 18 tis\u00edci instrukcemi RISC-V). D\u016fkazy byly vytv\u00e1\u0159eny automatick\u00fdm p\u0159evodem existuj\u00edc\u00edch fuzzingov\u00fdch test\u016f na form\u00e1ln\u00ed specifikace, po kter\u00fdch AI model Claude dok\u00e1zal, \u017ee p\u0159i jak\u00fdchkoli vstupn\u00edch datech o velikosti a\u017e 64 MB v programu nedoch\u00e1z\u00ed k hav\u00e1ri\u00edm. <\/p>\n

B\u011bhem vytv\u00e1\u0159en\u00ed d\u016fkaz\u016f dok\u00e1zal AI model odhalit a p\u0159ipravit opravy pro stovky chyb, kter\u00e9 nebyly d\u0159\u00edve zaznamen\u00e1ny p\u0159i fuzzingov\u00e9m testov\u00e1n\u00ed. Mezi jin\u00fdmi byly odhaleny zranitelnosti vedouc\u00ed k p\u0159ete\u010den\u00ed vyrovn\u00e1vac\u00ed pam\u011bti p\u0159i zpracov\u00e1n\u00ed ur\u010dit\u00fdch vstupn\u00edch dat (nap\u0159\u00edklad CVE-2026-56132 v libexpat), stejn\u011b jako logick\u00e9 chyby. Krom\u011b toho byl AI model pou\u017eit k prok\u00e1z\u00e1n\u00ed shody implementace algoritmu zlib v j\u00e1dru Linux se specifikac\u00ed RFC 1950.<\/p>\n

Tak\u00e9 byl v jazyce Rust vygenerov\u00e1n interpreter pro podmno\u017einu jazyka Python, pro kterou bylo pomoc\u00ed n\u00e1stroj\u016f Verus p\u0159ipraveno form\u00e1ln\u00ed d\u016fkazn\u00ed osv\u011bd\u010den\u00ed odpov\u00eddaj\u00edc\u00ed semantice CPython. Pro porovn\u00e1n\u00ed chov\u00e1n\u00ed s CPython bylo vykon\u00e1no v\u00edce ne\u017e 1,7 milionu n\u00e1hodn\u011b generovan\u00fdch Python program\u016f. Ve 99,95 % p\u0159\u00edpad\u016f se v\u00fdsledky prov\u00e1d\u011bn\u00ed t\u011bchto program\u016f v nov\u00e9 implementaci a v CPython shodovaly, p\u0159i\u010dem\u017e zji\u0161t\u011bn\u00e9 rozd\u00edly se uk\u00e1zaly jako zn\u00e1m\u00e9 hrani\u010dn\u00ed p\u0159\u00edpady.<\/p>\n

Prov\u00e1d\u011bn\u00e1 form\u00e1ln\u00ed verifikace zaru\u010duje shodu se specifikac\u00ed, ale zcela nevylu\u010duje vznik probl\u00e9m\u016f s bezpe\u010dnost\u00ed, jeliko\u017e z\u016fst\u00e1vaj\u00ed neform\u00e1ln\u011b zmapov\u00e1na rizika vypl\u00fdvaj\u00edc\u00ed z probl\u00e9m\u016f s v\u00edcevl\u00e1knovost\u00ed, dynamick\u00fdm spojov\u00e1n\u00edm a anom\u00e1ln\u00edm chov\u00e1n\u00edm skute\u010dn\u00e9ho hardwaru. Kl\u00ed\u010dovou v\u00fdhodou navrhovan\u00e9ho p\u0159\u00edstupu je pr\u00e1ce p\u0159\u00edmo s bin\u00e1rn\u00edmi soubory, co\u017e eliminuje pot\u0159ebu p\u0159episov\u00e1n\u00ed st\u00e1vaj\u00edc\u00edho k\u00f3du do form\u00e1ln\u011b verifikovateln\u00fdch jazyk\u016f.
\n
Zdroj: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"

\u041a\u043e\u043c\u043f\u0430\u043d\u0438\u044f \u0410nthropic \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u0438\u043b\u0430 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u044b \u044d\u043a\u0441\u043f\u0435\u0440\u0438\u043c\u0435\u043d\u0442\u043e\u0432 \u043f\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u044e AI-\u043c\u043e\u0434\u0435\u043b\u0435\u0439 \u0434\u043b\u044f \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043d\u0430\u0434\u0451\u0436\u043d\u043e\u0441\u0442\u0438 \u0438 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438 \u0443\u0436\u0435 \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u044e\u0449\u0438\u0445 \u043f\u0440\u043e\u0435\u043a\u0442\u043e\u0432. \u0412 \u0445\u043e\u0434\u0435 \u044d\u043a\u0441\u043f\u0435\u0440\u0438\u043c\u0435\u043d\u0442\u0430 \u043f\u0440\u0438 \u043f\u043e\u043c\u043e\u0449\u0438 AI-\u043c\u043e\u0434\u0435\u043b\u0435\u0439 \u0434\u043b\u044f 123 \u043e\u0442\u043a\u0440\u044b\u0442\u044b\u0445 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a, \u043f\u0440\u043e\u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0445 \u0432 \u0438\u043d\u0444\u0440\u0430\u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u0435 OSS Fuzz, \u0431\u044b\u043b\u0438 \u0441\u0433\u0435\u043d\u0435\u0440\u0438\u0440\u043e\u0432\u0430\u043d\u044b \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u043e\u0442\u0441\u0443\u0442\u0441\u0442\u0432\u0438\u044f \u043e\u0448\u0438\u0431\u043e\u043a \u043f\u0440\u0438 \u0440\u0430\u0431\u043e\u0442\u0435 \u0441 \u043f\u0430\u043c\u044f\u0442\u044c\u044e. \u041f\u0440\u043e\u0432\u0435\u0440\u043a\u0430 \u043f\u0440\u043e\u0432\u043e\u0434\u0438\u043b\u0430\u0441\u044c \u043d\u0430 \u0443\u0440\u043e\u0432\u043d\u0435 \u0441\u043a\u043e\u043c\u043f\u0438\u043b\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u0433\u043e \u0430\u0441\u0441\u0435\u043c\u0431\u043b\u0435\u0440\u043d\u043e\u0433\u043e \u043a\u043e\u0434\u0430 \u0434\u043b\u044f \u0430\u0440\u0445\u0438\u0442\u0435\u043a\u0442\u0443\u0440\u044b RISC-V. \u041e\u0431\u0449\u0438\u0439 \u043e\u0431\u044a\u0451\u043c \u0441\u0433\u0435\u043d\u0435\u0440\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0445 […]<\/p>\n","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"author":10,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[702],"tags":[],"class_list":["post-183972","post","type-post","status-publish","format-standard","hentry","category-news"],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"\ud83e\udd47Anthropic rozv\u00edj\u00ed techniku pro form\u00e1ln\u00ed verifikaci st\u00e1vaj\u00edc\u00edho SW pomoc\u00ed AI | ProHoster","description":"Spole\u010dnost Anthropic p\u0159edstavila v\u00fdsledky experiment\u016f s vyu\u017eit\u00edm AI model\u016f pro form\u00e1ln\u00ed verifikaci spolehlivosti a bezpe\u010dnosti ji\u017e existuj\u00edc\u00edch projekt\u016f.","canonical_url":"https:\/\/prohoster.info\/cs\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"cs_CZ","og:site_name":"ProHoster | \u041a\u0443\u043f\u0438\u0442\u044c \u043d\u0430\u0434\u0435\u0436\u043d\u044b\u0439 \u0445\u043e\u0441\u0442\u0438\u043d\u0433 \u0434\u043b\u044f \u0441\u0430\u0439\u0442\u043e\u0432 \u0441 \u0437\u0430\u0449\u0438\u0442\u043e\u0439 \u043e\u0442 DDoS, VPS VDS \u0441\u0435\u0440\u0432\u0435\u0440\u044b","og:type":"article","og:title":"\ud83e\udd47\u0410nthropic \u0440\u0430\u0437\u0432\u0438\u0432\u0430\u0435\u0442 \u0442\u0435\u0445\u043d\u0438\u043a\u0443 \u0434\u043b\u044f \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u044e\u0449\u0435\u0433\u043e \u041f\u041e \u043f\u0440\u0438 \u043f\u043e\u043c\u043e\u0449\u0438 AI | ProHoster","og:description":"\u041a\u043e\u043c\u043f\u0430\u043d\u0438\u044f \u0410nthropic \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u0438\u043b\u0430 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u044b \u044d\u043a\u0441\u043f\u0435\u0440\u0438\u043c\u0435\u043d\u0442\u043e\u0432 \u043f\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u044e AI-\u043c\u043e\u0434\u0435\u043b\u0435\u0439 \u0434\u043b\u044f \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043d\u0430\u0434\u0451\u0436\u043d\u043e\u0441\u0442\u0438 \u0438 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438 \u0443\u0436\u0435 \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u044e\u0449\u0438\u0445 \u043f\u0440\u043e\u0435\u043a\u0442\u043e\u0432.","og:url":"https:\/\/prohoster.info\/cs\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","og:image":"https:\/\/prohoster.info\/wp-content\/uploads\/2021\/11\/logo-350.jpg","og:image:secure_url":"https:\/\/prohoster.info\/wp-content\/uploads\/2021\/11\/logo-350.jpg","og:image:width":350,"og:image:height":350,"article:published_time":"2026-10-23T09:41:12+00:00","article:modified_time":"2026-10-23T09:41:16+00:00","article:publisher":"https:\/\/www.facebook.com\/prohoster"},"aioseo_meta_data":[],"gt_translate_keys":[{"key":"link","format":"url"}],"_links":{"self":[{"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/posts\/183972","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/users\/10"}],"replies":[{"embeddable":true,"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/comments?post=183972"}],"version-history":[{"count":1,"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/posts\/183972\/revisions"}],"predecessor-version":[{"id":183973,"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/posts\/183972\/revisions\/183973"}],"wp:attachment":[{"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/media?parent=183972"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/categories?post=183972"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/tags?post=183972"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}