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