The latest developments on probability in Coq are as follows.
ALEA
The ALEA probability library was revived for Coq 8.11 and later:
Ceramist
The Ceramist project verified probabilistic data structures such as Bloom filters in an axiom-free way:
1 Like