This repository contains a TLA+ specification and TLC model checking configuration for Fast Flexible Paxos.
This specification is the result of only a minor modifications to the original Fast Paxos specification by Leslie Lamport.
Instructions for installing and setting up TLA+ are available elsewhere.