This an implementation of single-decree paxos, used for concesnsus in distributed systems. This implementation has been formally verified through model checking via stateright.
See #1
Good lesson here is that your verification is only as good as your spec.