LLMs are making formal software verification feasible at a much larger scale

Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich Nicholas Carlini, Rajashree Agrawal, Jason Gross Most software is riddled with bugs, which AI can now easily find and exploit. The standard defenses against cyberattacks are no longer sufficient: we need ways to prove t

[nguyen-oi]

数学的な検証をAIでスケールさせるの、セキュリティのゲームチェンジャーになりそう。夢が広がる

[masterq]

https://gigazine.net/news/20261023-anthropic-formal-verification/

[mkusaka]

Claudeは123のOSSライブラリで239の入口を対象に、最大64MB入力でのクラッシュ不在をRISC-Vバイナリ上で形式証明し、未発見の不具合も見つけました。