aallan/vera

解決的問題

LLM 在程式碼連貫性、維護大型程式碼庫中的不變性以及狀態推理方面經常遇到困難。它們容易出現命名錯誤並遺失變數識別。Vera 透過將變數名稱替換為結構化引用，並要求每個函數都具有顯式且可驗證的契約來解決這些問題。

工作原理

Vera 使用一種獨特的方法來確保程式碼的正確性：

• 結構化引用： 使用帶類型的 De Bruijn indices（例如 @Int.0）而不是變數名稱，以避免與命名相關的錯誤。
• 強制契約： 每個函數必須聲明 requires（前置條件）、ensures（後置條件）和 effects（副作用）。
• 靜態驗證： SMT 求解器 (Z3) 嘗試在編譯時證明這些契約成立。
• 三層驗證： 如果契約無法透過靜態方式證明，編譯器會插入執行時守衛，以便在發生靜默失敗之前捕捉錯誤。
• 以代理為中心的診斷： 錯誤被設計為 LLM 的指令，提供解決問題的原理與具體的程式碼範例。

適用對象

• LLM 代理： 該語言專為 AI 模型編寫而優化，具有針對代理工作流量身定制的文件 (SKILL.md) 與指令 (AGENTS.md)。
• 構建 AI 驅動系統的開發人員： 那些需要由模型生成高保證程式碼的人員。

亮點

• 編譯為 WebAssembly，可在 CLI、瀏覽器或 WASI Preview 2 宿主機中執行。
• 具有顯式的副作用系統，用於追蹤 <Inference> 或 <Http> 等副作用。
• 包含用於編輯器支援的語言伺服器協定 (LSP)。
• 包含基準測試 (VeraBench)，顯示與傳統語言相比，模型編寫 Vera 的成功率更高。