SPECIFICATION Spec
INVARIANT TypeOK
INVARIANT FinalizedImpliesBlobsPresent
INVARIANT AtMostOneManifest
INVARIANT BeliefAccurate
INVARIANT CliFinalKnowledgeSound
CHECK_DEADLOCK FALSE