# Az AI-val a formális szoftververifikáció is elérhetőbbé válhat

*Wired · 2026-10-29 · Kutatás*

**Egy Stanford-kutató AI-eszközzel fél napnál rövidebb idő és 500 dollárnál kevesebb költség mellett végzett el egy mérnöki munkát, amelyhez három szakértőnek öt hónap kellett.**

Chuyue Sun kutatásában az AI a Signal üzenetküldő alkalmazás titkosításáért felelős kód egy részét ellenőrizte. A formális verifikáció célja régóta, hogy **matematikai módszerekkel bizonyítsák** a szoftver hibamentességét, de a folyamat hosszú és munkaigényes.

A &Truth vállalat 70 millió dollárt gyűjtött, a Harmonic pedig 295 millió dollár finanszírozást kapott. Az Anthropic és a Theorem közösen jelentette be, hogy AI-val segítettek hibákat találni nyílt forráskódú szoftverekben, amelyeket korábbi tesztek sem találtak meg. A technológia még **prototípus-fázisban van**.

Szkeptikusok szerint a módszer nem szűri ki a felhasználói hibákat és a hardverhibákat, a hibakereső AI-szoftvert fejlesztő Antithesis vezetője szerint pedig csak **kimerítő tesztelés igazolhatja**, hogy a biztosíték valós. A cégek közlése szerint Boeing-gépekben, Amazon-szerverekben és több mint 2,5 milliárd aktív Apple-eszközben is van legalább részben formálisan ellenőrzött szoftver.

## Miért számít?

Ha az AI csökkenti a verifikáció költségét, a módszer a kritikus rendszereken túl is elterjedhet, a vevők fizetési hajlandósága viszont még nem ismert. **Elterjedés a kritikus rendszereken túl**

---

Eredeti forrás: [The ‘Pain in the Ass’ Math That Could Save Vibe Coding From Itself](https://www.wired.com/story/software-verification-is-the-hot-new-answer-to-the-ai-safety-crisis)

Forrás: xhírek.hu – https://xhirek.hu/hir/az-ai-val-a-formalis-szoftververifikacio-is-elerhetobbe-valhat