Forall：基於規範驅動、附帶形式驗證的AI程式設計工具
Astrio 推出 Forall（∀），一個透過規範驅動生成程式碼並附帶機器可驗證證明的程式設計助手。支援 CLI 和 MCP 兩種使用方式，目前相容 TypeScript、Java 和 Rust，基於 Apache-2.0 開源。
Astrio 團隊正式釋出了 Forall（∀），這是一款基於規範驅動的 AI 程式設計助手，能夠在生成程式碼的同時附帶機器可驗證的形式化證明。Forall 的目標是幫助開發者構建更可靠的軟體，減少因邏輯錯誤導致的缺陷。
Forall 提供了兩種使用方式。第一種是安裝完整的命令列介面（CLI），使用者可以透過終端完成程式碼編寫、規範制定和證明生成的全部流程。安裝命令簡單，只需執行 curl -fsSL https://forall.astrio.app/install.sh | bash，首次使用時需要註冊 Forall 賬號或自帶 OpenAI / OpenRouter API 金鑰。第二種方式不安裝 CLI，而是透過模型上下文協議（MCP）整合到現有 IDE 如 Cursor、Claude Code 或 Codex 中，僅呼叫遠端驗證服務。使用者需在 Forall 官網建立 API 金鑰，然後配置 MCP 客戶端即可。
目前 Forall 支援 TypeScript、Java 和 Rust 三種程式語言，並計劃根據社群需求擴充套件更多語言。整個專案採用 Apache-2.0 許可證開源，託管在 GitHub 上。Astrio 還提供了 Discord 和 X 社群供開發者交流。目前該專案在 GitHub 上獲得了 160 顆星和 21 個分叉，已釋出 v0.1.0 版本。Forall 的核心理念是讓開發者透過編寫規範來驅動程式碼生成，同時自動產生可機器檢查的證明，從而大幅提升軟體的正確性和開發效率。