Or if you're interested in the opposite of pseudocode, here's a TLA+ spec for Paxos.

Related to yesterday's TLA+ video post https://news.ycombinator.com/item?id=13918648