In recent years, tiny rounding mistakes, often as small as 1 wei, have cost DeFi protocols over $100 million. Because the EVM only handles integers, every division forces a round‑up or round‑down decision, creating subtle gaps that attackers can exploit at scale. Learn how formal verification tools can systematically prove your contracts’ invariants and reveal hidden rounding bugs before they go live.