A minimalistic blockchain consensus implemented and verified in Coq | Heykuki News