(disclaimer: I had early access to the whitepaper for review)

You should look in the white paper[0] to the definition of an FBAS which differs from epaxos (while epaxos is egalitarian, SCP is federated). All related proofs are included in the whitepaper, the central one being theorem 3 in 4.2. Finally the protocol specification (Figure 15, p28) is also very interesting.

[0] https://www.stellar.org/papers/stellar-consensus-protocol.pd...