研究突破
DeepMind 以 AlphaProof Code 生成 650 萬行 Lean 證明，正式驗證 Signal 協定核心代碼
Google DeepMind 發表 AlphaProof Code，結合人類專家與 AI 代理對軟體進行形式驗證，並應用於 Signal 協定的參考實作 libsignal：Carbon 驅動的代理生成了約 650 萬行 Lean 證明，驗證前向保密、後洩漏安全與認證等保證，且證明覆蓋編譯後的機器碼而非僅設計層面。五人團隊四週完成的工作，傳統上需專家耗時數年，顯示 AI 正把過去過於昂貴的形式驗證變成可工程化的紀律。