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 的核心理念是让开发者通过编写规范来驱动代码生成，同时自动产生可机器检查的证明，从而大幅提升软件的正确性和开发效率。