募得7,000萬美元種子資金，&Truth投入AI形式驗證自動化

形式驗證新創公司 &Truth 宣布募得7,000萬美元種子資金（約935億韓元），並計畫結合AI與自有技術，縮短證明軟體符合需求條件所需的時間。

&Truth於29日（當地時間）發布成立公告，表示公司結束隱密營運，正式公開業務。資金來自一個由AI安全與創投領域人士組成的團體；公司未公布個別投資人及估值。

美國國家標準暨技術研究院（NIST）將形式驗證說明為一套程序：先正式描述需求，再以數學模型表示實作，最後透過邏輯規則證明實作符合規格。

一般軟體測試會以選定的輸入值執行程式，再檢視結果；形式驗證則是證明規格所列條件是否成立。

這類證明只在規格界定的範圍內有效。即使結果顯示程式符合需求，也不能據此認定需求已完整反映實際使用環境與原意。

&Truth表示，將在證明撰寫過程中導入AI與自有自動化技術，並以驗證多種程式語言的程式碼為目標。

公司聲稱，AI可讓證明生成速度提升100倍以上，自有技術還能再帶來100倍的速度提升。依公司說法，原本需耗時數月或數年的工作，有望縮短至數小時或數分鐘。

這些速度提升數字是公司提出的效能目標。成立公告未提供可獨立重現這些數字的評估結果。

Anthropic於10月22日公布與Theorem合作進行的形式驗證研究成果。該研究是獨立進行的工作，並未評估&Truth的產品或效能。

研究團隊為123個開源函式庫中的239個入口點建立證明，確認在輸入大小不超過64MB時，程式不會崩潰。

研究團隊修正證明過程中發現的缺陷後，再驗證結果。驗證範圍僅限於單執行緒靜態RISC-V二進位檔，以及研究團隊建模的Linux環境等特定條件。

Anthropic說明，這項結果不代表整個函式庫沒有錯誤。證明驗證器會檢查提交的證明是否符合規格，但無法判斷規格是否完整反映實際需求與環境。

25日，Reddit的RISC-V看板一篇貼文下，有人表示難以信任AI撰寫的證明，也有人回應應以證明驗證器作為判斷結果可信度的依據。該貼文獲得23個推薦，單一貼文不足以代表整體業界看法。

形式驗證也曾應用於虛擬資產領域。Zcash（ZEC）Ironwood的餘額完整性驗證包含超過2,700項形式驗證定理；這並不表示該案例與&Truth的產品或客戶有關。

&Truth以驗證多種程式語言的程式碼為目標，但成立公告未提出專為智能合約或區塊鏈程式碼設計的產品，也未提供相關客戶案例。