ao ler sobre a segurança e as provas de vivacidade de protocolos de consenso, observei um padrão, um modelo em um conjunto fixo de lemas de interseção de quórum que são sempre necessários. se isso for verdade, não podemos apenas escrever isso como um monte de caixas de lego em uma linguagem formal e fazer com que essas caixas sejam sempre executadas para qualquer novo protocolo de consenso? parece que a P&D de novos protocolos de consenso baseados em requisitos de camada de aplicativo pode ser acelerada, em vez de esperar anos.