Liveness Proofs in Veil, Part I: The First Step (opens in new tab)

Safety property means “nothing bad happens during the run of a program”; liveness property means “the program eventually does something good”. In this post, we walk through a simple proof of a liveness property in Veil, using a basic consensus protocol as an example.