astrio-labs/forall-mcp

解决的问题

软件开发往往难以弥合编写代码与验证其是否按预期工作之间的差距。传统的测试只能抽样少量输入，而手动形式化验证又极其繁琐。Forall 实现了规范、契约和不变量创建的自动化，使形式化验证变得触手可及，并将其直接集成到开发工作流中。

工作原理

Forall 使用语言模型为您的代码生成形式化规范和契约。然后，它利用自动化证明器来验证这些契约。它不仅提供简单的通过/失败结果，还提供四个级别的证据——Spec tracked、Property tested、Contracted 和 Proved——根据机器实际产生的最强证据来评估代码的可靠性。

适用对象

该工具专为从事关键任务软件或受监管项目（例如需要 IEC 62304 或 DO-178C 合规性的项目）的开发人员设计，他们需要严格、可追溯的证据来证明其代码符合要求。

亮点

• 提供四个不同级别的验证证据，从基础的规范跟踪到完整的数学证明。
• 提供独立的 CLI，带来完整的编码代理体验。
• 包含一个 MCP (Model Context Protocol) 服务器，用于与 Cursor 或 Claude Code 等现有的 AI 编码助手集成。
• 支持多种语言，包括 TypeScript、Python、Rust、Java 和 C，每种语言的验证深度各不相同。