Randomised Distributed Algorithms Library in Coq
Allyx Fontaine and Akka Zemmari
This our work on the formal specification and analysis of randomised distributed algorithms.
A first draft implementation in Coq8.4 and ssreflect1.4, using Alea Library, developed by A. Fontaine and A. Zemmari is available here:
This is clearly a work in progress. Many definitions and proofs are too long and are being improved little by little.