The proliferation of decentralized financial (DeFi) systems and smart contracts has underscored the critical need for software correctness. Bugs in such systems can lead to catastrophic financial losses. Formal verification offers a path to achieving mathematical certainty about software behavior. This paper presents the formal verification of the core logic for a token sale launchpad, implemented and proven correct using the Dafny programming language and verification system. We detail a compositional, bottom-up verification strategy, beginning with the proof of fundamental non-linear integer arithmetic properties, and building upon them to verify complex business logic, including asset conversion, time-based discounts, and capped-sale refund mechanics. The principal contributions are the formal proofs of critical safety and lifecycle properties. Most notably, we prove that refunds in a capped sale can never exceed the user's original deposit amount, and that the precision loss in round-trip financial calculations is strictly bounded. Furthermore, we verify the complete lifecycle logic, including user withdrawals under various sale mechanics and the correctness of post-sale token allocation, vesting, and claiming. This work serves as a comprehensive case study in applying rigorous verification techniques to build high-assurance financial software.

翻译：去中心化金融（DeFi）系统和智能合约的激增凸显了软件正确性的关键需求。此类系统中的漏洞可能导致灾难性的财务损失。形式化验证为实现软件行为的数学确定性提供了一条路径。本文介绍了一个代币销售启动平台核心逻辑的形式化验证，该验证使用Dafny编程语言和验证系统实现并证明其正确性。我们详细阐述了一种组合式、自底向上的验证策略：从证明基本的非线性整数算术属性开始，并在此基础上验证复杂的业务逻辑，包括资产转换、基于时间的折扣机制以及限额销售的退款机制。主要贡献在于对关键安全属性和生命周期属性的形式化证明。最显著的是，我们证明了限额销售中的退款金额永远不会超过用户的原始存款金额，并且往返金融计算中的精度损失被严格限定。此外，我们验证了完整的生命周期逻辑，包括不同销售机制下的用户提款，以及销售后代币分配、归属和申领的正确性。本工作为应用严格验证技术构建高可信度金融软件提供了一个全面的案例研究。