Isabelle logo

Manuel Eberl

Chair for Logic and Verification

Verifying Randomised Social Choice

by Manuel Eberl

In: Proceedings of FroCoS 2019

Best Paper by a Junior Researcher




This work describes the formalisation of a recent result from Randomised Social Choice Theory in Isabelle/HOL. The original result had been obtained through the use of linear programming, an unverified Java program, and SMT solvers; at the time that the formalisation effort began, no human-readable proof was available. Thus, the formalisation with Isabelle eventually served as both independent rigorous confirmation of the original result and led to human-readable proofs both in Isabelle and on paper.

This presentation focuses on the process of the formalisation itself, the domain-specific tooling that was developed for it in Isabelle, and how the structured human-readable proof was constructed from the SMT proof. It also briefly discusses how the formalisation uncovered a serious flaw in a second peer-reviewed publication.

Download preprint PDF (452 KiB)


  author = "Eberl, Manuel",
  editor = "Andreas Herzig and Andrei Popescu"
  title = "Verifying Randomised Social Choice",
  year = "2019",
  booktitle = "Frontiers of Combining Systems, {FroCoS} 2019",
  series = "Lecture Notes in Computer Science",
  publisher = "Springer",
  volume = "11715",
  doi = "10.1007/978-3-030-29007-8_14"

Download BibTeX (366 Bytes)

(The final publication is available at