Verdi currently supports verifying safety properties, but not liveness properties, and none of Verdi’s network semantics currently capture Byzantine fault models. We believe that Verdi could be extended to support these features: liveness properties could be verified by supporting infinite traces and adding fairness hypotheses as axioms as in TLA, while Byzantine fault models can be supported by adding more non-determinism in the network semantics.
TLA-style state-machine refinement and Hoare-logic verification (Dafny, an SMT-based program verification toolchain)
from Verdi Raft's paper,
This approach enables building practical distributed systems and proving both safety and, unlike our Raft proof in Verdi, liveness properties.
Also unlike our Raft implementation in Verdi, IronFleet’s implementation of Paxos supports many important practical features including verified marshaling and parsing, state transfer, and log truncation