id: move-prover title: 形式验证代码 custom_edit_url: https://github.com/move-language/move/edit/main/language/move-prover/README.md

此子树下的代码是实验性的。在它不再被标记为实验性之前，它不在 Diem Bug Bounty 的范围内。

Move 验证器

Move 验证器支持 Move 代码的形式化规范和验证。它可以自动证明 Move 智能合约的逻辑属性，同时提供类似于类型检查器或代码质量检查器的用户体验。其目的是使合约更加 可信，具体包括

• 保护 Diem 区块链管理的巨额资产免受智能合约错误的影响
• 抵御资源丰富的对手
• 预见合理的监管审查和合规要求
• 允许具有数学背景但可能没有软件工程背景的领域专家理解智能合约的功能

有关更多信息，请参阅文档

• [待完成] Move 验证器白皮书
• Move 验证器用户指南
• Move 规范语言
• 安装
• 测试
• [待完成] Move 验证器开发者指南