A couple of weeks ago I got nerd sniped into writing a TLA+ specification for the Viewstamped Replication Revisited paper. I have written specifications for multiple variants of Raft, Apache BookKeeper, SWIM, Kafka replication, Kafka consumer group protocol, RabbitMQ streams replication and many more including some protocols that are not publicly available. But VR Revisited has been more challenging than most, not because it is more complex, but because the paper is hard to interpret.