🌗 大型語言模型正讓大規模形式軟體驗證成為可能 \ Anthropic ➤ 結合 AI 與形式方法：從測試進化為嚴密的數學證明 ✤ https://www.anthropic.com/research/formal-verification Anthropic 研究團隊利用 Claude 模型突破了軟體安全領域的長年障礙，成功將形式軟體驗證推向大規模應用。透過將現有的模糊測試（Fuzz testing）自動轉化為形式規格，並讓 AI 在 RISC-V 組合語言層級自動生成證明，研究人員已在一百多個開源庫中證明了安全屬性，甚至發現了存在多年的隱藏漏洞。這項技術大幅降低了形式驗證的人力成本，讓「數學證明」等級的軟體安全保障從航太工業走向主流軟體開發。 + 將形式驗證從不可能的任務轉變為自動化流程，這絕對是軟體安全史上的里程碑。 + 雖然目前仍有單執行緒等假設限制，但能在組合語言層級直接產出證明，展現了大型語言模型在極端邏輯任務上的驚人潛力。 #形式驗證 #AI安全 #軟體開發 #Claude #漏洞修復