aallan/vera

解決的問題

模型在規模擴大時難以維持一致性，難以推理狀態，也難以管理變數名稱，這常導致命名相關錯誤並失去對值的追蹤。Vera 是一種專為大型語言模型撰寫程式碼而設計的程式語言，以結構化引用取代傳統變數名稱，並強制要求契約以確保程式碼可被機械化驗證。

工作原理

Vera 以帶型別的槽位參考（例如 @Int.0 表示最近的整數綁定）取代變數名稱。它使用 SMT 求解器（Z3）在每個呼叫點靜態證明前置條件（requires）與後置條件（ensures）。該語言預設為純函數，函數簽章中必須顯式宣告副作用（如 <Http> 或 <Inference>）。程式碼編譯為 WebAssembly，可在命令列、瀏覽器或 WASI Preview 2 組件中執行。

適用對象

以 AI 代理與 LLM 為主要程式碼撰寫者的場景，以及希望生成形式化驗證、安全且無命名衝突程式碼的開發者。

特色亮點

帶型別的槽位參考：透過使用結構化參考而非變數名稱，消除命名錯誤。
強制契約：每個函數必須宣告前置條件與後置條件，編譯器透過 Z3 靜態證明其正確性。
顯式副作用類型：副作用在簽章中顯式標註，防止未授權的操作。
面向代理的診斷優化：編譯器錯誤以模型可理解的指令形式呈現，提供推理依據與具體修復範例。
設計即安全：透過在類型檢查階段強制字串來源規則，防止 SQL 注入等常見漏洞。
多目標編譯：可編譯為 WebAssembly，在 CLI、瀏覽器與 WASI 0.2 主機上執行。