Abstract VCG: Tie-breaking rules in VCG mechanism design

We present computer-checked solutions to the tie-breaking problem in Vickrey-Clarke-Groves (VCG) auctions for Sponsored Search, addressing scenarios involving equal bids. We formally prove that our solution preserves the incentive compatibility property. Both the specification and verification of this theorem are carried out using mech.v, a formal framework for mechanism design built on top of the MathComp library within the Rocq proof assistant. As mech.v and its applications continue to evolve, we aim to contribute not only provably correct algorithms but also reusable tactics for the development of machine-checked proofs in mechanism design.