Skip to Main content Skip to Navigation

A Foundational Framework for the Specification and Verification of Mechanism Design

Pierre Jouvelot 1, 2 Emilio Jesús Gallego Arias 3 
3 PI.R2 - Design, study and implementation of languages for proofs and programs
CNRS - Centre National de la Recherche Scientifique, Inria de Paris, UPCité - Université Paris Cité, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
Abstract : We introduce mech.v, a new framework for the specification and verification of mechanisms, implemented using the Coq interactive theorem prover and the Mathematical Components library. We provide a general definition of mechanism, a subclass capturing auctions, and a few examples of auctions including three notions of Vickrey-Clarke-Groves (VCG), proving their main incentive properties such as truthfulness with reasonable verification effort. We define and prove some more lemmas and definitions usually found in the mechanism design (MD) literature such as Pareto-optimality, rationality, dominance and Nash equilibria. We also define a mechanism refinement system, which we use to relate the implementation of an efficient version of the VCG mechanism for an online advertisement auction to the general VCG specification, allowing us to transfer the truthfulness property from the generic proof. We hope that our library can be useful as a formally verified, unambiguous reference with applications ranging from verification of deployed mechanism to education, and that this is a first step to gather interesting results and definitions from the MD literature to eventually provide a comprehensive mechanically formalized reference.
Complete list of metadata
Contributor : Claire Medrala Connect in order to contact the contributor
Submitted on : Thursday, May 12, 2022 - 5:47:56 PM
Last modification on : Tuesday, September 6, 2022 - 1:27:06 PM


Files produced by the author(s)


  • HAL Id : hal-03666871, version 1


Pierre Jouvelot, Emilio Jesús Gallego Arias. A Foundational Framework for the Specification and Verification of Mechanism Design. [Research Report] E-458.PDF, MINES ParisTech - PSL Research University. 2022. ⟨hal-03666871⟩



Record views


Files downloads