FFG has this too, see here. It looks less formal, but keep in mind that the portion of CBC’s proofs that are more formal are the generic ones that assume pre-existing safety oracles; proofs for any specific oracles are still quite rough.
FFG has this too, with variable epoch lengths.
But generally, like I’ve said, it seems that it would be less work in the long-run to go straight to implementing CBC.
I’m inclined to disagree; much of the machinery in FFG is quite transferable to a CBC setting. Consider:
- Signature aggregation (CBC will require more advanced aggregation eg. going straight to STARKs, but the same network pathways would be in use, similar DoS considerations would need to be analyzed, etc)
- The beacon chain: fully transferable
- Random beacon: fully transferable
- Validator shuffling: fully transferable
- Dynasty switching: “full” CBC does have a different scheme for validator induction; this would require more work