基于 Dafny 的代币发行launchpad形式化验证：组合化方法

去中心化金融(DeFi)系统和智能合约的不断增长凸显了软件正确性的关键需求。此类系统中的漏洞可能导致灾难性的财务损失。形式化验证提供了实现软件行为数学确定性的途径。本文提出了使用 Dafny 编程语言和验证系统实现并证明正确性的代币发行launchpad核心逻辑的形式化验证。我们详细阐述了一种组合化、自下而上的验证策略，首先对基本的非线性整数算术属性进行证明，然后逐步验证复杂的业务逻辑，包括资产转换、基于时间的折扣以及限额出售的退款机制。本文的主要贡献在于对关键安全性和生命周期属性的形式化证明。最显著的是，我们证明了限额出售中的退款绝不会超过用户原始存款金额，同时验证了舍入后金融计算精度损失严格受到限制。此外，我们还验证了完整的生命周期逻辑，包括在各种出售机制下用户的提款，以及出售后代币的分配、归属和索取的正确性。这一工作为将严格的验证技术应用于构建高保证金融软件提供了全面的案例研究。