Alpenglow Verifier

Property Definitions

Formal definitions for safety, liveness, and resilience properties of Alpenglow.

Ensuring Correctness
These properties ensure that nothing bad ever happens, such as finalizing conflicting blocks or accepting forged certificates.

* @type: safety;
* @description: "Ensures no two conflicting blocks are ever finalized in the same slot.";
NoConflictingBlocksFinalized ==
    A sl in DOMAIN finalized:
        Cardinality(finalized[sl]) <= 1

* @type: safety;
* @description: "Guarantees that certificates are unique for each slot and cannot be forged.";
CertificateUniqueness ==
    A sl in DOMAIN certs:
        Cardinality(certs[sl]) <= 1

* @type: safety;
* @description: "Prevents Byzantine nodes from causing validators to vote for conflicting blocks in the same slot.";
NoEquivocation ==
    A n in Nodes:
        A sl in DOMAIN votes:
            A v1, v2 in votes[sl][n]:
                v1.block = v2.block