Formal verification of the Stellar Consensus Protocol
The .thy files are Isabelle/HOL theories. FBASystem.thy formalizes some definitions and proofs of the Stellar whitepaper, while PersonalQuorums.thy formalizes a simpler take on federated voting.
SCP.ivy formalizes and proves safety of the ballot protocol. Can be checked with IVy: https://microsoft.github.io/ivy/