Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny

TL;DR

This paper demonstrates the formal verification of a token sale launchpad's core logic using Dafny, ensuring critical safety properties and correctness of complex financial operations through a compositional approach.

Contribution

It introduces a compositional verification strategy in Dafny for complex smart contract logic, including safety proofs for refunds, lifecycle, and financial calculations.

Findings

Refunds never exceed user deposits

Financial calculations have strictly bounded precision loss

Lifecycle and token allocation logic verified for correctness

Abstract

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.