Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny. - Evgeny Ukhanov (CoRR, 2025)