on reading safety and liveness proofs of consensus protocols, I have observed a pattern, a template in a fixed set of quorum intersection lemmas being always needed. if this true, can't we just write this as a bunch of lego boxes in formal language and have this boxes be always run on for any new consensus protocol? seems like R&D of newer consensus protocols based on app-layer requirements can be expedited, instead of waiting for years.