Espresso HotShot Epoch Changes in Quint

How we used Quint to formalize Espresso's epoch change protocol with executable specifications.