产品简介
Armada 是一个专为高性能并发程序设计的形式化验证工具。它允许开发者使用类似C的语言编写程序，并通过自动化验证确保正确性，同时保持性能。适合需要安全编写并发代码的软件开发者，解决了手动验证困难、易出错的痛点。
核心功能
- 形式化验证并发程序正确性
- 支持自定义内存布局和同步原语
- 使用SMT自动化减少验证努力
- 集成rely-guarantee等高级推理技术
- 验证后性能与未验证代码相当
快速开始
- 安装.NET 5.0运行时、pip和scons（通过`pip install scons`）
- 下载并安装Dafny v3.2.0
- 运行`scons -j
-f SConstruct1`生成证明 - 运行`scons -j
-f SConstruct2 --DAFNYPATH= `验证证明
界面预览
与其他方案对比
| 对比项 | Armada | 同类方案 |
|---|---|---|
| 验证方式 | 自动化形式化验证，使用SMT和推理技术减少开发者努力 | 传统手动验证或忽略验证，难度高且易出错 |
| 性能开销 | 验证后性能与未验证代码相当 | 可能因验证引入额外性能损耗 |
适合谁用
- 需要编写高性能并发程序的系统开发者
- 在并发编程中追求程序正确性的软件工程师
- 研究形式化验证方法的技术研究人员
下载与版本
当前最新版本为 main，发布于 。支持 Windows、macOS、Linux。
⚠️ 注意：本项目仅提供源代码下载，不包含可直接运行的安装包（exe/dmg/apk 等。下载后需要自行编译构建才能使用，适合有一定开发经验的用户。如果你不熟悉编译流程，建议寻找同类开箱即用的替代方案。
注意事项
- 本工具仅供学习和研究使用，请遵守相关法律法规。
- 请尊重内容创作者版权，勿将下载内容用于商业或非法传播。
- 项目源码地址：https://github.com/microsoft/Armada