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 的核心理念是讓開發者通過編寫規範來驅動代碼生成，同時自動產生可機器檢查的證明，從而大幅提升軟件的正確性和開發效率。