Formal Verification of TON Master Chain Contracts

This report describes a formal verification of the TON blockchain's elector smart contract (and related config contract), detailing the modeling in Coq, an accounting invariant proved for funds tracking, the proof effort (including loop invariants and lemmas), and two bugs discovered: a minor message-accounting omission and a critical logic error that can permanently lock excess bid funds when users exceed max_stake. The authors conclude that formal verification complemented manual audits by finding issues that were previously missed and recommend combining both approaches for high-assurance critical code.