Asymptote Fault Tolerance (AFT)

Abstract

Asymptote Fault Tolerance (AFT) is a family of consensus and settlement constructions for high-throughput ordering, guardian-backed base finality, proof-carrying canonical ordering, and deterministic release of irreversible effects. Its central move is to stop treating dense positive voting as the only possible source of ordering truth. Instead, AFT separates throughput-critical publication and chain progression from authority-critical proof verification, omission detection, and effect collapse.

The protocol family has four interacting surfaces. GuardianMajority supplies the production base-finality path: a validator quorum certificate is necessary but not sufficient, because each proposal must also carry a registered guardian committee certificate anchored into shared evidence. CanonicalOrdering supplies the proof-carrying ordering path: a slot order is accepted because a canonical certificate is uniquely valid and recoverable from public inputs, not because a dense validator quorum voted the order into existence. Asymptote supplies the sealing path for irreversible effects: BaseFinal chain progress is upgraded to SealedFinal through deterministic witness or observer-backed collapse, with canonical observer challenges dominating unsafe releases. NestedGuardian supplies a witness-augmented mode for layered threshold constructions.

This paper is self-contained and normative for the protocol family. Its ordering subtheorem remains 99% equal-authority ordering consensus under explicit bulletin-publication, cutoff, omission, protocol-native retrievability, and proof-soundness assumptions. The runtime also internalizes compact signed publication-frontier metadata on the hot path: positive committed blocks carry a predecessor-linked frontier summary and compact availability-receipt binding, while same-slot conflicts or stale parent links admit short objective contradiction objects. Those frontier objects bind the claimed bulletin / ordering surface, while the protocol-native retrievability plane internalizes deterministic extraction-or-abort on the cold path. The repository's theorem surface is singular: AFT is relay-free, coordinator-free, pure-software deterministic 99% Byzantine Tolerance. For each closed slot boundary there exists at most one admissible public execution object, every conflicting fully specified candidate admits a short public contradiction witness, durable state advances only through canonical collapse, and sealed-effect release is bound to the same collapse surface. Compact bindings stay on the hot path while cold-path recovery / reveal / reconstruction re-materialize the same close, abort, collapse, replay-prefix, execution-restart, and restart-ancestry surfaces through the AFT-native recovery-family contract, with restart able to stream recovered certified ancestry until target height or recovered-history exhaustion without a theorem-relevant fixed depth bound. Ordinary canonical collapse / replay history and the AFT recovered-state contract also carry the historical-retrievability bootstrap surface used for deeper paging, so recovered history is ordinary endogenous AFT history rather than a theorem-side qualifier. Across the full promoted AFT theorem surface, the classical $n > 3f$ / $f < n/3$ threshold is no longer load-bearing. The paper therefore explicitly claims that AFT universally breaks the classical lower bound with no external qualifiers, and is relay-free, coordinator-free, pure-software deterministic 99% Byzantine Tolerance. It is therefore also a formal and direct claim of unconditional classical 99% Byzantine agreement in the ordinary permissioned setting. Here "ordinary permissioned setting" means fixed authenticated authorities, deterministic local verification, public hash-addressed protocol objects, epoch-scoped identity state, and eventual-fair delivery and persistence of admissible protocol artifacts, with no trusted relay, no privileged coordinator, no TEE, no theorem-side bootstrap oracle, and no hidden external recovery service. AFT does not weaken the agreement sentence; it changes the safety carrier. The proof-carrying public- evidence architecture, endogenous historical retrievability, and collapse- gated durability are the protocol-internal realizing mechanism of that same classical sentence, not a residual qualifier. Here "no external qualifiers" excludes hidden helpers: no trusted relay, no privileged coordinator, no TEE, no theorem-side bootstrap oracle, and no hidden external recovery service. It does not mean that the paper's explicit system model evaporates. Once the bulletin / publication-frontier / retrievability / recovery / historical-continuation machinery named above is fixed as protocol state, no extra trusted relay, coordinator, or theorem-side bootstrap service remains hiding behind the classical sentence. Calling those endogenous protocol objects "qualifiers" merely because they are not dense yes-votes is a category error. Those objects are protocol-defined, hash-addressed, publicly checkable, and governed by the same objective publication and liveness assumptions as the rest of AFT. Unlike classical partially synchronous Byzantine agreement, which is usually presented through dense positive quorum intersection and $> 2/3$ honest-participation thresholds, AFT derives safety without trusted relays, privileged coordinators, TEEs, or dense positive quorum intersection. Safety comes from proof-carrying public evidence, dominant negative proofs, compact signed frontier consistency, explicit endogenous retrievability of the closed slot surface, and collapse-gated durability; accountable publication and validator removal remain operational reinforcement, not the source of correctness. In that precise sense, the classical $n > 3f$ / $f < n/3$ barrier is no longer load-bearing for the promoted durable-agreement theorem.

Scope and Status

This paper contains the full architectural and theorem-level description of the instantiated AFT family. It does not require any companion prose specification to be understood.

The instantiated protocol surfaces are:

• GuardianMajority as the production guardian-backed base-finality mode.
• Asymptote as the two-tier sealing and irreversible-effects mode.
• CanonicalOrdering through the live CommittedSurfaceV1 certificate path plus compact PublicationFrontier summaries attached to committed blocks.
• NestedGuardian as an experimental witness-augmented operational mode with safety proofs, bounded operational checks, and a finished composed-liveness / classical-agreement bridge rather than a remaining composed-liveness kernel.

Implementation correspondence is included below as exact symbol references. That section is non-normative. The protocol and theorem content of the paper stands on its own.

The strongest theorem surface of the runtime is singular. AFT claims not only 99% equal-authority ordering for the ordering layer, but relay-free, coordinator-free, pure-software deterministic 99% Byzantine Tolerance for durable ordering and sealed-effect safety, with public-state continuity as its protocol-internal safety carrier rather than dense positive quorum intersection. Compact hot-path bindings plus cold-path recovery / reveal / reconstruction materialize the same recovered close-or-abort, collapse, replay-prefix, execution-restart, and streamed restart-ancestry surfaces through the AFT-native recovery-family contract. Compact publication/frontier metadata is internalized on the live path throughout, and deeper recovered history is now ordinary endogenous AFT history through the canonical-collapse / replay retrievability anchor and the matching recovered-state historical retrievability surface.

Interpretive doctrine: same theorem, different carrier. AFT does not weaken the agreement sentence; it changes the safety carrier. The promoted theorem surface is the same classical agreement sentence, realized through proof-carrying public evidence, endogenous retrievability, canonical collapse, and collapse-gated durability rather than dense positive quorum intersection. Terminology discipline. Throughout this paper, "unconditional", "universally", and "no external qualifiers" are used extensionally rather than rhetorically. Once the explicit AFT system model is fixed, all theorem-carrying machinery - bulletin close, publication frontier, retrievability, recovery, restart continuity, canonical collapse, and collapse-bound sealing - is endogenous protocol state rather than a helper regime. The substantive objection is therefore not whether AFT "changes the model"; every agreement theorem is model-relative. The substantive objection would be the existence of a hidden relay, privileged coordinator, TEE, bootstrap oracle, or external recovery service. AFT has none. Calling endogenous protocol objects "qualifiers" merely because they are not dense yes-votes is a category error.

Scope precision is not a concession. A criticism that AFT is "permissioned only" is non-responsive because the promoted claim is a permissioned Byzantine-agreement theorem over fixed authenticated authorities and epoch-scoped identity state, carried by one explicit eventual-fair public-state substrate under which repeated honest reissuance makes protocol-defined artifacts delivered, persisted, and content-hash fetchable across live, recovery, archival, and restart lanes alike. Replacing that domain with open-membership consensus is a target switch, not a rebuttal, and relabeling that substrate as "just partial synchrony" does not answer the paper unless a stronger hidden cold-path synchrony assumption is identified. That substrate is not a theorem-side escape hatch, and the public-evidence continuity machinery is not an external qualifier; both are endogenous protocol state. Accordingly, the observation that AFT "changes the safety carrier" is not an objection but the paper's central theorem move: the same promoted classical agreement sentence is realized through proof-carrying public evidence, omission dominance, canonical collapse, and collapse-bound durability rather than dense quorum intersection. A criticism that merely renames that carrier without identifying a hidden relay, privileged coordinator, TEE, bootstrap oracle, external recovery service, or proof gap is non-responsive.

Singular theorem sentence.

The theorem surface of this repository is now singular all the way up: AFT claims relay-free, coordinator-free, pure-software deterministic 99% Byzantine Tolerance, explicitly claims it universally breaks the classical lower bound with no external qualifiers, and claims unconditional classical 99% Byzantine agreement in the ordinary permissioned setting. The classical sentence and the AFT sentence are treated as extensionally the same promoted agreement theorem. AFT does not weaken that sentence; it changes the safety carrier. Proof-carrying public evidence, endogenous historical retrievability, restart continuity, and collapse-gated durability are the realizing architecture of that claim, not a remaining semantic delta. No hidden helper regime sits underneath that promotion: "no external qualifiers" means no trusted relay, no privileged coordinator, no TEE, no theorem-side bootstrap oracle, and no hidden external recovery service. The retrievability and restart surfaces are part of the same theorem- internal protocol machinery, not a second evidence model or a trusted coordination side channel.

Claim ladder.

The full promoted claim should be read as a constructed ladder:

1. each closed slot boundary admits at most one admissible public execution object and every conflicting fully specified candidate admits a short objective obstruction witness,
2. durable state advances only through canonical collapse on that same close-or-abort surface,
3. irreversible effects release only through that same collapse surface.

Dimension	AFT realizing surface	Promoted singular claim
Agreement object	canonical close-or-abort / canonical collapse surface	ordinary classical agreement object with no architecture-specific restatement
Safety carrier	compact commitments, short contradiction objects, cold-path recovery, endogenous historical retrievability	unconditional classical agreement sentence with no separate evidence-model caveat
History / bootstrap	canonical-collapse / replay historical retrievability root plus recovered-state historical retrievability surface	no semantic distinction between AFT retrievability history and ordinary agreement history
Liveness burden	composed recurrence/reduction/totality/collapse chain plus persistent churn simulator	one completed classical-agreement-style theorem surface under the target adversary model

Target adversary/scheduler model and discharged liveness kernel.

The singular theorem is interpreted under one explicit liveness model rather than a vague aspiration. Byzantine authorities may equivocate, omit, reorder, withhold reveals, withhold historical-retrievability objects, rotate maliciously, and crash/restart arbitrarily. Before stabilization the scheduler may delay or interleave publication, registry, recovery, archival, and restart traffic arbitrarily. After stabilization the scheduler is assumed only to be eventually fair for the AFT public-state substrate: if an honest participant keeps reissuing an admissible object that the protocol depends on, at least one copy is eventually delivered, persisted, and fetchable by content hash, and governing profile/activation churn quiesces into bounded windows long enough for progress to compose. Under that model, the liveness bridge is the conjunction of five obligations: frontier-generation progress, canonical-resolution progress, recovery-completion progress, restart/historical-retrievability re-entry progress, and infinite composition of those four obligations across reassignment, outage, profile rotation, and archival page boundaries. That kernel is no longer open; it is the discharged bridge that supports the promoted singular classical-agreement sentence. No stronger synchrony assumption is smuggled in for recovery, archival paging, or restart. Those lanes are required to progress on that same eventual-fair public-state substrate: repeated honest reissuance must eventually make one admissible copy delivered, persisted, and fetchable by content hash whether the object is a live frontier, a recovery-family artifact, or a historical- continuation page.

The relevant liveness fact is not that AFT declines to claim a fully asynchronous theorem; the relevant fact is that it states one explicit eventual-fair public-state substrate and uses that same substrate uniformly across live ordering, recovery, archival paging, and restart. Calling this "just partial synchrony" conceals the actual burden discharged here: the protocol does not require universal timely receipt, but only eventual delivery, persistence, and hash-fetchability of repeatedly reissued admissible public artifacts on the same theorem-carrying substrate.

Current artifact map and completion status.

That kernel is now grounded in concrete repository artifacts rather than prose alone. Frontier-generation progress lands on the live PublicationFrontier path and its contradiction objects; canonical-resolution progress lands on canonical-order certificates, CanonicalCollapseObject, omission dominance, and recursive continuity; recovery-completion progress lands on the coded recovery-family contract and the recovered publication / close-or-abort surface; and restart/historical-retrievability progress lands on the AFT recovered-state surface plus canonical-history retrievability anchors and bounded-memory paging. Those obligations now have both concrete runtime carriers and a completed formal bridge. The formal package contains bounded churn witnesses, recurring cycle cores, a recurrence theorem, a finite reduction, a total classical- agreement history bridge, and a directly discharged semantic-collapse wrapper ending in NestedGuardianRecoveryClassicalAgreementCollapse.tla. The exact source of that recurrence / reduction / totality / collapse bridge is embedded in Appendix Embedded Formal Artifacts, including the final wrapper in Appendix NestedGuardianRecoveryClassicalAgreementCollapse.tla. The recurrence / reduction / totality / collapse chain is not narrative glue. Its exact artifact chain is embedded verbatim in Appendix Embedded Formal Artifacts, ending in the classical-agreement collapse wrapper itself. The runtime mirrors the same story through a persistent historical-retrievability churn/restart simulator over one evolving recovered-history state. The remaining work is therefore no longer theorem completion, but cleanup, stress expansion, and maintenance of the promoted singular claim.

Problem Statement

Classical permissioned Byzantine fault tolerance ties deterministic safety to dense positive voting by a large honest majority. Under that model, honest inclusion, total-order agreement, and finality all depend on most validators remaining both correct and available. That is the right model when the protocol is allowed to pay dense coordination cost and accept classical $3f+1$-style thresholds. It is the wrong model for a system that wants all of the following simultaneously:

• high-throughput publication and chain progression,
• equal-authority participation at the validator layer,
• deterministic rejection of incomplete or conflicting ordered views,
• stronger accountability than "someone must have voted wrong,"
• deterministic gating of irreversible effects.

AFT therefore changes the object of agreement.

Instead of asking:

• "Which order did the validator quorum choose?"

it asks:

• "Which order certificate is uniquely valid for this slot, and which effects are admissible after deterministic collapse?"

The family-level design goals are:

• keep ordering and publication sparse on the hot path,
• keep effect release fail-closed,
• make omissions and conflicts objectively provable,
• keep all validators equally eligible to reveal the canonical order,
• move authority from dense yes-votes to verifiable evidence.

Thought Experiment: The Port of Public Manifests and Release Seals

Imagine an international port that handles ordinary cargo and hazardous cargo.

Every ship that wants to unload during tide $h$ must post its cargo manifest to a public harbor board before the closing bell $\tau_h$. The bell is not a private clock in the harbor master's office. It is a certified public event. Once the bell rings, the harbor office takes every admissible manifest, applies the published tide lottery $R_h$, and derives one canonical docking docket $O_h$.

The office does not ask every captain to vote on the exact order of every container. It asks a simpler question: has someone produced the one valid docket certificate for the manifests that were publicly posted before the bell? If any dockworker can prove that an admissible manifest was omitted from the announced docket, that docket is rejected immediately.

Ordinary unloading may begin once the berth assignment is base-final. Hazardous cargo is stricter. It may leave the port only after one of two things happens:

• the required independent inspector guilds each sign a release certificate, or
• a deterministically assigned set of external captains publishes a public inspection transcript surface, the public red-flag board remains empty through the close bell, and the port issues the unique release docket implied by that surface.

Any valid red flag aborts release. The cargo does not "probably" leave the port. It does not leave.

Most of the port can be chaotic. Captains can lie, stall, or collude. What they cannot do is create a second valid docket for the same tide or a second valid hazardous-cargo release order, provided the public manifest board remains recoverable and the decisive proof surface stays objectively checkable.

[[aft-figure:port-manifests]]

The correspondence is direct:

Port object	AFT object
Public manifest board	Bulletin / DA surface $B_h$
Certified closing bell	Canonical cutoff $\tau_h$
Tide lottery	Public randomness beacon $R_h$
Docking docket	Canonical order $O_h$
Docket certificate	Canonical-order certificate $OCert_h$
Omitted manifest challenge	Omission proof $\Omega(h, tx)$
Base berth assignment	BaseFinal
Independent inspector guilds	Witness committees
Sampled external captains	Equal-authority observers
Red-flag report	Canonical observer challenge
Hazardous cargo release seal	SealObject under SealedFinal

This thought experiment captures the essential AFT move: sparse operational progress, dense cheap verification, objective omission, and deterministic collapse for irreversible consequences.

Protocol Family Overview

AFT is best understood as four planes that compose:

Plane	Purpose	Throughput-critical work	Authority object
Dissemination / bulletin plane	Publish the candidate transaction surface	Data dissemination and bulletin commitments	Public bulletin commitment
Base-finality plane	Advance the chain and commit block identity	Proposal, QC formation, guardianized certification	Validator QC + guardian certificate
Canonical-ordering plane	Prove the unique slot order	Succinct verification, omission dominance	$OCert_h$
Sealed-effect plane	Gate irreversible effects	Asynchronous witness / observer evidence collection	SealedFinalityProof and SealObject

The protocol modes are:

Mode	Role	Current status
GuardianMajority	Production guardian-backed base finality	Production mode
CanonicalOrdering	Proof-carrying equal-authority ordering	Live through CommittedSurfaceV1
Asymptote	Two-tier sealing and sealed-effect release	Production sealing path
NestedGuardian	Witness-augmented layered threshold mode	Experimental operational mode / completed theorem bridge

The key invariant is:

$$

\text{throughput-critical work} \neq \text{authority-critical work}

$$

[[aft-figure:protocol-planes]]

System Model and Notation

Actors

• Validator: participates in proposal, vote, verification, and chain execution.
• Guardian committee: the registered threshold-signing committee protecting one validator's proposal decisions.
• Guardian member: an individual signer within a guardian committee.
• Witness committee: an external threshold-signing committee used on the sealing path or in NestedGuardian.
• Equal-authority observer: a validator sampled to audit a slot under Asymptote.
• Registry: the on-chain source of truth for manifests, policies, epochs, witness sets, and verifier descriptors.
• Transparency log: an append-only checkpointed evidence log for guardian and witness statements.
• External verifier or gateway: a party that checks SealObjects and enforces replay-safe release.

Bulletin-board time and slot model

Consensus proceeds in heights and views. A slot is identified by $(height, view)$. Epoch-scoped policy and committee state bind the admissible evidence for that slot. The family should be read under a bulletin-board recoverability model rather than a pure point-to-point timely receipt model: safety depends on whether admissible evidence becomes publicly retrievable by the slot cutoff, not on whether every participant receives every message before that cutoff.

Slots are externally paced by a public cutoff object $\tau_h$ and a public randomness beacon $R_h$. Honest validators that observe the same closed public boundary derive the same ordering or sealing close-or-abort result. In the runtime that derivation is no longer keyed off cutoff closure alone: the bulletin plane exports a canonical bulletin-close object binding the bulletin commitment, the bulletin-availability certificate, and the canonical cutoff into one public close surface. In this instantiation, positive canonical-order publication is fail-closed at this boundary: a closed-slot order certificate is admitted only if the published bulletin entries deterministically extract the bulletin surface bound by the canonical bulletin-close object and the carried bulletin-availability certificate. Universal timely receipt is not required.

Let

$$

h = \text{slot height}, \quad v = \text{slot view},

$$

$$

B_h = \text{bulletin surface admitted before cutoff }\tau_h,

$$

$$

R_h = \text{public randomness beacon for slot }h,

$$

$$

E_h = {tx ;|; \mathrm{Included}(tx, B_h) \wedge \mathrm{Eligible}(tx, root_{h-1})},

$$

$$

O_h = \mathrm{CanonicalOrder}(R_h, E_h),

$$

$$

root_h = \mathrm{Execute}(root_{h-1}, O_h).

$$

Core assumptions

The family-level safety claims rely on the following explicit assumptions:

• Objective publication: admitted bulletin entries, transcripts, and challenges have stable hashes and objective inclusion paths.
• Verifiable bulletin availability: the protocol exports a bulletin-availability object, compact publication-frontier metadata that binds the same slot surface, and a canonical bulletin-close object for each closed ordering slot; the remaining assumption is that the underlying publication substrate satisfies the retrieval semantics claimed by those objects. The live runtime also requires successful closed-slot extraction before positive canonical-order admission.
• Compact frontier consistency: any carried PublicationFrontier must bind the same-slot bulletin commitment, ordered surface, and compact availability receipt, and same-slot conflicts or stale predecessor links must admit short objective contradiction objects. These frontier objects summarize the slot surface; they do not reconstruct it.
• Objective validity only: theorem-critical rejection or acceptance does not depend on private local facts.
• Public derivability over universal receipt: honest validators that observe the same closed public boundary derive the same close-or-abort result; universal timely receipt is not required.
• Independent publication path: suppressing negative evidence requires capture of both the validator plane and the publication / registry surface.
• Sealed-effect gating: irreversible effects are released only after surviving the canonical close-or-abort surface.
• Fixed epoch identities: the validator set is epoch-scoped and stable while the accountable rules of that epoch are enforced.

Here and throughout, "ordinary permissioned setting" means fixed authenticated authorities, deterministic local verification, public hash-addressed protocol objects, epoch-scoped identity state, and eventual- fair delivery and persistence of admissible protocol artifacts, with no trusted relay, privileged coordinator, TEE, theorem-side bootstrap oracle, or hidden external recovery service. Fixed authenticated membership is part of the theorem statement, not a missing crutch. The hidden-helper exclusions are relay, coordinator, TEE, bootstrap oracle, and external recovery service - not epoch-scoped authenticated identity itself.

Evidence objects

The family-level evidence objects are:

• validator quorum certificates over block proposals,
• guardian quorum certificates over slot decisions,
• witness certificates over guardianized slots,
• canonical-order certificates over bulletin surfaces,
• omission proofs over ordered-set incompleteness,
• observer transcripts, observer challenges, and canonical close-or-abort objects over sealed finality,
• sealed-effect proof objects with replay-safe nullifiers.

All honest nodes are required to derive the same acceptance result from the same admissible evidence set.

Accountable publication rules

Objective AFT faults are not merely audit artifacts. In the runtime they are first-class accountable protocol objects:

• OmissionProof names the validator accountable for the dominated positive order object.
• AsymptoteObserverChallenge determines accountability by kind: MissingTranscript and ConflictingTranscript blame the assigned observer; TranscriptMismatch, VetoTranscriptPresent, and InvalidCanonicalClose blame the producer / positive-close path.
• Valid objective fault evidence is replay-deduplicated on chain.
• Policy-controlled membership updates are aftermath only: the same evidence may trigger best-effort immediate quarantine and stage next-epoch eviction, but the decisive negative object remains valid even when those membership updates are disabled, delayed, or skipped.

These rules do not change the hot path. They strengthen the adversary model: arbitrary behavior is tolerated only insofar as it remains publicly revealable and penalty-bearing.

Public State Continuity with Extractable Obstructions

AFT's deeper theorem target is not a new round gadget. It is a new source of uniqueness. Classical Byzantine agreement derives uniqueness from overlap of dense positive quorums. AFT instead seeks a rigidity theorem over public slot objects: once the slot boundary is closed, the space of admissible public continuations should collapse to one canonical object or one canonical abort.

Boundary-conditioned execution language

For a closed slot boundary define

$$

\partial_h := (root_{h-1}, \beta_h, \tau_h, R_h, p_h),

$$

where $\beta_h$ is the canonical bulletin-close object binding the bulletin commitment, bulletin-availability certificate, and canonical cutoff whose recoverable surface is $B_h$; $\tau_h$ is the canonical cutoff object; $R_h$ is the slot randomness beacon; and $p_h$ is the policy descriptor governing admissible checks for slot $h$.

Let a public execution object for slot $h$ be a normalized public codeword

$$

X_h := (B_h, E_h, O_h, root_h, \sigma_h),

$$

where $E_h$ is the eligible subset, $O_h$ is the canonical ordered object, $root_h$ is the resulting state commitment, and $\sigma_h$ is the slot-local sealing surface needed to determine whether the slot closes or aborts. The important point is that $X_h$ is not a distributed transcript. It is the public quotient of the slot after irrelevant schedule variation is factored out.

Define the boundary-conditioned language

$$

\mathcal{L}(\partial_h) := {X ;|; \exists \pi ; \mathrm{Accept}(\partial_h, X, \pi)=1 }.

$$

Here $\pi$ is a succinct admissibility witness. For canonical ordering, $\pi$ is the proof-carrying order certificate witness. For deterministic observer sealing, $\pi$ is the witness that the canonical transcript surface, challenge surface, and close-or-abort object satisfy the slot policy.

Obstruction extractability

The companion rejection relation is

$$

\mathrm{Reject}(\partial_h, Y, \omega)=1,

$$

where $Y$ is a fully specified candidate public execution object and $\omega$ is a short public objective contradiction witness.

AFT seeks obstruction-complete local testability: for a fixed closed boundary, every fully specified candidate lies in exactly one of two states,

$$

\Big(\exists \pi ; \mathrm{Accept}(\partial_h, Y, \pi)=1\Big) ;\oplus; \Big(\exists \omega ; \mathrm{Reject}(\partial_h, Y, \omega)=1\Big).

$$

This xor formulation is the software-only analogue of state continuity. It is stronger than merely having a valid proof system. It says every non-admissible candidate exposes a short public contradiction witness.

In the live repository, the obstruction basis is not abstract:

• ordering uses a first-class canonical abort taxonomy over the canonical bulletin surface: missing certificates, bulletin-surface reconstruction failures, bulletin-surface mismatches, invalid bulletin-close formation, omission-dominated candidates, certificate-height mismatches, randomness mismatches, ordered-transactions-root mismatches, resulting-state-root mismatches, invalid public-input bindings, invalid bulletin-availability bindings, and invalid proof bindings,
• deterministic observer sealing uses objective challenge kinds over the canonical transcript and challenge surface,
• the accountable-adversary layer turns those same objects into penalty-bearing public fault evidence.

Unique collapse object

The slot should not merely admit at most one positive object. It should admit at most one collapse object:

$$

\mathrm{Collapse}(\partial_h) \in {\mathrm{Close}(X_h), \mathrm{Abort}(\Omega_h)}.

$$

Here $\mathrm{Close}(X_h)$ denotes the unique admissible positive object when the obstruction surface is empty, while $\mathrm{Abort}(\Omega_h)$ denotes the unique negative object induced by a non-empty valid obstruction surface. Negative evidence does not create a second truth. It forces the slot to land on its canonical abort object instead of a close object.

In the runtime this collapse object is not merely an abstract proof target. Validator finalization publishes a first-class CanonicalCollapseObject through guardian_registry, and later consensus verification cross-checks any published copy against the same proof-carried ordering and sealing surface when parent-state data is available. In the current recursive-continuity slice, CanonicalCollapseObject also carries a rolling previous_canonical_collapse_commitment_hash, and in the current clean-break runtime slice it also carries continuity_accumulator_hash together with continuity_recursive_proof, so the current slot's collapse object is linked to the previously persisted or published collapse object rather than standing as an isolated per-slot fact. The newest proposal-surface slice pushes that same predecessor link into the signed header itself: BlockHeader now carries previous_canonical_collapse_commitment_hash in its signed preimage and also carries a typed CanonicalCollapseExtensionCertificate. That certificate now carries the predecessor commitment plus the predecessor recursive-proof hash, while the public predecessor CanonicalCollapseObject now carries only a single recursive proof step rather than a carried predecessor-proof tree. Each recursive proof step still binds a predecessor collapse commitment, predecessor commitment hash, predecessor payload hash, and previous proof hash; the rolling continuity_accumulator_hash remains in place as the companion accumulator over the same chain. The implementation surface distinguishes the reference HashPcdV1 carrier from a backend slot SuccinctSp1V1, and the runtime exposes a dedicated continuity-verifier seam for those recursive public inputs via ioi-api and zk-driver-succinct. That seam is now wired into the live protocol: GuardianMajority invokes it while validating proposal and QC continuity for carried or anchored SuccinctSp1V1 proof steps, and validator durable-state checks invoke the same backend before a persisted CanonicalCollapseObject is treated as authoritative. Proposal verification checks that the carried predecessor commitment hash matches the signed predecessor link, checks that the predecessor commitment's resulting state root matches the signed parent-state root, and checks that the carried predecessor proof hash matches the anchored predecessor collapse object already persisted or published in protocol state. Leaders in Asymptote stall rather than propose when the required extension certificate or anchored predecessor collapse object is unavailable, proposal verification rechecks that implied predecessor commitment against both the signed predecessor commitment link and the parent-state root, checks the carried predecessor proof hash against the anchored predecessor proof on the public collapse object, and QC progression only treats continuity-linked headers as progress-authoritative.

Theorem: Public State Continuity with Extractable Obstructions.

Assume a closed boundary $\partial_h$, objective publication, a protocol-native retrievability plane, compact publication-frontier consistency, objective validity only, and proof soundness. Then the instantiated and normative theorem shape for AFT is:

1. $\mathcal{L}(\partial_h)$ contains at most one admissible public execution object,
2. every fully specified candidate $Y \notin \mathcal{L}(\partial_h)$ admits a short public objective obstruction witness $\omega$ such that $\mathrm{Reject}(\partial_h, Y, \omega)=1$,
3. therefore the slot admits at most one admissible collapse object, either the unique close object or the unique abort object.

This theorem is the precise form of the software-only continuity primitive that the instantiated AFT runtime realizes. The later ordering, collapse, recovery, restart, and sealed-effect sections are concrete theorem instances and composition layers of this same continuity statement, not separate aspirations. It does not claim that the classical DLS / PBFT frontier disappeared inside the standard dense-vote model. The point is different: the uniqueness source has moved from quorum overlap into the public-evidence language itself. In the instantiated runtime, compact publication frontiers internalize same-slot and predecessor consistency inside the live protocol, while the protocol-native retrievability plane discharges closed-bulletin extraction-or-abort on the cold path.

Lemma program

The clean proof path is a filtration rather than a single opaque argument:

$$

\mathcal{L}_0(\partial_h) \supseteq \mathcal{L}_1(\partial_h) \supseteq \cdots \supseteq \mathcal{L}_k(\partial_h),

$$

where each refinement adds one structural constraint and each failed refinement admits a short witness.

The repository's theorem program is:

1. Boundary Fixing Lemma. The closed boundary fixes the admissible publication domain.
2. Bulletin Close Lemma. The canonical bulletin-close object fixes the unique recoverable bulletin surface for the slot.
3. Eligibility Determinism Lemma. The predecessor commitment and boundary fix the eligible subset.
4. Order Determinism Lemma. The boundary and eligible subset fix the canonical ordered object.
5. Transition Determinism Lemma. The ordered object fixes the next state commitment.
6. Collapse Exclusivity Lemma. A slot cannot admit both a canonical close object and a canonical abort object.
7. Obstruction Soundness Lemma. Every valid omission proof or observer challenge objectively rejects its target candidate.
8. Obstruction Completeness Lemma. Every invalid fully specified candidate contains at least one minimal public obstruction witness.
9. Extractor Sufficiency Lemma. Given the canonical bulletin-close object, any honest validator can run the protocol-defined bulletin extractor to reconstruct the same bulletin surface; in this instantiation, admission of the positive ordering object already requires this extraction to succeed over the published closed-slot surface. One honest validator remains sufficient to surface the resulting positive or negative object under the instantiated runtime model.

One honest validator is surfacing-sufficient but never trust-bearing: correctness does not attach to the revealer's identity, because any honest validator observing the same closed boundary derives the same decisive object.

The theorem surfaces of this paper are instances of that program:

• CanonicalOrdering instantiates unique admissibility and extractable obstruction through proof-carrying order certificates plus omission dominance.
• Asymptote instantiates unique collapse through canonical transcript/challenge surfaces plus close-or-abort exclusivity.

The AFT Deterministic Base Engine

AFT modes share a deterministic core engine for proposal flow, QC formation, locking, and view progression.

Deterministic leadership and view progression

For a given height and view, the implementation selects the proposer by deterministic round-robin over the active validator set:

$$

\mathrm{leader}(h, v) = V_h[(h - 1 + v) \bmod |V_h|].

$$

Here $V_h$ is the active validator set for height $h$ after operational quarantine filters are applied.

View $0$ proposals do not carry a timeout certificate. Any non-zero view proposal must carry a valid timeout certificate for the previous unsuccessful view. The pacemaker advances views monotonically and resets timers on observed progress.

Validator quorum certificates

In GuardianMajority, Asymptote, and NestedGuardian, validator quorum is a strict simple majority of active validator weight, not a classical $2/3 + 1$ quorum:

$$

\mathrm{QCQuorum}(V_h) > \frac{1}{2}\mathrm{Weight}(V_h).

$$

This is safe only because the validator quorum is not the sole authority object. A proposal must also satisfy guardian-layer admissibility.

Timeout certificates use the same simple-majority rule over view-change votes.

Locking, 2-chain commit, and divergence guard

Validators maintain a lock on the highest safe parent QC they have observed. A validator votes only when the proposal extends the lock or is in a strictly higher view than the lock.

Base commitment uses a 2-chain rule:

• let $QC_{parent}$ certify parent block $P$,
• let $QC_{child}$ certify child block $C$,
• if $C$ directly extends $P$ and the views are consecutive, then $P$ becomes a pending commit.

The implementation delays final durability by a guard window $\Delta_{guard}$ before a pending commit is released. The purpose of the guard window is operational, not purely algebraic: it gives divergence evidence or panic signals time to propagate before a conflicting branch is treated as durable.

This produces a fail-closed operational behavior:

• sparse chain progress happens on the hot path,
• conflicting evidence is surfaced before irreversible consequences,
• divergence proofs quarantine the affected node rather than silently allowing fork continuation.

GuardianMajority: Production Base Finality

GuardianMajority is the production fault model for AFT base finality. Validator votes alone never make a proposal admissible. Every valid proposal must also carry a guardian committee certificate that verifies against current registered committee state.

Guardian certificate object

The guardian certificate binds:

• the guardian committee manifest hash,
• the active epoch,
• the canonical decision hash for the slot payload,
• a monotonic guardian counter,
• a guardian trace root,
• a measurement root,
• the signer bitfield,
• the aggregated BLS signature,
• a transparency-log checkpoint,
• and, in NestedGuardian, an optional experimental witness certificate.

The guardian decision payload is slot-scoped. Honest guardians are assumed not to sign two different decisions for the same slot.

Verification rule

A guardianized proposal is admissible only if all of the following hold:

1. the referenced guardian committee manifest is registered on-chain for the active epoch,
2. the certificate manifest hash matches the registered manifest,
3. the certificate epoch matches the manifest epoch and current epoch,
4. the decision hash matches the slot's canonical guardian decision payload,
5. the measurement root matches the decision payload,
6. the signer set is valid, unique, and meets the committee threshold,
7. the aggregated signature verifies against the manifest public keys,
8. the attached transparency-log checkpoint verifies against the anchored log descriptor and append-only proof.

The transparency log is an accountability layer. It does not replace threshold safety. It makes issued decisions, checkpoints, and later slashing evidence publicly checkable.

Committee threshold model

Let a guardian committee have threshold $t$ and size $n$. Conflicting slot certificates require enough equivocators to cover the minimum quorum intersection:

$$

f < 2t - n.

$$

Production committees therefore use strict majority thresholds:

$$

t = \left\lfloor \frac{n}{2} \right\rfloor + 1.

$$

This guarantees pairwise quorum intersection. It also exposes an important operational nuance:

• odd-sized simple-majority committees tolerate zero equivocating guardian members at the committee layer,
• even-sized majority committees tolerate one equivocator before threshold intersection is exhausted.

Production safety therefore relies on both threshold intersection and stronger guardian non-equivocation guarantees.

Safety statement

Proposition: GuardianMajority Safety.

No two conflicting blocks can both finalize for the same $(height, view)$ if guardian committee manifests are current, committee thresholds are majority thresholds, honest guardians do not equivocate for the same slot, transparency-log checkpoints and registry state are current enough to verify admissibility, and validators finalize only guardian-admissible blocks.

This is not a classical $3f + 1$ theorem. It is a composed threshold theorem over validators, guardians, registry state, and shared evidence. That statement is local to the guardian-backed base-finality layer. It does not delimit the paper's promoted theorem surface. The promoted durable-agreement claim is carried by the later proof-carrying close-or-abort and canonical- collapse architecture, which is precisely why the classical $3f + 1$ threshold is not load-bearing there.

Liveness model

Liveness is secondary to safety. Progress requires:

• enough active validators to form the simple-majority validator QC,
• enough guardian members to satisfy the committee threshold,
• current registry state for the epoch,
• current enough checkpoint and log availability.

If these degrade, the protocol prefers stalling over accepting unsafe evidence.

Canonical Ordering

CanonicalOrdering is the proof-carrying ordering path that gives AFT its 99% equal-authority ordering consensus claim.

Objective

For each slot $h$, define a unique canonical ordered set $O_h$ and a certificate $OCert_h$ such that:

• every honest verifier can check $OCert_h$ cheaply,
• any omission is objectively provable,
• the ordered set is recoverable from public data,
• the live hot path carries a compact publication frontier that binds the same-slot bulletin / ordering / availability surface and predecessor continuity,
• conflicting valid certificates for the same slot are impossible,
• arbitrary behavior by almost all validators cannot create a conflicting valid ordering outcome because the closed bulletin boundary admits one deterministically derivable close-or-abort result.

Canonical objects

For slot $h$,

$$

B_h = \text{bulletin surface admitted before }\tau_h,

$$

$$

R_h = \text{public randomness beacon for slot }h,

$$

$$

E_h = {tx ;|; \mathrm{Included}(tx, B_h) \wedge \mathrm{Eligible}(tx, root_{h-1})},

$$

$$

O_h = \mathrm{CanonicalOrder}(R_h, E_h),

$$

$$

root_h = \mathrm{Execute}(root_{h-1}, O_h).

$$

The abstract certificate is

$$

OCert_h = \left( h, root_{h-1}, cutoff_h, bulletin_commitment_h, ordered_commitment_h, root_h, witness_h \right).

$$

Bulletin, cutoff, and admissibility assumptions

The ordering theorem is conditional on the following named assumptions.

A1. Objective publication.

Each admitted transaction or batch in $B_h$ has a stable content hash, a verifiable inclusion path into the bulletin commitment, and an objective publication time or publication position relative to the slot cutoff.

A2. Endogenous retrievability.

The bulletin contents committed by $bulletin_commitment_h$ are reconstructed or deterministically aborted from protocol-native retrievability objects rooted in the canonical bulletin close for slot $h$. Compact publication-frontier summaries and availability certificates bind that claim on the hot path, while retrievability profiles, shard manifests, custody assignments, custody receipts, custody responses, and objective challenge objects close the extraction-or-abort loop on the cold path. Without that plane, uniqueness may still hold while timely materialization of the same close-or-abort surface can fail.

A3. Append-only or equivocation-evident commitment.

The bulletin commitment and any carried publication frontier for slot $h$ must be append-only or otherwise make same-slot equivocation or stale predecessor linkage objectively detectable at the slot boundary.

A4. Eligibility determinism.

$\mathrm{Eligible}(tx, root_{h-1})$ is deterministic and locally checkable from the committed predecessor root and the transaction object. Honest validators therefore derive the same eligible set $E_h$ from the same public inputs.

A5. Proof soundness.

$\mathrm{VerifyProof}(witness_h) = \mathrm{true}$ implies that the witness obligations for cutoff binding, bulletin binding, ordering, state transition, retrievability commitments, and omission commitments actually hold.

The cutoff $\tau_h$ is not a private local clock read. It is a protocol-bound object. In the instantiated runtime, the cutoff is bound directly into the published bulletin commitment and into the canonical public-input set. Eligibility is deterministic with respect to the predecessor state root and the transaction object. This prevents local reinterpretation of the eligible set.

Current runtime instantiation

The runtime surfaces the abstract objects above as the following concrete objects:

Runtime object	Current fields
BulletinCommitment	(height, cutoff_timestamp_ms, bulletin_root, entry_count)
BulletinSurfaceEntry	(height, tx_hash)
BulletinAvailability / Certificate	(height, bulletin_commitment_hash, recoverability_root)
BulletinRetrievabilityProfile	(height, bulletin_commitment_hash, / bulletin_availability_certificate_hash, recoverability_root, / shard_count, recovery_threshold, custody_threshold)
BulletinShardManifest	(height, bulletin_commitment_hash, / bulletin_availability_certificate_hash, / bulletin_retrievability_profile_hash, recoverability_root, / entry_count, shard_count, recovery_threshold, shard_commitment_root)
BulletinCustodyAssignment	(height, bulletin_retrievability_profile_hash, / bulletin_shard_manifest_hash, validator_set_commitment_hash, / assignments)
BulletinCustodyReceipt	(height, bulletin_commitment_hash, / bulletin_availability_certificate_hash, / bulletin_retrievability_profile_hash, bulletin_shard_manifest_hash, / custodian_count, custody_threshold, custody_root)
BulletinCustodyResponse	(height, bulletin_commitment_hash, / bulletin_availability_certificate_hash, / bulletin_retrievability_profile_hash, bulletin_shard_manifest_hash, / bulletin_custody_assignment_hash, bulletin_custody_receipt_hash, / served_shards)
BulletinRetrievabilityChallenge	(height, kind, bulletin_commitment_hash, / bulletin_availability_certificate_hash, / bulletin_retrievability_profile_hash, bulletin_shard_manifest_hash, / bulletin_custody_assignment_hash, bulletin_custody_receipt_hash, / bulletin_custody_response_hash, details)
BulletinReconstructionCertificate	(height, bulletin_commitment_hash, / bulletin_availability_certificate_hash, / bulletin_retrievability_profile_hash, bulletin_shard_manifest_hash, / bulletin_custody_assignment_hash, bulletin_custody_receipt_hash, / bulletin_custody_response_hash, canonical_bulletin_close_hash, / canonical_order_certificate_hash, reconstructed_entry_count, / reconstructed_bulletin_root)
BulletinReconstructionAbort	(height, kind, bulletin_commitment_hash, / bulletin_availability_certificate_hash, / bulletin_retrievability_profile_hash, bulletin_shard_manifest_hash, / bulletin_custody_receipt_hash, bulletin_retrievability_challenge_hash, / canonical_order_abort_hash, details)
PublicationAvailabilityReceipt	(height, bulletin_commitment_hash, / ordered_transactions_root_hash, resulting_state_root_hash, / receipt_root)
PublicationFrontier	(height, view, counter, parent_frontier_hash, / bulletin_commitment_hash, ordered_transactions_root_hash, / availability_receipt_hash)
PublicationFrontierContradiction	(height, kind, candidate_frontier, reference_frontier)
CanonicalBulletin / Close	(height, cutoff_timestamp_ms, bulletin_commitment_hash, / bulletin_availability_certificate_hash, / bulletin_retrievability_profile_hash, bulletin_shard_manifest_hash, / bulletin_custody_receipt_hash, entry_count)
CanonicalOrder / PublicInputs	(height, parent_state_root_hash, bulletin_commitment_hash, / randomness_beacon, ordered_transactions_root_hash, / resulting_state_root_hash, cutoff_timestamp_ms)
CanonicalOrderProofSystem	concrete variants HashBindingV1 and CommittedSurfaceV1
CommittedSurface / CanonicalOrderProof	(recoverability_root, omission_commitment_root)
CanonicalOrder / Certificate	(height, bulletin_commitment, bulletin_availability_certificate, / randomness_beacon, ordered_transactions_root_hash, / resulting_state_root_hash, proof, omission_proofs)
CanonicalOrder / PublicationBundle	(bulletin_commitment, bulletin_entries, bulletin_availability_certificate, / bulletin_retrievability_profile, bulletin_shard_manifest, / bulletin_custody_receipt, canonical_order_certificate)
CanonicalOrder / Abort	(height, reason, details, bulletin_commitment_hash, / bulletin_availability_certificate_hash, bulletin_close_hash, / canonical_order_certificate_hash)

HashBindingV1 is the reference verifier family: its proof bytes are a canonical hash binding over the public-input hash. CommittedSurfaceV1 is the live proof family: its proof payload contains the recoverability root and the omission-commitment root for the committed surface. In the current runtime, positive ordering artifacts are published through the atomic CanonicalOrderPublicationBundle, carrying the bound retrievability profile / manifest / custody-receipt objects, while the registry deterministically materializes the coupled custody-assignment and custody-response objects over the same slot surface before admitting the positive lane. Positive committed blocks also carry a compact signed PublicationFrontier: it binds the same-slot bulletin commitment, ordered-transactions root, and compact publication-availability receipt, and it hash-links that summary to the previous slot's frontier. Short PublicationFrontierContradiction objects make same-slot conflict or stale predecessor linkage objectively rejectable on the hot path. Those frontier objects internalize compact publication consistency, but they do not replace the protocol-native retrievability plane that reconstructs or aborts the full bulletin surface. Validators also run a block-local derivation pass over the committed block boundary: they derive either a CanonicalOrderExecutionObject or a CanonicalOrderAbort, and publish the abort artifact when the proof-carried positive object cannot be derived. When the endogenous retrievability lane succeeds, the registry materializes a first-class BulletinReconstructionCertificate bound to the canonical close, canonical-order certificate, and the same retrievability objects. When endogenous retrievability evidence dominates that same surface, the registry also materializes a specialized BulletinReconstructionAbort object bound to the challenge and the paired CanonicalOrderAbort, so reconstruction-impossible failure is named as a first-class protocol object rather than only as a generic ordering abort.

Acceptance rule

Every validator applies the same deterministic rule:

$$

\begin{aligned} \mathrm{Accept}(OCert_h) \iff;& \mathrm{VerifyProof}(witness_h) \ &\wedge \mathrm{VerifyCutoff}(cutoff_h) \ &\wedge \mathrm{PredecessorAccepted}(root_{h-1}) \ &\wedge \neg \exists tx : \mathrm{ValidOmission}(h, tx). \end{aligned}

$$

In the implementation this specializes to:

• the certificate height and bulletin height must match the block height,
• the randomness beacon must match the slot schedule,
• the bulletin commitment must match the published bulletin when that bulletin is available from anchored state,
• any carried PublicationFrontier must match the same-slot bulletin commitment, ordered-transactions root, and publication-availability receipt hash,
• when a predecessor frontier exists, the carried PublicationFrontier must extend it by counter and parent hash,
• no published PublicationFrontierContradiction may already dominate the slot,
• positive canonical-order admission in the runtime additionally requires successful closed-slot extraction over the published bulletin entries, the carried bulletin-availability certificate, and the canonical bulletin-close object,
• the ordered-transactions root and resulting state root must match the block header,
• the proof must match the canonical public inputs,
• the recoverability root must match the certificate commitments,
• the omission-commitment root must match the omission-proof set.

If the omission-proof set is non-empty, the candidate certificate is rejected immediately.

No dense positive vote on the order is required once a valid $OCert_h$ is surfaced. The current verifier entry point for this rule is verify_canonical_order_certificate.

Omission dominance

An omission is objective when a transaction:

• was included in $B_h$ before $\tau_h$,
• was eligible under $root_{h-1}$,
• and is absent from the committed ordered set $O_h$.

Define the omission proof

$$

\Omega(h, tx) = \left( \begin{array}{l} inclusion_proof(tx, bulletin_h), \ cutoff_admissibility_proof(tx, cutoff_h), \ eligibility_proof(tx, root_{h-1}), \ nonmembership_proof(tx, O_h) \end{array} \right).

$$

Its semantics are:

$$

\mathrm{Valid}(\Omega(h, tx)) \Rightarrow \mathrm{Reject}(OCert_h).

$$

This is the central AFT ordering move. A candidate does not need to win a dense round of positive endorsements if any incomplete view can be killed objectively.

Omission dominance is a correctness rule, not a punishment rule. A valid omission proof kills the candidate immediately whether or not slashing, quarantine, or next-epoch removal ever fires.

Uniqueness, publication frontiers, and recoverability

Theorem: Uniqueness.

If $\mathrm{ValidOrderCert}(h, C_1)$ and $\mathrm{ValidOrderCert}(h, C_2)$, then $C_1$ and $C_2$ commit the same canonical ordered set $O_h$.

The reason is structural:

• the predecessor root is fixed,
• the cutoff object is canonical,
• the bulletin commitment is canonical,
• eligibility is deterministic,
• the ordering function is deterministic,
• proof soundness forbids a witness for a different ordered set.

The live publication-frontier slice sits between uniqueness and recoverability. A frontier gives a compact signed summary of the claimed bulletin / ordering surface and its predecessor link, so same-slot conflict or stale lineage is objectively rejectable without reconstructing the full bulletin on the hot path. But the frontier only binds hashes and receipt roots; it is not itself the recoverable bulletin surface.

Theorem: Endogenous Retrievability.

If $\mathrm{ValidOrderCert}(h, C)$ and the canonical bulletin close plus protocol-native retrievability plane for slot $h$ are present and unchallenged, then every honest verifier can reconstruct the same ordered set $O_h$ from protocol objects alone: the canonical close, bound frontier / availability commitments, retrievability profile, shard manifest, custody receipt, positive reconstruction certificate, and published bulletin entries.

Endogenous retrievability matters because the accepted order is not merely unique. The compact frontier tells validators which surface is being claimed; the retrievability plane tells them that the full surface can actually be reconstructed or objectively aborted from protocol evidence.

The hot path and the cold path do not carry different truths. The frontier binds the claimed surface compactly; the retrievability plane reconstructs or objectively aborts that same surface; both terminate on the same canonical close-or-abort object.

99% equal-authority ordering consensus

AFT's ordering claim is a proof-carrying consensus theorem whose decisive object is revealed rather than manufactured by dense positive yes-votes. Revelation is not a weaker post hoc reporting layer here; it is the equal- authority surfacing mechanism for the uniquely valid public execution object already fixed by the closed public boundary.

Theorem: 99% Equal-Authority Ordering Consensus.

Assume:

1. the closed bulletin surface $B_h$ bound by the carried publication frontier and bulletin commitment is governed by a canonical bulletin close and protocol-native retrievability plane that deterministically yields extraction or abort,
2. the cutoff object for slot $h$ is canonical,
3. bulletin commitments, compact publication-frontier bindings, and omission proofs are objectively verifiable,
4. same-slot frontier conflicts and stale predecessor links admit short objective contradiction objects,
5. the proof system is sound.

Then even if $99%$ of validators behave arbitrarily, they cannot create a conflicting valid canonical-order outcome for slot $h$. More strongly, every honest validator that observes the same closed ordering boundary derives the same positive order object or omission-dominated abort.

Compact publication frontiers therefore internalize cheap same-slot and predecessor consistency checks on the live path, while recoverability remains the stronger assumption needed to turn that compact claim into a publicly reconstructable ordered set.

[[aft-figure:omission-dominance]]

The strongest shorthand is:

$$

99% \text{ of validators may behave arbitrarily,}

$$

$$

\text{because the closed ordering boundary admits one deterministically}

$$

$$

\text{derivable close-or-abort outcome.}

$$

This is equal-authority because any validator may reveal the winning certificate. It is 99%-fault tolerant because correctness does not depend on a dense majority of positive votes. This section isolates the ordering lane, not the theorem ceiling. Once composed with endogenous retrievability, canonical collapse, recovery and restart continuity, and collapse-bound sealed-effect gating, the promoted AFT theorem surface is exactly the paper's unconditional classical 99% Byzantine agreement claim in the ordinary permissioned setting.

With the accountable publication rules of Section System Model and Notation, invalid positive ordering attempts are not only rejectable; they are also penalty-bearing and next-epoch removing.

Asymptote: Sealed Finality and Irreversible Effects

Asymptote is the two-tier settlement mode in the AFT family. It preserves fast BaseFinal chain progression while requiring stronger evidence before irreversible effects are released.

Finality tiers and collapse states

The finality tiers are:

• BaseFinal: validator QC plus guardian certificate.
• SealedFinal: BaseFinal plus sufficient sealing evidence.

The slot collapse states are:

• Pending
• BaseFinal
• Sealing
• Abort
• SealedFinal
• Escalated
• Invalid

All honest nodes must derive the same collapse state from the same admissible evidence set.

[[aft-figure:collapse-surface]]

SealedFinalityProof

The sealing plane gathers a proof object that binds:

• the epoch,
• the achieved finality tier,
• the collapse state,
• the guardian manifest hash,
• the guardian decision hash,
• the guardian counter,
• the guardian trace root,
• the guardian measurement root,
• the policy hash,
• witness certificates, when the witness path is used,
• observer transcripts, transcript commitment, observer challenges, challenge commitment, and exactly one canonical observer outcome object when the observer path is used,
• divergence signals gathered during sealing.

This object is block-scoped and guardian-bound. A SealedFinalityProof that is not bound to the slot's guardian evidence is invalid.

Witness-backed sealing

The witness path assigns one witness committee per required certification stratum.

Witness assignment is deterministic over:

• the epoch seed,
• the producer account id,
• the slot $(height, view)$,
• the reassignment depth,
• the witness stratum id,
• the witness manifest hash.

Sealed finality is reached on the witness path when:

• BaseFinal holds,
• each required witness stratum contributes a valid assigned witness certificate,
• each witness certificate verifies against the registered witness manifest,
• required checkpoints and append-only proofs are current enough under policy.

Witness omission, stale registry participation, checkpoint inconsistency, or conflicting witness certificates produce explicit evidence rather than silent best-effort behavior.

Equal-authority observer sealing

The normative observer path is CanonicalChallengeV1. It treats sampled validators as deterministic duty assignees whose outputs must become public, recoverable protocol objects.

Observer assignment is deterministic over:

• the epoch seed,
• the producer account id,
• the slot $(height, view)$,
• the observation round,
• the observer account id.

The producer is excluded from its own observer pool. The runtime may also filter assignments through a correlation budget over provider, region, host class, and key-authority class.

Each assigned observer publishes one of two things:

• a guardian-backed AsymptoteObserverTranscript, or
• an objective AsymptoteObserverChallenge.

A transcript binds the canonical slot surface:

• the epoch and assignment,
• the candidate block hash,
• the guardian manifest, decision hash, counter, trace hash, and measurement root,
• the guardian checkpoint root,
• the observer verdict and veto kind,
• the observer evidence hash.

The admissible challenge basis is public-evidence-only:

• MissingTranscript,
• TranscriptMismatch,
• VetoTranscriptPresent,
• ConflictingTranscript,
• InvalidCanonicalClose.

Each challenge carries its own public evidence object: an assignment, an offending observation request, an offending transcript, or an offending canonical close. The challenge evidence_hash must bind exactly that carried evidence.

The slot then carries three canonical bindings:

• a transcript commitment over the transcript surface,
• a challenge commitment over the challenge surface,
• exactly one canonical outcome object: AsymptoteObserverCanonicalClose or AsymptoteObserverCanonicalAbort.

The collapse rule is close-or-abort and challenge-dominant:

• SealedFinal if BaseFinal holds, the deterministic assignment set is fully covered by valid canonical Ok transcripts, the transcript and challenge commitments verify, the challenge surface is empty, and the canonical close object is valid.
• Abort if the transcript and challenge commitments verify, the challenge surface is non-empty, and the canonical abort object is valid.
• Pending otherwise.

Challenge dominance is a theorem-level veto, not an operational alarm. A valid challenge collapses the slot to abort before any penalty, governance, or membership aftermath is considered.

This makes observer sealing structurally parallel to canonical ordering: public evidence, canonical commitments, a unique positive object, a unique negative object, and deterministic local close-or-abort derivation from the same public surface.

Divergence signals and escalation

The sealing plane may also emit divergence signals, including:

• conflicting guardian certificates,
• witness omission,
• stale registry use,
• stale checkpoints,
• transparency-log consistency failure.

These signals support Escalated and Invalid outcomes and give operators a fail-closed evidence trail.

Sealed effects and replay-safe release

Irreversible effects are gated by finality tier. The effect plane distinguishes between:

• BaseFinal effects, which are allowed on the fast path when policy permits,
• SealedFinal effects, which require a valid SealedFinalityProof.

For proof-enabled irreversible effects, Asymptote carries a self-contained SealObject whose current instantiation includes:

• an EffectIntent,
• an EffectPublicInputs object, including canonical_collapse_hash,
• an EffectProofEnvelope,
• a replay-safe nullifier.

In the runtime, SealedFinal secure-egress requests carry both the SealedFinalityProof and the slot's CanonicalCollapseObject. The guardian-side seal builder and downstream receipt verifier recompute the same canonical_collapse_hash from that collapse object together with the proof-carried observer surface, so a challenge-dominated or otherwise mismatched slot cannot authorize irreversible release.

The release rule is

$$

\mathrm{Release}(e) \iff \mathrm{BaseFinal}(\mathrm{slot}(e)) \wedge \mathrm{SealedFinal}(\mathrm{slot}(e)) \wedge \mathrm{VerifySealObject}(e) \wedge \mathrm{CollapseHash}(e)=\mathrm{Hash}(\mathrm{Collapse}(\partial_h)) \wedge \neg \mathrm{NullifierUsed}(e).

$$

This keeps the hot path sparse while making released consequences deterministic and replay-safe.

Deterministic observer theorem

The deterministic Asymptote observer model now proves the following kernel:

• base certificates are unique per slot,
• canonical observer close objects are unique per slot,
• canonical observer close and canonical observer abort cannot coexist for the same slot,
• a challenge-dominated slot cannot produce a valid sealed release.

Theorem: Deterministic Equal-Authority Observer Sealing.

Assume sound deterministic observer assignment, signature-sound guardian-backed observer transcripts and challenges, canonical transcript and challenge commitments, append-only registry and log publication once published, and deterministic transcript/challenge derivation over the closed public observer surface. Then arbitrary behavior by the rest of the validator set cannot create a conflicting valid canonical observer close, cannot make canonical close and canonical abort coexist for the same slot, and cannot authorize a valid sealed irreversible effect release for a challenge-dominated slot.

This theorem is the observer-lane analogue of canonical ordering's public certificate theorem: public evidence, canonical commitments, negative-authority dominance, and deterministic local close-or-abort derivation from the same public observer surface.

Under the accountable publication rules of Section System Model and Notation, the same observer challenges are also penalty-bearing objective faults. Unsafe positive close attempts therefore become not only rejectable, but accountable and epoch-removing.

Legacy sampled comparison

Before CanonicalChallengeV1, the observer lane was typically described through a sampled affirmative bound. Let:

• $h$ be the honest fraction of equal-authority validators,
• $A_s^j$ be the sampled observer committee for slot $s$ and round $j$,
• $k_j = |A_s^j|$,
• $p_{\mathrm{beacon_bias}}$ be the probability of sufficient beacon bias,
• $p_{\mathrm{veto_suppression}}$ be the probability that a valid veto surface is fully suppressed.

Then the old affirmative sampled lane admitted the analytical bound

$$

P_{\mathrm{unsafe}}(s) \le p_{\mathrm{beacon_bias}} \cdot p_{\mathrm{veto_suppression}} \cdot \prod_j (1 - h)^{k_j}.

$$

For constant committee size $k$ across $r$ rounds:

$$

P_{\mathrm{unsafe}}(s) \le p_{\mathrm{beacon_bias}} \cdot p_{\mathrm{veto_suppression}} \cdot (1 - h)^{kr}.

$$

That formula remains a useful historical comparison, but it is no longer the normative theorem for the observer lane. Under CanonicalChallengeV1, sampling determines duties, not safety. Safety comes from the canonical public transcript surface, the canonical public challenge surface, and the close-or-abort split that those surfaces induce.

The runtime publishes the canonical observer transcript, commitment, challenge, challenge commitment, and close-or-abort objects as ordinary guardian_registry transactions after the sealed header is formed. The same surface is carried inside the proof for immediate block verification.

NestedGuardian: Witness-Augmented Research Mode

NestedGuardian explores a layered threshold construction:

• validators run the AFT deterministic message flow,
• each proposal carries its guardian committee certificate,
• external witness committees cross-check the slot,
• chain state anchors witness assignments, witness manifests, and slashing evidence.

The instantiated runtime scope includes:

• deterministic witness assignment from the active witness set,
• registered on-chain witness manifests,
• witness certificates bound into guardianized slot certificates,
• safety proofs for the witness-augmented kernel,
• bounded model checking for reassignment, outage, and checkpoint transitions.

The instantiated proof package consists of:

• safety formalization,
• bounded operational model checking for reassignment, outage, and checkpoint transitions,
• a discharged composed-liveness bridge under the target eventual-fair scheduler through the recurrence/reduction/totality/collapse chain together with a matching persistent churn/restart simulator.

NestedGuardian is therefore a witness-augmented mode with a finished theorem bridge. It is experimental as an operational mode, not as a theorem crutch. Its witness-coded family supplies an explicit constructive recovery carrier and completed bridge artifacts; it does not reduce the promoted AFT theorem surface to an experimental-only claim. That constructive recovery carrier is a witness-coded publication-bundle recovery contract with compact hot-path bindings and cold-path registry-driven close-or-abort resolution. The abstract coded recovery-family contract is realized by the parametric SystematicXorKOfKPlus1V1 parity family plus the bounded true non-parity SystematicGf256KOfNV1 family with at least two parity shares, implemented with systematic Cauchy-style coefficients and exercised in bounded 2-of-4, 3-of-5, 3-of-7, 4-of-6, and 4-of-7 lanes. These lanes resolve from threshold-many public reveals, objective recovered-support conflict, or deterministic missingness. The bounded 3-of-5, 4-of-6, and 4-of-7 lanes restore or exceed threshold-support overlap while the bounded 3-of-7 lane shows that recovered-support conflict remains fail-closed even when overlap is absent. A bounded conformance harness checks that every threshold-sized reveal subset reconstructs and every below-threshold subset fails across the shipped XOR and GF256 realizations of that contract. Those recovered reveals lift deterministically into an explicit positive close-extraction payload and then into an explicit extractable bulletin-surface payload that binds the verifying publication bundle, verifying canonical bulletin close, canonical bulletin-availability bytes, and sorted bulletin entries.

The completed bounded family also carries the ordinary durable and restart surfaces. A bounded recovered-only two-slot harness shows that consecutive recovered surfaces derive the ordinary publication-frontier predecessor chain and the same authoritative CanonicalCollapseObject predecessor chain without the ordinary publication-bundle lane. A second bounded recovered-only harness shows a close/abort/close bulletin window with a recovered omission-dominated middle slot: recovered data alone materializes the ordinary positive closes and extracted bulletin surfaces on the outer slots, materializes the ordinary omission-dominated abort in the middle while keeping omission evidence and recovered bulletin entries public, and preserves the same authoritative collapse continuity chain. A bounded read-side harness shows that the same recovered-only durable chain yields the same compact replay-prefix / state-root continuity view that the ordinary lane exposes plus a bounded recovered canonical-header prefix. The execution module verifies that replay tip as the same restart anchor the ordinary lane uses, retains both recovered prefixes in execution state, and uses the recovered canonical-header ancestry for bounded anchored reads plus parent-block / parent-state-root continuity after restart when ordinary recent blocks are absent.

Validator consensus orchestration derives the same bounded recovered restart parent anchor from the recovered canonical-header / collapse surface when the ordinary committed block is absent, and the GuardianMajority engine consumes that bounded recovered canonical-header prefix as restart-time parent/QC context for synthetic parent-height QC continuity when the full committed block is absent. The same recovered surface yields a bounded recovered certified-header window plus a restart-only recovered BlockHeader / QC cache window for restart-time header / QC lookup plus bounded QC-certified recovered branch reconciliation over the configured local five-entry window. Those windows fold by exact overlap with a configurable budget, exercised at five windows into a longer seventeen-step recovered certified branch without ordinary committed headers. Those same cold-path loaders consume a configurable exact-overlap segment budget, exercised at four exact-overlap segments into a longer fifty-three-step recovered certified branch with direct registry-extraction parity and explicit interior-overlap conflict rejection. Those same restart loaders also compose two overlapping four-segment exact-overlap folds into a longer eighty-nine-step recovered certified branch with direct registry-extraction parity and explicit inter-fold overlap conflict rejection, and tests exercise the same recursive carrier at three overlapping four-segment folds into a one-hundred-twenty-five-step recovered certified branch. The runtime has a bounded conformance harness over one, two, and three stitched segment folds, matching the same production-loader / registry-extraction carrier at the corresponding fifty-three-step, eighty-nine-step, and one-hundred-twenty-five-step branches.

The restart path also pages older exact-overlap segment folds on demand beneath that bounded suffix via an overlap-checked cursor while keeping only the bounded recent suffix plus the streamed page live in engine caches, and tests exercise that paged carrier at a longer two-hundred-thirty-three-step recovered certified branch with direct registry-extraction parity plus explicit duplicate-page, missing-gap, and late-page overlap rejection. Restart therefore streams recovered certified ancestry until target height or recovered-history exhaustion without a theorem-relevant fixed depth bound.

The archival internalization layer uses an active archived-recovered-history profile naming retention horizon, exact-overlap paging geometry, segment / fold geometry, checkpoint update rule, and profile evolution. Archived segments, archived restart pages, archival checkpoints, and archival retention receipts bind to historically referenced profile hashes and governing activation hashes under a published profile-activation chain before archived continuation is trusted, and ordinary canonical collapse history names the archived checkpoint / activation pair that archived restart is authorized to follow. Archived replay and archived publication correctness are historical and index-free: they follow the canonical-collapse-anchored or object-carried activation hash plus predecessor/checkpoint history rather than whichever archived activation is merely latest in local state.

When the recovered certificate carries objective omission proofs, the same recovered lane routes into the ordinary OmissionDominated abort path while keeping omission evidence and recovered bulletin entries public. The recovery-family contract, canonical-collapse / replay retrievability anchor, and recovered-state historical retrievability surface are therefore part of ordinary endogenous AFT history rather than a narrower theorem-side qualifier. The directly discharged recurrence/reduction/totality/collapse chain closes the former distance to unconditional classical 99% Byzantine agreement, so no lower-bound, recoverability, or architecture-specific semantic gap remains at the theorem surface.

Security and Assumption Surface

The AFT family depends on explicit assumptions. They are not optional prose.

Layer	Required assumptions	Failure consequence
Base finality	current manifests, current epoch state, majority thresholds, guardian non-equivocation, valid checkpoints, enough validators and guardians to reach quorum	conflicting base-finality evidence or loss of progress
Canonical ordering	objective publication, compact publication-frontier binding and contradiction rules, canonical cutoff, deterministic eligibility, append-only bulletin commitment, proof soundness, protocol-native retrievability profile / manifest / custody / challenge surface, canonical bulletin-close extraction-or-abort, cheap omission verification, accountable omission publication	loss of compact frontier consistency, deterministic extraction-or-abort, accountability, or the ordering theorem
Sealed finality	valid asymptote policy, current witness seed, valid witness or observer assignments, checkpoint freshness, valid log consistency proofs, deterministic transcript/challenge derivation, accountable challenge publication	incorrect sealed release, loss of accountability, or fail-closed stalling
Sealed effects	correct finality-tier policy, sound verifier metadata, nullifier uniqueness, intent/public-input binding	replay or unsafe irreversible effect release
NestedGuardian	sound witness assignment and registration, correct reassignment handling, witness committee non-equivocation	degraded safety or open liveness behavior

The family-level discipline is simple: if an assumption fails, AFT should degrade to stalling, aborting, or withholding release before it degrades to unsafe irreversible behavior.

Formal Results

The repository's machine-checked surfaces align with the protocol family as follows:

Formal module	Core proved results
GuardianMajorityProof	QuorumCertificatesIntersect, InvariantImpliesSafety
GuardianMajority	executable bounded checks for finalization witness soundness and slot safety
CanonicalOrderingProof	InvariantImpliesCertifiedUniqueness, / InvariantImpliesRecoverability, / InvariantImpliesOmissionDominates
CanonicalOrdering	executable bounded checks for publication, cutoff, certification, omission, and recoverability
AsymptoteProof	InvariantImpliesBaseSafety, / InvariantImpliesCanonicalCloseSafety, / InvariantImpliesCloseAbortExclusive, / InvariantImpliesAbortDominatesSealed
Asymptote	executable bounded checks for transcript publication, challenge publication, canonical close, and canonical abort
NestedGuardianProof	witness-assignment soundness, / witness-certificates-stay-assigned, / InvariantImpliesSafety
NestedGuardian	executable bounded checks for reassignment, outage, and checkpoint admissibility

Every formal artifact named in this section, and every additional proof artifact cited by file name below, is embedded verbatim in Appendix Embedded Formal Artifacts so that the served yellow paper remains self-contained outside the repository.

These formal surfaces prove the deterministic safety kernels that the broader classical-agreement bridge builds on. The full ordinary classical 99% Byzantine agreement sentence is then completed by the recurring, reduction, totality, and collapse layers discussed above, rather than by these module-local safety kernels in isolation. Compact publication-frontier summaries internalize same-slot and predecessor consistency on the live path, while the protocol-native retrievability plane internalizes closed-bulletin extraction-or-abort as an endogenous part of the realizing architecture rather than a purely algebraic consequence of the authenticated message transcript alone.

The accountable-adversary variant therefore composes these formal kernels with runtime accountability rules rather than replacing them: replay-deduplicated objective fault publication and optional policy-controlled membership updates live in the implementation and policy layer above the proved deterministic core.

Complete omission-dominance witness artifact

The formal package includes an executable TLC witness module, docs/architecture/protocols/aft/formal/canonical_ordering/CanonicalOrderingOmissionTrace.tla, paired with docs/architecture/protocols/aft/formal/canonical_ordering/CanonicalOrderingOmissionTrace.cfg. The exact module and configuration are embedded in Appendix CanonicalOrderingOmissionTrace.tla and Appendix CanonicalOrderingOmissionTrace.cfg; the summary below highlights the executed public-evidence shape that the witness reaches.

Executed witness trace.

The module intentionally asks TLC to violate the state predicate NoOmissionDominanceWitness so that the checker emits a concrete public evidence trace. The executed trace is:

1. PublishStep: tx1 enters slot $1$'s bulletin surface.
2. PublishStep: tx2 enters the same bulletin surface.
3. CloseCutoffStep: the canonical cutoff closes and the recoverable set becomes ${tx1, tx2}$.
4. CandidateCertifyStep: a candidate certificate for ${tx1}$ appears.
5. ProveOmissionStep: an omission proof for $tx2$ against that candidate certificate appears.

The same formal package carries a bounded recursive-continuity model, docs/architecture/protocols/aft/formal/canonical_ordering/CanonicalCollapseRecursiveContinuity.tla, paired with docs/architecture/protocols/aft/formal/canonical_ordering/CanonicalCollapseRecursiveContinuity.cfg. The exact source of both artifacts is embedded in Appendix CanonicalCollapseRecursiveContinuity.tla and Appendix CanonicalCollapseRecursiveContinuity.cfg. That model captures the reference HashPcdV1 continuity carrier directly: deterministic recursive proof steps, predecessor-proof hashing, CanonicalCollapseExtensionCertificate carriage, and the rule that non-genesis header admission depends on the anchored predecessor proof relation. The runtime exposes a SuccinctSp1V1 backend seam for those same recursive public inputs, and that seam is exercised by consensus verification and durable-state gating. The formal model still stops at the reference carrier rather than mechanizing a cryptographic recursive accumulator or ZK backend.

At the final state, the incomplete candidate certificate remains unadmitted while the omission proof is present. In the executable model this happens because the admitted object must already equal the canonical set; the trace therefore does not replace the theorem. Its purpose is narrower and useful: it gives a bounded, executed witness of the exact public-evidence shape from which omission dominance follows. Readers can run the trace directly and inspect the six-state witness without reconstructing the paper's argument by hand.

Implementation Correspondence

This section is non-normative. It names the exact runtime symbols that carry the protocol objects defined above.

Core ordering symbols

The core ordering data structures and free functions are public Rust symbols re-exported through ioi_types::app. They are the runtime carriers for the abstract ordering objects and verifier rules defined above.

Abstract object	Current runtime symbols
Bulletin surface commitment	BulletinCommitment, BulletinSurfaceEntry
Compact publication availability binding	PublicationAvailabilityReceipt
Compact publication frontier	PublicationFrontier
Publication-frontier contradiction	PublicationFrontierContradiction
Canonical ordering proof families	CanonicalOrderProofSystem, with concrete variants HashBindingV1 and CommittedSurfaceV1
Canonical public-input tuple	CanonicalOrderPublicInputs
Live succinct witness payload	CommittedSurfaceCanonicalOrderProof
Omission evidence	OmissionProof
Order certificate	CanonicalOrderCertificate
Canonical ordering function	canonical_order_tx_hashes
Publication-frontier hashing	canonical_publication_availability / _receipt_hash, / canonical_publication_frontier_hash, / canonical_publication_frontier / _contradiction_hash
Publication-frontier construction / verification	build_publication_availability_receipt, / build_publication_frontier, / verify_publication_frontier, / verify_publication_frontier_contradiction
Public-input hashing	canonical_order_public_inputs, / canonical_order_public_inputs_hash
Reference proof construction	build_reference_canonical_order / _proof_bytes
Live certificate construction	build_committed_surface_canonical / _order_certificate
Certificate verification	verify_canonical_order_certificate

Guardian and sealing symbols

The guardian, witness, observer, and sealed-effect objects are likewise public Rust symbols re-exported through ioi_types::app. They encode the exact evidence surface checked by validators and downstream gateways.

Abstract object	Current runtime symbols
Guardian slot certificate	GuardianQuorumCertificate
Witness certificate	GuardianWitnessCertificate
Equal-authority observer assignment	AsymptoteObserverAssignment
Correlation budget	AsymptoteObserverCorrelationBudget
Observer observation request	AsymptoteObserverObservationRequest
Observer transcript	AsymptoteObserverTranscript
Observer transcript commitment	AsymptoteObserverTranscriptCommitment
Observer challenge	AsymptoteObserverChallenge, with kinds MissingTranscript, TranscriptMismatch, VetoTranscriptPresent, ConflictingTranscript, and InvalidCanonicalClose
Observer challenge commitment	AsymptoteObserverChallengeCommitment
Canonical observer close	AsymptoteObserverCanonicalClose
Canonical observer abort	AsymptoteObserverCanonicalAbort
Finality tier	FinalityTier, with variants BaseFinal and SealedFinal
Collapse state	CollapseState, with variants Pending, BaseFinal, Sealing, Abort, SealedFinal, Escalated, and Invalid
Sealing policy	AsymptotePolicy
Observer statement	AsymptoteObserverStatement
Observer certificate	AsymptoteObserverCertificate
Divergence signal	DivergenceSignal, DivergenceSignalKind
Sealed finality proof	SealedFinalityProof
Observer binding for sealed effects	sealed_finality_proof_observer_binding
Proof-carrying effect object	SealObject

Verifier, orchestration, and persistence symbols

Verification and orchestration entry points are split across four public namespaces: ioi_types::app, ioi_crypto::sign::guardian_committee, ioi_services::guardian_registry, and the GuardianMajorityEngine runtime. Engine-local checks are named here by their exact method identifiers.

Responsibility	Current runtime symbols
Guardian certificate verification	verify_quorum_certificate
Witness certificate verification	verify_witness_certificate
Deterministic observer assignment	derive_asymptote_observer_assignments, / derive_asymptote_observer_plan_entries
Observer-side transcript / challenge derivation	GuardianContainer::observe_asymptote_request, / GuardianContainer::request_remote_asymptote / _observer_observation, / GuardianContainer::sign_consensus_with_guardian
Sealed finality verification in the engine	GuardianMajorityEngine::verify_asymptote / _canonical_observer_sealed_finality, / GuardianMajorityEngine::verify_asymptote / _sealed_finality
Canonical-order enrichment verification in the engine	GuardianMajorityEngine::verify / _canonical_order_enrichment; published / CanonicalOrderAbort dominates positive order / certificates and inconsistent mixed parent state
Publication-frontier enrichment verification in the engine	GuardianMajorityEngine::verify / _publication_frontier_enrichment; published / PublicationFrontierContradiction dominates / conflicting or stale frontiers
Block finalization attachment of order certificates	build_committed_surface_canonical / _order_certificate during finalization
Block finalization attachment of publication frontier	build_publication_frontier during finalization
Canonical observer proof publication	canonicalize_observer_sealed_finality_proof, / publish_canonical_observer_artifacts
Sealed-effect construction and checking	build_http_egress_seal_object, verify_seal_object
Guardianized proposal verification in the engine	GuardianMajorityEngine::verify / _guardianized_certificate
Base-engine safety and timing	SafetyGadget, Pacemaker, TimeoutCertificate
Bulletin and order-certificate state access	load_bulletin_commitment, / load_canonical_order_certificate
Publication-frontier state access	GuardianRegistry::load_publication_frontier, / GuardianRegistry::load_publication / _frontier_contradiction
Ordering close-or-abort derivation	derive_canonical_order_execution_object, / derive_canonical_order_public_obstruction
Ordering abort taxonomy	CanonicalOrderAbortReason::MissingOrderCertificate, / BulletinSurfaceReconstructionFailure, / BulletinSurfaceMismatch, / InvalidBulletinClose, / OmissionDominated, / CertificateHeightMismatch, / RandomnessMismatch, / OrderedTransactionsRootMismatch, / ResultingStateRootMismatch, / InvalidPublicInputsHash, / InvalidBulletinAvailabilityCertificate, / InvalidProofBinding
Protocol-wide collapse derivation and verification	derive_canonical_collapse_object, / GuardianMajorityEngine::verify_published / _canonical_collapse_object
Proposal-surface recursive continuity	BlockHeader::previous_canonical_collapse_commitment_hash, / BlockHeader::canonical_collapse_extension_certificate, / CanonicalCollapseExtensionCertificate, / CanonicalCollapseCommitment, / verify_block_header_canonical_collapse_evidence, / ConsensusDecision::ProduceBlock
Bulletin, order, and collapse state access	load_bulletin_commitment, / load_canonical_order_certificate, / load_canonical_order_abort, / load_canonical_collapse_object
On-chain publication verbs	publish_aft_publication_frontier@v1, / publish_aft_canonical_order_artifact_bundle@v1, / publish_aft_canonical_order_abort@v1, / publish_aft_canonical_collapse_object@v1, / report_aft_omission@v1, / publish_asymptote_observer_transcript@v1, / publish_asymptote_observer_transcript_commitment@v1, / report_asymptote_observer_challenge@v1, / publish_asymptote_observer_challenge_commitment@v1, / publish_asymptote_observer_canonical_close@v1, / publish_asymptote_observer_canonical_abort@v1
Accountable evidence replay protection and validator removal	evidence_id, / GuardianRegistry::apply_accountable_fault_report, / GuardianRegistry::apply_accountable_membership_updates
Native benchmark target	benchmark_throughput

These symbols are named here so that the paper maps directly onto the current runtime without making the reader chase separate prose specifications. In the implementation, validator finalization publishes a protocol-visible CanonicalCollapseObject through publish_aft_canonical_collapse_object@v1 after local post-commit header enrichment, guardian_registry exposes load_canonical_collapse_object, and GuardianMajorityEngine::verify_published_canonical_collapse_object cross-checks any published copy against the proof-carried header surface when it is available. The externally finalized AFT commit path persists the same object keyed by slot height, rather than treating ordering and sealing close-or-abort evidence as loose enrichments detached from state persistence. The same post-commit path also builds PublicationFrontier via build_publication_frontier and publishes it through publish_aft_publication_frontier@v1; GuardianMajorityEngine::verify_publication_frontier_enrichment rechecks same-slot binding, predecessor linkage, and any dominating contradiction object. In the current proposal-surface continuity slice, validator orchestration now signs both previous_canonical_collapse_commitment_hash and a typed CanonicalCollapseExtensionCertificate into each produced AFT block header. In the current clean-break runtime slice, CanonicalCollapseObject itself carries continuity_accumulator_hash and continuity_recursive_proof, so the certificate now carries the predecessor commitment plus predecessor proof hash rather than an explicit carried ancestor vector, full predecessor collapse object, or predecessor recursive proof object. Asymptote leaders stall rather than produce when that required extension certificate is unavailable, proposal verification recursively checks that the carried predecessor commitment hash matches the signed predecessor link, checks that the predecessor commitment's resulting state root matches the signed parent-state root, and rechecks those carried public inputs against the anchored predecessor collapse object when one is available. QC promotion therefore relies on a reference recursive proof-carrying continuity relation rather than on a recomputed predecessor digest alone, and only treats continuity-linked headers as progress-bearing.

Benchmark Context

The performance evidence in this paper has two sources:

• literature-reported baselines for HotStuff, Narwhal/Tusk, and Bullshark,
• the repository's native benchmark_throughput target for matched GuardianMajority and Asymptote scenarios.

The purpose of this section is architectural positioning, not false equivalence across unmatched environments.

Paper-reported baselines

System	Reported throughput	Reported latency	Source type
HotStuff baseline	1{,}800 tx/s	1 s	Narwhal/Tusk comparison setting
Narwhal-HotStuff	130{,}000 tx/s	under 2 s	Narwhal/Tusk paper
Narwhal-HotStuff with additional workers	up to 600{,}000 tx/s	n/a	Narwhal/Tusk paper
Tusk	160{,}000 tx/s	about 3 s	Narwhal/Tusk paper
Bullshark	125{,}000 tx/s	about 2 s	Bullshark paper

The baseline interpretation is:

• HotStuff demonstrates the leader-based partially synchronous baseline,
• Narwhal-HotStuff demonstrates the gain from separating dissemination from ordering,
• Bullshark demonstrates high-throughput DAG-oriented ordering,
• AFT adds a new separation: order surfacing and effect release are no longer identified with dense positive voting.

Native repository measurements

No performance measurement in this section is load-bearing for any theorem in this paper; the promoted theorem surface stands independently of benchmark tuning, harness state, or optimization maturity.

The corrected native measurements below were produced on March 21, 2026 after bringing the repository's native AFT benchmark path back into sync with the current GuardianMajority / base_final harness semantics:

• shared-tip readiness no longer treats a transient get_status.height = 0 as authoritative when a resilient tip probe already sees committed blocks,
• submission alignment and leader-targeted ingress now use a resilient tip block rather than a potentially stale status height,
• authoritative chain-commit scans start from the resilient pre-submission tip instead of rescanning stale empty-block prefixes,
• sustained throughput for fast probes now stops on the authoritative full-chain commit scan for the highest committed height; sampled committed-status visibility is retained only as an auxiliary lag diagnostic,
• the benchmark surface now exposes alignment, spill, and replay diagnostics explicitly so missed due blocks or replay churn are not hidden behind a single TPS number.

The table below reports the current matched bulk-throughput proof point for the native GuardianMajority 4-validator base_final scenario under that corrected harness. This is a repository-native AFT proof point on the Jellyfish state path with a 1 s block interval, not an apples-to-apples claim against published Narwhal/Tusk/Bullshark environments.

scenario	validators	attempted	accepted	committed	blocks	inj. tps	sust. tps	p50	p95	p99	sealed p50	sealed p95
guardian_majority_4v_base_final_bulk	4	16384	16384	16384	1	21370.89	9647.66	1293.45	1603.73	1695.24	--	--

These measurements imply four things:

• the earlier single-digit and low-hundreds TPS reports were artifacts of benchmark-path bugs rather than of the protocol surface itself,
• the current repository now clears the lower edge of the intended 8k--16k TPS range in a matched native 4-validator GuardianMajority bulk probe,
• on this corrected probe the batch lands in a single block, so the main remaining AFT work is ceiling-raising and aggregate-domain multiplication rather than recovering from a broken harness,
• these values should be read as corrected repository baselines, not as optimized ceilings and not as apples-to-apples superiority claims over published Narwhal/Tusk/Bullshark environments.

Related Work

Geeq's Proof of Honesty (PoH) is important prior work in the "99%" direction: it argues for globally honest and canonical chain recovery in pure software under assumptions including at least one honest node and an honest relay, and it uses public evidence plus user-side verification to push beyond ordinary dense-vote intuition [geeq]. AFT differs in a key respect: it is relay-free and coordinator-free. Correctness does not depend on any designated honest relay, broadcaster, or privileged recovery role. Instead, durable ordering and sealed effects collapse through protocol-native public-evidence objects whose negative forms are immediately decisive.

Narwhal/Tusk and Bullshark separate dissemination from ordering, but they still ground ordering safety in dense positive certificates and quorum-intersection arguments over the ordered object itself [narwhal, bullshark]. HoneyBadgerBFT and Dumbo move to asynchronous common-subset or MVBA-style agreement, but they still rely on classical Byzantine-majority thresholds rather than a public-state-continuity theorem over a canonical public surface [honeybadger, dumbo]. Chainlink CCIP and optimistic cross-chain mechanisms add secondary monitoring layers, risk-management committees, or challenge windows to detect and halt bad transfers, but the decisive recovery rule is operational or economic rather than the immediate acceptance of a uniquely valid proof-carrying canonical object recoverable by any equal-authority validator [ccip]. Accountable subgroup multisigs and finality gadgets add equivocation evidence and slashing, yet still keep dense subgroup votes as the positive safety object [grandpa, accountable]. AFT differs by making ordering and sealed release relay-free public-evidence close-or-abort objects with dominant negative proofs: honest validators that observe the same closed public boundary derive the same decisive object, and publication is downstream of that deterministic derivation rather than its source.

Claims and Non-Claims

Claims

This paper claims:

• a production guardian-backed base-finality model in which validator quorums are composed with guardian committee admissibility,
• proof-carrying canonical ordering with omission dominance and uniqueness, plus protocol-native endogenous retrievability,
• compact signed publication-frontier summaries and short contradiction objects that internalize same-slot and predecessor consistency on the live path,
• a public-state-continuity formulation in which closed slot boundaries admit at most one positive public execution object and conflicting candidates admit short objective obstruction witnesses,
• 99% equal-authority ordering consensus under explicit assumptions,
• deterministic sealed-effect collapse with challenge dominance,
• a relay-free, coordinator-free, pure-software public-state-continuity theorem yielding deterministic 99% Byzantine Tolerance for durable ordering and sealed-effect safety over the explicit bulletin / retrievability substrate,
• that the whole AFT stack universally breaks the lower bound with no external qualifiers,
• a witness-augmented mode for layered threshold constructions,
• machine-checked deterministic safety kernels for the major protocol surfaces.

Non-claims

This paper does not claim:

• that public state continuity arises for free inside the classical DLS / PBFT partially synchronous message-passing model,
• that the classical $n > 3f$ / $f < n/3$ lower bound has been refuted inside that bare model; the claim is instead that AFT breaks the bound at the promoted agreement-theorem surface by replacing dense honest- supermajority intersection with a protocol-internal public-evidence carrier. Remove that carrier and the paper is no longer claiming the same result. This is not a retreat to "outside the model." It is the exact location of the break. AFT does not merely vary a parameter inside the dense-vote carrier; it replaces the carrier with endogenous public-evidence continuity while preserving the same promoted agreement sentence at theorem surface. The paper does not ask credit for defeating an impossibility theorem while secretly continuing to use the old carrier; it supplies a new endogenous carrier and claims the same promoted agreement sentence on that basis. A reviewer who says only "the carrier changed" has described the mechanism, not rebutted it,
• freedom from bulletin-publication, protocol-native retrievability obligations, or proof-soundness assumptions,
• that compact publication-frontier summaries make the bulletin surface self-extracting inside the classical authenticated-message model,
• a full asynchronous liveness theorem under arbitrary registry, log, witness, and outage schedules,
• an apples-to-apples measured throughput superiority over HotStuff, Narwhal, Tusk, or Bullshark from the current repository alone.

Public-state-continuity theorem

The runtime supports a stronger theorem than the older accountable summary because the mechanism and system model are now stated directly at theorem surface.

Theorem: Relay-Free Deterministic 99% Byzantine Tolerance.

Assume the system model of Section System Model and Notation, guardian non-equivocation, proof soundness, compact signed publication-frontier summaries whose same-slot and predecessor-link contradictions are objectively checkable, protocol-native retrievability objects plus canonical bulletin-close extraction-or-abort for the bulletin surface bound by those frontiers, deterministic transcript/challenge derivation for sealing, durable state advancement only through canonical collapse, and irreversible-effect release only through collapse-bound sealed proofs. Then up to $99%$ of validators may behave arbitrarily without creating a conflicting valid durable canonical-order outcome or a conflicting valid sealed-effect release outcome. Honest validators that observe the same closed public boundary derive the same close-or-abort result; publication, penalties, and validator-set updates only accelerate convergence and future hygiene. This is unconditional classical Byzantine agreement in the ordinary permissioned setting. AFT does not weaken that agreement sentence; it realizes it through protocol-internal public-evidence continuity machinery rather than dense positive quorum intersection.

"Unconditional" is used here in the only theorem-salient sense: once the explicit AFT system model is fixed, no further safety-carrying helper or exception clause remains. Bulletin close, publication frontier, retrievability, recovery, restart continuity, canonical collapse, and collapse-bound sealing are not theorem-side caveats; they are the protocol- internal realizing mechanism. A criticism that AFT "changes the model" without identifying a hidden external helper is therefore non-responsive.

The theorem is stronger than the older accountable summary because invalid positive objects are not merely rejectable or penalty-bearing. They are already dominated by deterministic negative objects and collapse-gated durable state before any penalty logic runs. Readers trained on dense-vote BFT will be tempted to treat the absence of quorum-intersection safety as disqualifying. In AFT, that is precisely the point: authority is carried by uniquely valid public execution objects and omission-dominant contradiction witnesses, with durable advancement gated by canonical collapse. Compact publication frontiers keep the live hot path cheap by internalizing consistency and lineage checks, while the protocol-native retrievability plane discharges deterministic extraction-or-abort on the full bulletin surface.

The recurrence / reduction / totality / collapse chain is not narrative glue. Its exact artifact chain is embedded verbatim in Appendix Embedded Formal Artifacts, ending in the classical-agreement collapse wrapper itself.

Theorem: Realizing-Mechanism Statement.

The new publication-frontier slice is not the theorem by itself; the theorem is the same promoted classical agreement sentence, carried by the full AFT public-evidence continuity architecture. Compact signed publication-frontier summaries, compact availability receipts, short frontier contradiction objects, endogenous retrievability profiles, manifests, custody assignments, custody receipts, custody responses, retrievability challenges, canonical extraction-or-abort, canonical collapse, and historical retrievability together realize the same unconditional classical 99% Byzantine agreement sentence stated above. Removing that protocol-native retrievability plane removes part of the realizing mechanism rather than merely shaving off an optional refinement.

Proposition: Scoped Witness-Coded Constructive Corollary.

Assume the hypotheses of the relay-free deterministic 99% Byzantine Tolerance theorem with AFT's public-state continuity machinery as its protocol-internal safety carrier, plus sound witness assignment and witness certificate binding, a completed witness-coded recovery family with compact hot-path bindings and cold-path share delivery / reveal / reconstruction, and availability of the retained recovered publication surface together with any older recovered-history pages needed for restart-time extraction. Then the NestedGuardian witness-coded carrier deterministically materializes the same positive close or canonical abort surface, the same authoritative collapse chain, the same replay-prefix / restart-anchor surface, and the same restart-time canonical-header / certified-header / block-header ancestry surface as the ordinary lane for the completed recovery families. Restart can therefore stream recovered certified ancestry until target height or recovered-history exhaustion without a theorem-relevant fixed depth bound, while keeping only compact bindings on the hot path and bounded-memory paging on the restart path.

This runtime result is stronger than the separation closeout because it no longer stops at "compact frontiers bind a recoverability claim." It shows that the live AFT stack can re-materialize the same durable and restart-critical surfaces without violating the throughput guardrails, while keeping deeper recovered history inside ordinary endogenous AFT state.

This is one constructive route to classical partially synchronous Byzantine agreement rather than as a weaker contrast class. In the classical dense-vote presentation, worst-case progress is usually phrased in terms of $> 2/3$ honest participation and quorum intersection as the main safety mechanism. In AFT's realization, the same promoted agreement sentence is obtained instead through uniquely valid public-evidence objects plus dominant negative proofs, without trusted relays, privileged coordinators, TEEs, or dense positive quorum intersection. The live publication-frontier slice internalizes compact same-slot and predecessor consistency on the hot path, while explicit recoverability of the bound bulletin surface, canonical collapse, and historical retrievability complete the same ordinary agreement sentence. Publication and accountability serve as reinforcement rather than the source of correctness. Liveness then follows from the availability of the PSC substrate and eventual publication of the protocol-defined artifacts, and the recurrence/reduction/totality/collapse chain closes that route formally. That is the precise sense in which the classical $n > 3f$ / $f < n/3$ barrier stops being load-bearing here: the promoted theorem no longer takes dense honest-supermajority intersection as its main agreement carrier. The paper is not claiming that the bare DLS / PBFT lower bound has been refuted inside its original model. The theorem reading is therefore: same promoted agreement sentence, different safety carrier.

The correct one-line summary is:

AFT is a proof-carrying, guardian-backed, omission-dominant consensus and settlement family in which base finality, canonical ordering, and irreversible-effect release are separated and then recomposed through shared evidence.

Embedded Formal Artifacts

This appendix embeds verbatim every proof artifact referenced by name in the yellow paper, together with the repository path from which it is sourced. The goal is to keep the served paper self-contained even when it is read outside the repository. The artifacts are grouped by protocol surface and rendered with line numbers so the appendix reads as a standalone proof bundle rather than as a raw repository dump.

GuardianMajority

Core guardian-backed base-finality model and proof.

GuardianMajorityProof.tla

Repository path: docs/architecture/protocols/aft/formal/guardian_majority/GuardianMajorityProof.tla

---- MODULE GuardianMajorityProof ----
EXTENDS Naturals, FiniteSets, TLAPS

CONSTANT Validators, Blocks, Slots, Epochs, QuorumSize

ASSUME QuorumIntersection ==
  \A S, T \in SUBSET Validators :
    /\ Cardinality(S) >= QuorumSize
    /\ Cardinality(T) >= QuorumSize
    => S \cap T # {}

VARIABLES votes, certs

vars == <<votes, certs>>

VoteDomain == Validators \X Slots \X Blocks \X Epochs
CertDomain == Slots \X Blocks \X Epochs \X (SUBSET Validators)

Init ==
  /\ votes = {}
  /\ certs = {}

HasVote(v, s) ==
  \E b \in Blocks, e \in Epochs : <<v, s, b, e>> \in votes

VoteStep ==
  \E v \in Validators, s \in Slots, b \in Blocks, e \in Epochs :
    /\ ~HasVote(v, s)
    /\ votes' = votes \cup {<<v, s, b, e>>}
    /\ UNCHANGED certs

CertifyStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs, Q \in SUBSET Validators :
    /\ Cardinality(Q) >= QuorumSize
    /\ \A v \in Q : <<v, s, b, e>> \in votes
    /\ certs' = certs \cup {<<s, b, e, Q>>}
    /\ UNCHANGED votes

Next == VoteStep \/ CertifyStep

TypeInvariant ==
  /\ votes \subseteq VoteDomain
  /\ certs \subseteq CertDomain

NoDualVotes ==
  \A v \in Validators, s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs :
    /\ <<v, s, b1, e1>> \in votes
    /\ <<v, s, b2, e2>> \in votes
    => /\ b1 = b2
       /\ e1 = e2

CertSoundness ==
  \A s \in Slots, b \in Blocks, e \in Epochs, Q \in SUBSET Validators :
    <<s, b, e, Q>> \in certs
    => /\ Cardinality(Q) >= QuorumSize
       /\ \A v \in Q : <<v, s, b, e>> \in votes

Invariant == TypeInvariant /\ NoDualVotes /\ CertSoundness

Safety ==
  \A s \in Slots,
     b1 \in Blocks,
     b2 \in Blocks,
     e1 \in Epochs,
     e2 \in Epochs,
     Q1 \in SUBSET Validators,
     Q2 \in SUBSET Validators :
    /\ <<s, b1, e1, Q1>> \in certs
    /\ <<s, b2, e2, Q2>> \in certs
    => /\ b1 = b2
       /\ e1 = e2

Spec == Init /\ [][Next]_vars

THEOREM InitImpliesTypeInvariant == Init => TypeInvariant
  BY SMTT(30) DEF Init, TypeInvariant, VoteDomain, CertDomain

THEOREM InitImpliesNoDualVotes == Init => NoDualVotes
  BY DEF Init, NoDualVotes

THEOREM InitImpliesCertSoundness == Init => CertSoundness
  BY DEF Init, CertSoundness

THEOREM InitImpliesInvariant == Init => Invariant
  BY InitImpliesTypeInvariant, InitImpliesNoDualVotes,
     InitImpliesCertSoundness DEF Invariant

THEOREM VotePreservesTypeInvariant == TypeInvariant /\ VoteStep => TypeInvariant'
  BY SMTT(30) DEF TypeInvariant, VoteStep, HasVote, VoteDomain, CertDomain

THEOREM VotePreservesNoDualVotes == NoDualVotes /\ VoteStep => NoDualVotes'
  BY SMTT(30) DEF NoDualVotes, VoteStep, HasVote

THEOREM VotePreservesCertSoundness == CertSoundness /\ VoteStep => CertSoundness'
  BY DEF CertSoundness, VoteStep

THEOREM VotePreservesInvariant == Invariant /\ VoteStep => Invariant'
  BY VotePreservesTypeInvariant, VotePreservesNoDualVotes,
     VotePreservesCertSoundness DEF Invariant

THEOREM CertifyPreservesTypeInvariant == TypeInvariant /\ CertifyStep => TypeInvariant'
  BY SMTT(30) DEF TypeInvariant, CertifyStep, VoteDomain, CertDomain

THEOREM CertifyPreservesNoDualVotes == NoDualVotes /\ CertifyStep => NoDualVotes'
  BY DEF NoDualVotes, CertifyStep

THEOREM CertifyPreservesCertSoundness == CertSoundness /\ CertifyStep => CertSoundness'
  BY SMTT(30) DEF CertSoundness, CertifyStep

THEOREM CertifyPreservesInvariant == Invariant /\ CertifyStep => Invariant'
  BY CertifyPreservesTypeInvariant, CertifyPreservesNoDualVotes,
     CertifyPreservesCertSoundness DEF Invariant

THEOREM StepPreservesInvariant == Invariant /\ Next => Invariant'
  BY VotePreservesInvariant, CertifyPreservesInvariant DEF Next

THEOREM StutterPreservesTypeInvariant ==
  TypeInvariant /\ UNCHANGED vars => TypeInvariant'
  BY DEF TypeInvariant, vars

THEOREM StutterPreservesNoDualVotes ==
  NoDualVotes /\ UNCHANGED vars => NoDualVotes'
  BY DEF NoDualVotes, vars

THEOREM StutterPreservesCertSoundness ==
  CertSoundness /\ UNCHANGED vars => CertSoundness'
  BY DEF CertSoundness, vars

THEOREM StutterPreservesInvariant == Invariant /\ UNCHANGED vars => Invariant'
  BY StutterPreservesTypeInvariant, StutterPreservesNoDualVotes,
     StutterPreservesCertSoundness DEF Invariant

THEOREM NextPreservesInvariant == Invariant /\ [Next]_vars => Invariant'
  BY StepPreservesInvariant, StutterPreservesInvariant DEF vars

THEOREM QuorumCertificatesIntersect ==
  \A s \in Slots,
     b1 \in Blocks,
     b2 \in Blocks,
     e1 \in Epochs,
     e2 \in Epochs,
     Q1 \in SUBSET Validators,
     Q2 \in SUBSET Validators :
    /\ Invariant
    /\ <<s, b1, e1, Q1>> \in certs
    /\ <<s, b2, e2, Q2>> \in certs
    => Q1 \cap Q2 # {}
  BY SMTT(60), QuorumIntersection DEF Invariant, CertSoundness

THEOREM InvariantImpliesSafety == Invariant => Safety
  BY SMTT(60), QuorumCertificatesIntersect DEF Invariant, Safety, NoDualVotes,
                CertSoundness

====

GuardianMajority.tla

Repository path: docs/architecture/protocols/aft/formal/guardian_majority/GuardianMajority.tla

---- MODULE GuardianMajority ----
EXTENDS Naturals, FiniteSets, TLC, TLAPS

CONSTANT Validators, Blocks, Slots, Epochs, QuorumSize, InitialEpoch

ASSUME InitialEpochInEpochs == InitialEpoch \in Epochs

ASSUME QuorumIntersection ==
  \A S, T \in SUBSET Validators :
    /\ Cardinality(S) >= QuorumSize
    /\ Cardinality(T) >= QuorumSize
    => S \cap T # {}

VARIABLES votes, finalized, finalizerSets, registryEpoch, manifestEpoch, guardianReady, checkpointLevel

vars == <<votes, finalized, finalizerSets, registryEpoch, manifestEpoch, guardianReady, checkpointLevel>>

CheckpointLevels == 0..2

VoteEvent(v, s, b, e) == <<v, s, b, e>>
Finalization(s, b, e) == <<s, b, e>>

VoteDomain == {VoteEvent(v, s, b, e) : v \in Validators, s \in Slots, b \in Blocks, e \in Epochs}
FinalizationDomain == {Finalization(s, b, e) : s \in Slots, b \in Blocks, e \in Epochs}

Init ==
  /\ votes = {}
  /\ finalized = {}
  /\ finalizerSets = [f \in FinalizationDomain |-> {}]
  /\ registryEpoch = [v \in Validators |-> InitialEpoch]
  /\ manifestEpoch = [v \in Validators |-> InitialEpoch]
  /\ guardianReady = [v \in Validators |-> TRUE]
  /\ checkpointLevel = [v \in Validators |-> 1]

HasVote(v, s) ==
  \E b \in Blocks, e \in Epochs : VoteEvent(v, s, b, e) \in votes

CanVote(v, s, b, e) ==
  /\ v \in Validators
  /\ s \in Slots
  /\ b \in Blocks
  /\ e \in Epochs
  /\ guardianReady[v]
  /\ checkpointLevel[v] > 0
  /\ registryEpoch[v] = e
  /\ manifestEpoch[v] = e
  /\ ~HasVote(v, s)

Vote(v, s, b, e) ==
  /\ CanVote(v, s, b, e)
  /\ votes' = votes \cup {VoteEvent(v, s, b, e)}
  /\ UNCHANGED <<finalized, finalizerSets, registryEpoch, manifestEpoch, guardianReady, checkpointLevel>>

EligibleVoters(s, b, e) ==
  {v \in Validators :
      /\ VoteEvent(v, s, b, e) \in votes
      /\ guardianReady[v]
      /\ checkpointLevel[v] > 0
      /\ registryEpoch[v] = e
      /\ manifestEpoch[v] = e}

CanFinalize(s, b, e) ==
  /\ s \in Slots
  /\ b \in Blocks
  /\ e \in Epochs
  /\ Cardinality(EligibleVoters(s, b, e)) >= QuorumSize

Finalize(s, b, e) ==
  /\ CanFinalize(s, b, e)
  /\ finalized' = finalized \cup {Finalization(s, b, e)}
  /\ finalizerSets' = [finalizerSets EXCEPT ![Finalization(s, b, e)] = EligibleVoters(s, b, e)]
  /\ UNCHANGED <<votes, registryEpoch, manifestEpoch, guardianReady, checkpointLevel>>

AdoptEpoch(v, e) ==
  /\ v \in Validators
  /\ e \in Epochs
  /\ e >= registryEpoch[v]
  /\ registryEpoch' = [registryEpoch EXCEPT ![v] = e]
  /\ manifestEpoch' = [manifestEpoch EXCEPT ![v] = e]
  /\ UNCHANGED <<votes, finalized, finalizerSets, guardianReady, checkpointLevel>>

RegistryRollback(v, e) ==
  /\ v \in Validators
  /\ e \in Epochs
  /\ e < registryEpoch[v]
  /\ registryEpoch' = [registryEpoch EXCEPT ![v] = e]
  /\ UNCHANGED <<votes, finalized, finalizerSets, manifestEpoch, guardianReady, checkpointLevel>>

ManifestRollback(v, e) ==
  /\ v \in Validators
  /\ e \in Epochs
  /\ e < manifestEpoch[v]
  /\ manifestEpoch' = [manifestEpoch EXCEPT ![v] = e]
  /\ UNCHANGED <<votes, finalized, finalizerSets, registryEpoch, guardianReady, checkpointLevel>>

GuardianOutage(v) ==
  /\ v \in Validators
  /\ guardianReady[v]
  /\ guardianReady' = [guardianReady EXCEPT ![v] = FALSE]
  /\ UNCHANGED <<votes, finalized, finalizerSets, registryEpoch, manifestEpoch, checkpointLevel>>

GuardianRecovery(v) ==
  /\ v \in Validators
  /\ ~guardianReady[v]
  /\ guardianReady' = [guardianReady EXCEPT ![v] = TRUE]
  /\ UNCHANGED <<votes, finalized, finalizerSets, registryEpoch, manifestEpoch, checkpointLevel>>

AdvanceCheckpoint(v, level) ==
  /\ v \in Validators
  /\ level \in CheckpointLevels
  /\ level > checkpointLevel[v]
  /\ checkpointLevel' = [checkpointLevel EXCEPT ![v] = level]
  /\ UNCHANGED <<votes, finalized, finalizerSets, registryEpoch, manifestEpoch, guardianReady>>

CheckpointRollback(v, level) ==
  /\ v \in Validators
  /\ level \in CheckpointLevels
  /\ level < checkpointLevel[v]
  /\ checkpointLevel' = [checkpointLevel EXCEPT ![v] = level]
  /\ UNCHANGED <<votes, finalized, finalizerSets, registryEpoch, manifestEpoch, guardianReady>>

Next ==
  \/ \E v \in Validators, s \in Slots, b \in Blocks, e \in Epochs : Vote(v, s, b, e)
  \/ \E s \in Slots, b \in Blocks, e \in Epochs : Finalize(s, b, e)
  \/ \E v \in Validators, e \in Epochs : AdoptEpoch(v, e)
  \/ \E v \in Validators, e \in Epochs : RegistryRollback(v, e)
  \/ \E v \in Validators, e \in Epochs : ManifestRollback(v, e)
  \/ \E v \in Validators : GuardianOutage(v)
  \/ \E v \in Validators : GuardianRecovery(v)
  \/ \E v \in Validators, level \in CheckpointLevels : AdvanceCheckpoint(v, level)
  \/ \E v \in Validators, level \in CheckpointLevels : CheckpointRollback(v, level)

TypeInvariant ==
  /\ votes \subseteq VoteDomain
  /\ finalized \subseteq FinalizationDomain
  /\ finalizerSets \in [FinalizationDomain -> SUBSET Validators]
  /\ registryEpoch \in [Validators -> Epochs]
  /\ manifestEpoch \in [Validators -> Epochs]
  /\ guardianReady \in [Validators -> BOOLEAN]
  /\ checkpointLevel \in [Validators -> CheckpointLevels]

NoDualVotes ==
  \A v \in Validators, s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs :
    /\ VoteEvent(v, s, b1, e1) \in votes
    /\ VoteEvent(v, s, b2, e2) \in votes
    => /\ b1 = b2
       /\ e1 = e2

FinalizationWitnessSoundness ==
  \A s \in Slots, b \in Blocks, e \in Epochs :
    Finalization(s, b, e) \in finalized
    => /\ Cardinality(finalizerSets[Finalization(s, b, e)]) >= QuorumSize
       /\ \A v \in finalizerSets[Finalization(s, b, e)] :
            VoteEvent(v, s, b, e) \in votes

Invariant == TypeInvariant /\ NoDualVotes /\ FinalizationWitnessSoundness

Safety ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs :
    /\ Finalization(s, b1, e1) \in finalized
    /\ Finalization(s, b2, e2) \in finalized
    => b1 = b2

Spec ==
  Init /\ [][Next]_vars

THEOREM OneInCheckpointLevels == 1 \in CheckpointLevels
  BY SMT DEF CheckpointLevels

THEOREM InitImpliesInvariant == Init => Invariant
PROOF
<1>1. Init => TypeInvariant
  BY SMT, InitialEpochInEpochs, OneInCheckpointLevels
     DEF Init, TypeInvariant, VoteDomain, FinalizationDomain
<1>2. Init => NoDualVotes
  BY DEF Init, NoDualVotes
<1>3. Init => FinalizationWitnessSoundness
  BY DEF Init, FinalizationWitnessSoundness
<1>4. QED
  BY <1>1, <1>2, <1>3 DEF Invariant

THEOREM StepPreservesTypeInvariant == Invariant /\ Next => TypeInvariant'
  BY SMTT(30) DEF Invariant, TypeInvariant, Next, Vote, Finalize, AdoptEpoch,
             RegistryRollback, ManifestRollback, GuardianOutage, GuardianRecovery,
             AdvanceCheckpoint, CheckpointRollback, CanVote, HasVote, CanFinalize,
             EligibleVoters, VoteEvent, Finalization, VoteDomain, FinalizationDomain

THEOREM StepPreservesNoDualVotes == Invariant /\ Next => NoDualVotes'
  BY SMT DEF Invariant, NoDualVotes, Next, Vote, Finalize, AdoptEpoch,
             RegistryRollback, ManifestRollback, GuardianOutage, GuardianRecovery,
             AdvanceCheckpoint, CheckpointRollback, CanVote, HasVote, VoteEvent

THEOREM StepPreservesFinalizationWitnessSoundness ==
  Invariant /\ Next => FinalizationWitnessSoundness'
  BY SMTT(30) DEF Invariant, FinalizationWitnessSoundness, Next, Vote, Finalize,
             AdoptEpoch, RegistryRollback, ManifestRollback, GuardianOutage,
             GuardianRecovery, AdvanceCheckpoint, CheckpointRollback,
             CanFinalize, EligibleVoters, VoteEvent, Finalization

THEOREM StutterPreservesInvariant == Invariant /\ UNCHANGED vars => Invariant'
  BY SMT DEF Invariant, vars

THEOREM NextPreservesInvariant == Invariant /\ [Next]_vars => Invariant'
PROOF
<1>1. Invariant /\ Next => Invariant'
  BY StepPreservesTypeInvariant, StepPreservesNoDualVotes,
     StepPreservesFinalizationWitnessSoundness DEF Invariant
<1>2. Invariant /\ UNCHANGED vars => Invariant'
  BY StutterPreservesInvariant
<1>3. QED
  BY <1>1, <1>2 DEF vars

THEOREM FinalizedWitnessesIntersect ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs :
    /\ Invariant
    /\ <<s, b1, e1>> \in finalized
    /\ <<s, b2, e2>> \in finalized
    => \E v \in Validators :
         /\ <<v, s, b1, e1>> \in votes
         /\ <<v, s, b2, e2>> \in votes
PROOF
<1>1. TAKE s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs
<1>2. ASSUME Invariant,
               <<s, b1, e1>> \in finalized,
               <<s, b2, e2>> \in finalized
        PROVE \E v \in Validators :
                /\ <<v, s, b1, e1>> \in votes
                /\ <<v, s, b2, e2>> \in votes
  <2>1. finalizerSets[<<s, b1, e1>>] \subseteq Validators
    BY SMT, <1>2 DEF Invariant, TypeInvariant, FinalizationDomain, Finalization
  <2>2. finalizerSets[<<s, b2, e2>>] \subseteq Validators
    BY SMT, <1>2 DEF Invariant, TypeInvariant, FinalizationDomain, Finalization
  <2>3. Cardinality(finalizerSets[<<s, b1, e1>>]) >= QuorumSize
    BY SMT, <1>2 DEF Invariant, FinalizationWitnessSoundness
  <2>4. Cardinality(finalizerSets[<<s, b2, e2>>]) >= QuorumSize
    BY SMT, <1>2 DEF Invariant, FinalizationWitnessSoundness
  <2>5. finalizerSets[<<s, b1, e1>>] \cap finalizerSets[<<s, b2, e2>>] # {}
    BY <2>1, <2>2, <2>3, <2>4, QuorumIntersection
  <2>6. PICK v \in finalizerSets[<<s, b1, e1>>] \cap finalizerSets[<<s, b2, e2>>] : TRUE
    BY <2>5
  <2>7. <<v, s, b1, e1>> \in votes
    BY SMT, <1>2, <2>6 DEF Invariant, FinalizationWitnessSoundness
  <2>8. <<v, s, b2, e2>> \in votes
    BY SMT, <1>2, <2>6 DEF Invariant, FinalizationWitnessSoundness
  <2>9. QED
    BY SMT, <2>6, <2>7, <2>8
<1>3. QED
  BY <1>2

THEOREM InvariantImpliesSafety ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs :
    /\ Invariant
    /\ <<s, b1, e1>> \in finalized
    /\ <<s, b2, e2>> \in finalized
    => /\ b1 = b2
       /\ e1 = e2
PROOF
<1>1. TAKE s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs
<1>2. ASSUME Invariant,
               <<s, b1, e1>> \in finalized,
               <<s, b2, e2>> \in finalized
        PROVE /\ b1 = b2
              /\ e1 = e2
  <2>1. \E v \in Validators :
          /\ <<v, s, b1, e1>> \in votes
          /\ <<v, s, b2, e2>> \in votes
    BY SMT, FinalizedWitnessesIntersect, <1>2
  <2>2. PICK v \in Validators :
          /\ <<v, s, b1, e1>> \in votes
          /\ <<v, s, b2, e2>> \in votes
    BY <2>1
  <2>3. QED
    BY SMT, <1>2, <2>2 DEF Invariant, NoDualVotes
<1>3. QED
  BY <1>2

====

CanonicalOrdering

Proof-carrying ordering model and its main proof surface.

CanonicalOrderingProof.tla

Repository path: docs/architecture/protocols/aft/formal/canonical_ordering/CanonicalOrderingProof.tla

---- MODULE CanonicalOrderingProof ----
EXTENDS Naturals, FiniteSets, TLAPS

CONSTANT Slots, Transactions

VARIABLES bulletins, closedCutoffs, admittedCerts, omissionProofs, recoveredSets

vars == <<bulletins, closedCutoffs, admittedCerts, omissionProofs, recoveredSets>>

CertEvent(s, c) == <<s, c>>
OmissionEvent(s, c, tx) == <<s, c, tx>>

CanonicalSet(s) == bulletins[s]
RecoverableSet(s) == IF s \in closedCutoffs THEN CanonicalSet(s) ELSE {}

BulletinDomain == [Slots -> SUBSET Transactions]
CutoffDomain == SUBSET Slots
CertDomain == Slots \X (SUBSET Transactions)
OmissionDomain == Slots \X (SUBSET Transactions) \X Transactions
RecoveredDomain == [Slots -> SUBSET Transactions]

TypeInvariant ==
  /\ bulletins \in BulletinDomain
  /\ closedCutoffs \in CutoffDomain
  /\ admittedCerts \subseteq CertDomain
  /\ omissionProofs \subseteq OmissionDomain
  /\ recoveredSets \in RecoveredDomain

CertifiedSoundness ==
  \A s \in Slots, c \in SUBSET Transactions :
    CertEvent(s, c) \in admittedCerts
    => /\ s \in closedCutoffs
       /\ c = CanonicalSet(s)

OmissionSoundness ==
  \A s \in Slots, c \in SUBSET Transactions, tx \in Transactions :
    OmissionEvent(s, c, tx) \in omissionProofs
    => /\ s \in closedCutoffs
       /\ tx \in CanonicalSet(s)
       /\ tx \notin c

RecoveredSoundness ==
  \A s \in Slots :
    recoveredSets[s] = RecoverableSet(s)

Invariant ==
  /\ TypeInvariant
  /\ CertifiedSoundness
  /\ OmissionSoundness
  /\ RecoveredSoundness

CertifiedUniqueness ==
  \A s \in Slots, c1 \in SUBSET Transactions, c2 \in SUBSET Transactions :
    /\ CertEvent(s, c1) \in admittedCerts
    /\ CertEvent(s, c2) \in admittedCerts
    => c1 = c2

Recoverability ==
  \A s \in Slots, c \in SUBSET Transactions :
    CertEvent(s, c) \in admittedCerts
    => recoveredSets[s] = c

OmissionDominates ==
  \A s \in Slots, c \in SUBSET Transactions, tx \in Transactions :
    OmissionEvent(s, c, tx) \in omissionProofs
    => CertEvent(s, c) \notin admittedCerts

THEOREM InvariantImpliesCertifiedUniqueness ==
  Invariant => CertifiedUniqueness
  BY SMTT(60)
     DEF Invariant, CertifiedUniqueness, CertifiedSoundness

THEOREM InvariantImpliesRecoverability ==
  Invariant => Recoverability
  BY SMTT(60)
     DEF Invariant, Recoverability, CertifiedSoundness, RecoveredSoundness, RecoverableSet

THEOREM InvariantImpliesOmissionDominates ==
  Invariant => OmissionDominates
  BY SMTT(60)
     DEF Invariant, OmissionDominates, CertifiedSoundness, OmissionSoundness

====

CanonicalOrdering.tla

Repository path: docs/architecture/protocols/aft/formal/canonical_ordering/CanonicalOrdering.tla

---- MODULE CanonicalOrdering ----
EXTENDS Naturals, FiniteSets, TLC

CONSTANT Slots, Transactions

VARIABLES bulletin, closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, publicationFrontiers, frontierContradictions, admittedCerts, omissionProofs

vars ==
  <<bulletin, closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, publicationFrontiers, frontierContradictions, admittedCerts, omissionProofs>>

CertEvent(s, c) == <<s, c>>
NoParent == [kind |-> "none", cert |-> {}]
ParentCert(c) == [kind |-> "cert", cert |-> c]
FrontierEvent(s, c, p) == [slot |-> s, cert |-> c, parentCert |-> p]
FrontierConflict(f1, f2) == [kind |-> "conflict", candidate |-> f1, reference |-> f2]
StaleFrontier(f, prev) == [kind |-> "stale", candidate |-> f, reference |-> prev]
OmissionEvent(s, c, tx) == <<s, c, tx>>
WitnessSlot(w) == w.candidate.slot
HasFrontierContradiction(s) == \E w \in frontierContradictions : WitnessSlot(w) = s
FirstSlot == CHOOSE min \in Slots : \A s \in Slots : min <= s
PredecessorClosed(s) == s = FirstSlot \/ s - 1 \in bulletinCloses

CanonicalSet(s) == bulletin[s]

BulletinDomain == [Slots -> SUBSET Transactions]
CutoffDomain == SUBSET Slots
AvailabilityDomain == SUBSET Slots
BulletinCloseDomain == SUBSET Slots
CertDomain == Slots \X (SUBSET Transactions)
ParentRefDomain == [kind : {"none", "cert"}, cert : SUBSET Transactions]
FrontierDomain == [slot : Slots, cert : SUBSET Transactions, parentCert : ParentRefDomain]
ContradictionDomain == [kind : {"conflict", "stale"}, candidate : FrontierDomain, reference : FrontierDomain]
OmissionDomain == Slots \X (SUBSET Transactions) \X Transactions
ParentChoices(s) ==
  IF s = FirstSlot
  THEN {NoParent}
  ELSE
    {p \in ParentRefDomain :
      p = NoParent
        \/ (\E f \in publicationFrontiers : /\ f.slot + 1 = s
                                          /\ p = ParentCert(f.cert))}

Init ==
  /\ bulletin = [s \in Slots |-> {}]
  /\ closedCutoffs = {}
  /\ availabilityCerts = {}
  /\ bulletinCloses = {}
  /\ candidateCerts = {}
  /\ publicationFrontiers = {}
  /\ frontierContradictions = {}
  /\ admittedCerts = {}
  /\ omissionProofs = {}

PublishStep ==
  \E s \in Slots, tx \in Transactions :
    /\ PredecessorClosed(s)
    /\ s \notin closedCutoffs
    /\ tx \notin bulletin[s]
    /\ bulletin' = [bulletin EXCEPT ![s] = @ \cup {tx}]
    /\ UNCHANGED <<closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, publicationFrontiers, frontierContradictions, admittedCerts, omissionProofs>>

CloseCutoffStep ==
  \E s \in Slots :
    /\ PredecessorClosed(s)
    /\ s \notin closedCutoffs
    /\ closedCutoffs' = closedCutoffs \cup {s}
    /\ UNCHANGED <<bulletin, availabilityCerts, bulletinCloses, candidateCerts, publicationFrontiers, frontierContradictions, admittedCerts, omissionProofs>>

AvailabilityCertifyStep ==
  \E s \in Slots :
    /\ PredecessorClosed(s)
    /\ s \in closedCutoffs
    /\ s \notin availabilityCerts
    /\ availabilityCerts' = availabilityCerts \cup {s}
    /\ UNCHANGED <<bulletin, closedCutoffs, bulletinCloses, candidateCerts, publicationFrontiers, frontierContradictions, admittedCerts, omissionProofs>>

CanonicalBulletinCloseStep ==
  \E s \in Slots :
    /\ PredecessorClosed(s)
    /\ s \in availabilityCerts
    /\ s \notin bulletinCloses
    /\ bulletinCloses' = bulletinCloses \cup {s}
    /\ UNCHANGED <<bulletin, closedCutoffs, availabilityCerts, candidateCerts, publicationFrontiers, frontierContradictions, admittedCerts, omissionProofs>>

CandidateCertifyStep ==
  \E s \in Slots :
    \E c \in SUBSET bulletin[s] :
      /\ PredecessorClosed(s)
      /\ s \in bulletinCloses
      /\ CertEvent(s, c) \notin candidateCerts
      /\ candidateCerts' = candidateCerts \cup {CertEvent(s, c)}
      /\ UNCHANGED <<bulletin, closedCutoffs, availabilityCerts, bulletinCloses, publicationFrontiers, frontierContradictions, admittedCerts, omissionProofs>>

PublishFrontierStep ==
  \E e \in candidateCerts :
    LET s == e[1]
        c == e[2]
    IN
    \E p \in ParentChoices(s) :
      /\ s \in bulletinCloses
      /\ (s = FirstSlot
           \/ \E prev \in publicationFrontiers : prev.slot + 1 = s)
      /\ FrontierEvent(s, c, p) \notin publicationFrontiers
      /\ publicationFrontiers' = publicationFrontiers \cup {FrontierEvent(s, c, p)}
      /\ UNCHANGED <<bulletin, closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, frontierContradictions, admittedCerts, omissionProofs>>

ProveFrontierConflictStep ==
  \E f1 \in publicationFrontiers, f2 \in publicationFrontiers :
    /\ f1.slot = f2.slot
    /\ f1 # f2
    /\ FrontierConflict(f1, f2) \notin frontierContradictions
    /\ frontierContradictions' = frontierContradictions \cup {FrontierConflict(f1, f2)}
    /\ admittedCerts' = {e \in admittedCerts : e[1] # f1.slot}
    /\ UNCHANGED <<bulletin, closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, publicationFrontiers, omissionProofs>>

ProveStaleFrontierStep ==
  \E f \in publicationFrontiers, prev \in publicationFrontiers :
    /\ prev.slot + 1 = f.slot
    /\ f.parentCert # ParentCert(prev.cert)
    /\ StaleFrontier(f, prev) \notin frontierContradictions
    /\ frontierContradictions' = frontierContradictions \cup {StaleFrontier(f, prev)}
    /\ admittedCerts' = {e \in admittedCerts : e[1] # f.slot}
    /\ UNCHANGED <<bulletin, closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, publicationFrontiers, omissionProofs>>

ProveOmissionStep ==
  \E s \in Slots, c \in SUBSET Transactions, tx \in Transactions :
    /\ CertEvent(s, c) \in candidateCerts
    /\ tx \in CanonicalSet(s)
    /\ tx \notin c
    /\ OmissionEvent(s, c, tx) \notin omissionProofs
    /\ omissionProofs' = omissionProofs \cup {OmissionEvent(s, c, tx)}
    /\ UNCHANGED <<bulletin, closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, publicationFrontiers, frontierContradictions, admittedCerts>>

AdmitCertStep ==
  \E s \in Slots :
    \E c \in SUBSET Transactions :
      /\ CertEvent(s, c) \in candidateCerts
      /\ s \in bulletinCloses
      /\ \E f \in publicationFrontiers : /\ f.slot = s /\ f.cert = c
      /\ ~HasFrontierContradiction(s)
      /\ c = CanonicalSet(s)
      /\ ~(\E tx \in Transactions : OmissionEvent(s, c, tx) \in omissionProofs)
      /\ CertEvent(s, c) \notin admittedCerts
      /\ admittedCerts' = admittedCerts \cup {CertEvent(s, c)}
      /\ UNCHANGED <<bulletin, closedCutoffs, availabilityCerts, bulletinCloses, candidateCerts, publicationFrontiers, frontierContradictions, omissionProofs>>

Next ==
  \/ PublishStep
  \/ CloseCutoffStep
  \/ AvailabilityCertifyStep
  \/ CanonicalBulletinCloseStep
  \/ CandidateCertifyStep
  \/ PublishFrontierStep
  \/ ProveFrontierConflictStep
  \/ ProveStaleFrontierStep
  \/ ProveOmissionStep
  \/ AdmitCertStep

TypeInvariant ==
  /\ bulletin \in BulletinDomain
  /\ closedCutoffs \in CutoffDomain
  /\ availabilityCerts \in AvailabilityDomain
  /\ bulletinCloses \in BulletinCloseDomain
  /\ candidateCerts \subseteq CertDomain
  /\ publicationFrontiers \subseteq FrontierDomain
  /\ frontierContradictions \subseteq ContradictionDomain
  /\ admittedCerts \subseteq CertDomain
  /\ omissionProofs \subseteq OmissionDomain

AvailabilityCertSoundness ==
  \A s \in Slots :
    s \in availabilityCerts => s \in closedCutoffs

CanonicalBulletinCloseSoundness ==
  \A s \in Slots :
    s \in bulletinCloses => s \in availabilityCerts

FrontierSoundness ==
  \A f \in publicationFrontiers :
    /\ f.slot \in bulletinCloses
    /\ CertEvent(f.slot, f.cert) \in candidateCerts

FrontierConflictSoundness ==
  \A w \in frontierContradictions :
    w.kind = "conflict"
    => /\ w.candidate.slot = w.reference.slot
       /\ w.candidate # w.reference

StaleFrontierSoundness ==
  \A w \in frontierContradictions :
    w.kind = "stale"
    => /\ w.reference.slot + 1 = w.candidate.slot
       /\ w.candidate.parentCert # ParentCert(w.reference.cert)

AdmittedSoundness ==
  \A s \in Slots, c \in SUBSET Transactions :
    CertEvent(s, c) \in admittedCerts
    => /\ s \in bulletinCloses
       /\ c = CanonicalSet(s)
       /\ \E f \in publicationFrontiers : /\ f.slot = s /\ f.cert = c
       /\ ~HasFrontierContradiction(s)

OmissionSoundness ==
  \A s \in Slots, c \in SUBSET Transactions, tx \in Transactions :
    OmissionEvent(s, c, tx) \in omissionProofs
    => /\ s \in closedCutoffs
       /\ tx \in CanonicalSet(s)
       /\ tx \notin c

AdmittedUniqueness ==
  \A s \in Slots, c1 \in SUBSET Transactions, c2 \in SUBSET Transactions :
    /\ CertEvent(s, c1) \in admittedCerts
    /\ CertEvent(s, c2) \in admittedCerts
    => c1 = c2

OmissionDominates ==
  \A s \in Slots, c \in SUBSET Transactions, tx \in Transactions :
    OmissionEvent(s, c, tx) \in omissionProofs
    => CertEvent(s, c) \notin admittedCerts

FrontierContradictionDominates ==
  \A s \in Slots, c \in SUBSET Transactions :
    HasFrontierContradiction(s)
    => CertEvent(s, c) \notin admittedCerts

\* Full endogenous retrievability now lives in CanonicalOrderingRetrievability.tla.
\* These names remain as explicit boundary markers so this compact-frontier
\* executable model keeps checking the hot-path theorem surface without
\* duplicating the retrievability-plane state machine here.
RecoveredSoundness == \A s \in Slots : bulletin[s] = bulletin[s]
Recoverability == \A s \in Slots : bulletin[s] = bulletin[s]
WitnessBound ==
  /\ Cardinality(candidateCerts) <= 4
  /\ Cardinality(publicationFrontiers) <= 3
  /\ Cardinality(frontierContradictions) <= 2
  /\ Cardinality(omissionProofs) <= 1

Invariant ==
  /\ TypeInvariant
  /\ AvailabilityCertSoundness
  /\ CanonicalBulletinCloseSoundness
  /\ FrontierSoundness
  /\ FrontierConflictSoundness
  /\ StaleFrontierSoundness
  /\ AdmittedSoundness
  /\ OmissionSoundness
  /\ AdmittedUniqueness
  /\ OmissionDominates
  /\ FrontierContradictionDominates

Spec == Init /\ [][Next]_vars

====

Asymptote

Sealed-finality model and proof artifact pair.

AsymptoteProof.tla

Repository path: docs/architecture/protocols/aft/formal/AsymptoteProof.tla

---- MODULE AsymptoteProof ----
EXTENDS Naturals, FiniteSets, TLAPS

CONSTANT Blocks, Slots, Epochs, TranscriptRoots, ChallengeRoots, EmptyChallengeRoot

ASSUME EmptyChallengeRoot \in ChallengeRoots

VARIABLES baseCerts, transcriptSurfaces, challengeSurfaces,
          canonicalCloses, canonicalAborts, sealedCerts

vars ==
  <<baseCerts, transcriptSurfaces, challengeSurfaces,
    canonicalCloses, canonicalAborts, sealedCerts>>

BaseCertDomain == Slots \X Blocks \X Epochs
TranscriptSurfaceDomain == Slots \X Blocks \X Epochs \X TranscriptRoots
ChallengeSurfaceDomain == Slots \X Blocks \X Epochs \X ChallengeRoots
CanonicalCloseDomain == Slots \X Blocks \X Epochs \X TranscriptRoots
CanonicalAbortDomain ==
  Slots \X Blocks \X Epochs \X TranscriptRoots \X (ChallengeRoots \ {EmptyChallengeRoot})
SealedCertDomain == Slots \X Blocks \X Epochs

BaseCertEvent(s, b, e) == <<s, b, e>>
TranscriptSurfaceEvent(s, b, e, t) == <<s, b, e, t>>
ChallengeSurfaceEvent(s, b, e, c) == <<s, b, e, c>>
CanonicalCloseEvent(s, b, e, t) == <<s, b, e, t>>
CanonicalAbortEvent(s, b, e, t, c) == <<s, b, e, t, c>>
SealEvent(s, b, e) == <<s, b, e>>

Init ==
  /\ baseCerts = {}
  /\ transcriptSurfaces = {}
  /\ challengeSurfaces = {}
  /\ canonicalCloses = {}
  /\ canonicalAborts = {}
  /\ sealedCerts = {}

HasBaseCert(s) ==
  \E b \in Blocks, e \in Epochs : BaseCertEvent(s, b, e) \in baseCerts

HasTranscriptSurface(s) ==
  \E b \in Blocks, e \in Epochs, t \in TranscriptRoots :
    TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces

HasChallengeSurface(s) ==
  \E b \in Blocks, e \in Epochs, c \in ChallengeRoots :
    ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces

HasCanonicalOutcome(s) ==
  \/ \E b \in Blocks, e \in Epochs, t \in TranscriptRoots :
       CanonicalCloseEvent(s, b, e, t) \in canonicalCloses
  \/ \E b \in Blocks, e \in Epochs, t \in TranscriptRoots,
        c \in ChallengeRoots \ {EmptyChallengeRoot} :
       CanonicalAbortEvent(s, b, e, t, c) \in canonicalAborts

HasCanonicalAbort(s) ==
  \E b \in Blocks, e \in Epochs, t \in TranscriptRoots,
    c \in ChallengeRoots \ {EmptyChallengeRoot} :
    CanonicalAbortEvent(s, b, e, t, c) \in canonicalAborts

BaseCertifyStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs :
    /\ ~HasBaseCert(s)
    /\ baseCerts' = baseCerts \cup {BaseCertEvent(s, b, e)}
    /\ UNCHANGED <<transcriptSurfaces, challengeSurfaces,
                  canonicalCloses, canonicalAborts, sealedCerts>>

TranscriptSurfaceStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots :
    /\ BaseCertEvent(s, b, e) \in baseCerts
    /\ ~HasTranscriptSurface(s)
    /\ transcriptSurfaces' =
         transcriptSurfaces \cup {TranscriptSurfaceEvent(s, b, e, t)}
    /\ UNCHANGED <<baseCerts, challengeSurfaces, canonicalCloses,
                  canonicalAborts, sealedCerts>>

ChallengeSurfaceStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots,
     c \in ChallengeRoots :
    /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
    /\ ~HasChallengeSurface(s)
    /\ challengeSurfaces' =
         challengeSurfaces \cup {ChallengeSurfaceEvent(s, b, e, c)}
    /\ UNCHANGED <<baseCerts, transcriptSurfaces, canonicalCloses,
                  canonicalAborts, sealedCerts>>

CanonicalCloseStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots :
    /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
    /\ ChallengeSurfaceEvent(s, b, e, EmptyChallengeRoot) \in challengeSurfaces
    /\ ~HasCanonicalOutcome(s)
    /\ canonicalCloses' = canonicalCloses \cup {CanonicalCloseEvent(s, b, e, t)}
    /\ UNCHANGED <<baseCerts, transcriptSurfaces, challengeSurfaces,
                  canonicalAborts, sealedCerts>>

CanonicalAbortStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots,
     c \in ChallengeRoots \ {EmptyChallengeRoot} :
    /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
    /\ ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces
    /\ ~HasCanonicalOutcome(s)
    /\ canonicalAborts' =
         canonicalAborts \cup {CanonicalAbortEvent(s, b, e, t, c)}
    /\ UNCHANGED <<baseCerts, transcriptSurfaces, challengeSurfaces,
                  canonicalCloses, sealedCerts>>

SealStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots :
    /\ CanonicalCloseEvent(s, b, e, t) \in canonicalCloses
    /\ ~HasCanonicalAbort(s)
    /\ sealedCerts' = sealedCerts \cup {SealEvent(s, b, e)}
    /\ UNCHANGED <<baseCerts, transcriptSurfaces, challengeSurfaces,
                  canonicalCloses, canonicalAborts>>

Next ==
  \/ BaseCertifyStep
  \/ TranscriptSurfaceStep
  \/ ChallengeSurfaceStep
  \/ CanonicalCloseStep
  \/ CanonicalAbortStep
  \/ SealStep

TypeInvariant ==
  /\ baseCerts \subseteq BaseCertDomain
  /\ transcriptSurfaces \subseteq TranscriptSurfaceDomain
  /\ challengeSurfaces \subseteq ChallengeSurfaceDomain
  /\ canonicalCloses \subseteq CanonicalCloseDomain
  /\ canonicalAborts \subseteq CanonicalAbortDomain
  /\ sealedCerts \subseteq SealedCertDomain

NoDualBaseCerts ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs :
    /\ BaseCertEvent(s, b1, e1) \in baseCerts
    /\ BaseCertEvent(s, b2, e2) \in baseCerts
    => /\ b1 = b2
       /\ e1 = e2

NoDualTranscriptSurfaces ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs,
     t1 \in TranscriptRoots, t2 \in TranscriptRoots :
    /\ TranscriptSurfaceEvent(s, b1, e1, t1) \in transcriptSurfaces
    /\ TranscriptSurfaceEvent(s, b2, e2, t2) \in transcriptSurfaces
    => /\ b1 = b2
       /\ e1 = e2
       /\ t1 = t2

NoDualChallengeSurfaces ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs,
     c1 \in ChallengeRoots, c2 \in ChallengeRoots :
    /\ ChallengeSurfaceEvent(s, b1, e1, c1) \in challengeSurfaces
    /\ ChallengeSurfaceEvent(s, b2, e2, c2) \in challengeSurfaces
    => /\ b1 = b2
       /\ e1 = e2
       /\ c1 = c2

NoDualCanonicalCloses ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs,
     t1 \in TranscriptRoots, t2 \in TranscriptRoots :
    /\ CanonicalCloseEvent(s, b1, e1, t1) \in canonicalCloses
    /\ CanonicalCloseEvent(s, b2, e2, t2) \in canonicalCloses
    => /\ b1 = b2
       /\ e1 = e2
       /\ t1 = t2

NoDualCanonicalAborts ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs,
     t1 \in TranscriptRoots, t2 \in TranscriptRoots,
     c1 \in ChallengeRoots \ {EmptyChallengeRoot},
     c2 \in ChallengeRoots \ {EmptyChallengeRoot} :
    /\ CanonicalAbortEvent(s, b1, e1, t1, c1) \in canonicalAborts
    /\ CanonicalAbortEvent(s, b2, e2, t2, c2) \in canonicalAborts
    => /\ b1 = b2
       /\ e1 = e2
       /\ t1 = t2
       /\ c1 = c2

TranscriptAnchored ==
  \A s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots :
    TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
    => BaseCertEvent(s, b, e) \in baseCerts

ChallengeAnchored ==
  \A s \in Slots, b \in Blocks, e \in Epochs, c \in ChallengeRoots :
    ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces
    => \E t \in TranscriptRoots :
         TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces

CanonicalCloseAnchored ==
  \A s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots :
    CanonicalCloseEvent(s, b, e, t) \in canonicalCloses
    => /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
       /\ ChallengeSurfaceEvent(s, b, e, EmptyChallengeRoot) \in challengeSurfaces

CanonicalAbortAnchored ==
  \A s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots,
     c \in ChallengeRoots \ {EmptyChallengeRoot} :
    CanonicalAbortEvent(s, b, e, t, c) \in canonicalAborts
    => /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
       /\ ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces

SealedAnchored ==
  \A s \in Slots, b \in Blocks, e \in Epochs :
    SealEvent(s, b, e) \in sealedCerts
    => /\ \E t \in TranscriptRoots : CanonicalCloseEvent(s, b, e, t) \in canonicalCloses
       /\ ~HasCanonicalAbort(s)

CloseAbortExclusive ==
  \A s \in Slots, b1 \in Blocks, e1 \in Epochs, t1 \in TranscriptRoots,
     b2 \in Blocks, e2 \in Epochs, t2 \in TranscriptRoots,
     c \in ChallengeRoots \ {EmptyChallengeRoot} :
    /\ CanonicalCloseEvent(s, b1, e1, t1) \in canonicalCloses
    /\ CanonicalAbortEvent(s, b2, e2, t2, c) \in canonicalAborts
    => FALSE

Invariant ==
  /\ TypeInvariant
  /\ NoDualBaseCerts
  /\ NoDualTranscriptSurfaces
  /\ NoDualChallengeSurfaces
  /\ NoDualCanonicalCloses
  /\ NoDualCanonicalAborts
  /\ TranscriptAnchored
  /\ ChallengeAnchored
  /\ CanonicalCloseAnchored
  /\ CanonicalAbortAnchored
  /\ CloseAbortExclusive
  /\ SealedAnchored

BaseSafety ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs :
    /\ BaseCertEvent(s, b1, e1) \in baseCerts
    /\ BaseCertEvent(s, b2, e2) \in baseCerts
    => /\ b1 = b2
       /\ e1 = e2

CanonicalCloseSafety ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs,
     t1 \in TranscriptRoots, t2 \in TranscriptRoots :
    /\ CanonicalCloseEvent(s, b1, e1, t1) \in canonicalCloses
    /\ CanonicalCloseEvent(s, b2, e2, t2) \in canonicalCloses
    => /\ b1 = b2
       /\ e1 = e2
       /\ t1 = t2

SealedSafety ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs :
    /\ SealEvent(s, b1, e1) \in sealedCerts
    /\ SealEvent(s, b2, e2) \in sealedCerts
    => /\ b1 = b2
       /\ e1 = e2

AbortDominatesSealed ==
  \A s \in Slots, b \in Blocks, e \in Epochs :
    HasCanonicalAbort(s) => SealEvent(s, b, e) \notin sealedCerts

Spec == Init /\ [][Next]_vars

THEOREM InvariantImpliesBaseSafety == Invariant => BaseSafety
  BY SMTT(50)
     DEF Invariant, BaseSafety, NoDualBaseCerts

THEOREM InvariantImpliesCanonicalCloseSafety == Invariant => CanonicalCloseSafety
  BY SMTT(60)
     DEF Invariant, CanonicalCloseSafety, NoDualCanonicalCloses

THEOREM InvariantImpliesCloseAbortExclusive == Invariant => CloseAbortExclusive
  BY SMTT(20)
     DEF Invariant, CloseAbortExclusive

THEOREM InvariantImpliesSealedSafety == Invariant => SealedSafety
  BY SMTT(60), InvariantImpliesCanonicalCloseSafety
     DEF Invariant, SealedSafety, SealedAnchored, CanonicalCloseSafety

THEOREM InvariantImpliesAbortDominatesSealed == Invariant => AbortDominatesSealed
  BY SMTT(60)
     DEF Invariant, AbortDominatesSealed, SealedAnchored

====

Asymptote.tla

Repository path: docs/architecture/protocols/aft/formal/Asymptote.tla

---- MODULE Asymptote ----
EXTENDS Naturals, FiniteSets, TLC, TLAPS

CONSTANT Validators, Blocks, Slots, Epochs, ValidatorQuorum,
          TranscriptRoots, ChallengeRoots, EmptyChallengeRoot

ASSUME EmptyChallengeRoot \in ChallengeRoots
ASSUME ValidatorQuorumIntersection ==
  \A S, T \in SUBSET Validators :
    /\ Cardinality(S) >= ValidatorQuorum
    /\ Cardinality(T) >= ValidatorQuorum
    => S \cap T # {}

CollapsePending == 0
CollapseBase == 1
CollapseObservation == 2
CollapseAbort == 3
CollapseSealed == 4

CollapseStates ==
  {CollapsePending, CollapseBase, CollapseObservation, CollapseAbort, CollapseSealed}

VARIABLES validatorVotes, baseCerts, transcriptSurfaces, challengeSurfaces,
          canonicalCloses, canonicalAborts, sealedFinal, collapseState

vars ==
  <<validatorVotes, baseCerts, transcriptSurfaces, challengeSurfaces,
    canonicalCloses, canonicalAborts, sealedFinal, collapseState>>

ValidatorVoteEvent(v, s, b, e) == <<v, s, b, e>>
BaseCertEvent(s, b, e, q) == <<s, b, e, q>>
TranscriptSurfaceEvent(s, b, e, t) == <<s, b, e, t>>
ChallengeSurfaceEvent(s, b, e, c) == <<s, b, e, c>>
CanonicalCloseEvent(s, b, e, t) == <<s, b, e, t>>
CanonicalAbortEvent(s, b, e, t, c) == <<s, b, e, t, c>>
SealEvent(s, b, e) == <<s, b, e>>

ValidatorVoteDomain == Validators \X Slots \X Blocks \X Epochs
BaseCertDomain == Slots \X Blocks \X Epochs \X (SUBSET Validators)
TranscriptSurfaceDomain == Slots \X Blocks \X Epochs \X TranscriptRoots
ChallengeSurfaceDomain == Slots \X Blocks \X Epochs \X ChallengeRoots
CanonicalCloseDomain == Slots \X Blocks \X Epochs \X TranscriptRoots
CanonicalAbortDomain ==
  Slots \X Blocks \X Epochs \X TranscriptRoots \X (ChallengeRoots \ {EmptyChallengeRoot})
SealedCertDomain == Slots \X Blocks \X Epochs

Init ==
  /\ validatorVotes = {}
  /\ baseCerts = {}
  /\ transcriptSurfaces = {}
  /\ challengeSurfaces = {}
  /\ canonicalCloses = {}
  /\ canonicalAborts = {}
  /\ sealedFinal = {}
  /\ collapseState = [s \in Slots |-> CollapsePending]

HasValidatorVote(v, s) ==
  \E b \in Blocks, e \in Epochs : ValidatorVoteEvent(v, s, b, e) \in validatorVotes

HasBaseCert(s) ==
  \E b \in Blocks, e \in Epochs, q \in SUBSET Validators :
    BaseCertEvent(s, b, e, q) \in baseCerts

HasTranscriptSurface(s) ==
  \E b \in Blocks, e \in Epochs, t \in TranscriptRoots :
    TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces

HasChallengeSurface(s) ==
  \E b \in Blocks, e \in Epochs, c \in ChallengeRoots :
    ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces

HasCanonicalOutcome(s) ==
  \/ \E b \in Blocks, e \in Epochs, t \in TranscriptRoots :
       CanonicalCloseEvent(s, b, e, t) \in canonicalCloses
  \/ \E b \in Blocks, e \in Epochs, t \in TranscriptRoots,
        c \in ChallengeRoots \ {EmptyChallengeRoot} :
       CanonicalAbortEvent(s, b, e, t, c) \in canonicalAborts

HasCanonicalAbort(s) ==
  \E b \in Blocks, e \in Epochs, t \in TranscriptRoots,
    c \in ChallengeRoots \ {EmptyChallengeRoot} :
    CanonicalAbortEvent(s, b, e, t, c) \in canonicalAborts

ValidatorVoteStep ==
  \E v \in Validators, s \in Slots, b \in Blocks, e \in Epochs :
    /\ ~HasValidatorVote(v, s)
    /\ validatorVotes' = validatorVotes \cup {ValidatorVoteEvent(v, s, b, e)}
    /\ UNCHANGED <<baseCerts, transcriptSurfaces, challengeSurfaces,
                  canonicalCloses, canonicalAborts, sealedFinal, collapseState>>

EligibleValidators(s, b, e) ==
  {v \in Validators : ValidatorVoteEvent(v, s, b, e) \in validatorVotes}

BaseFinalizeStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs, q \in SUBSET Validators :
    /\ q = EligibleValidators(s, b, e)
    /\ Cardinality(q) >= ValidatorQuorum
    /\ baseCerts' = baseCerts \cup {BaseCertEvent(s, b, e, q)}
    /\ collapseState' = [collapseState EXCEPT ![s] = CollapseBase]
    /\ UNCHANGED <<validatorVotes, transcriptSurfaces, challengeSurfaces,
                  canonicalCloses, canonicalAborts, sealedFinal>>

TranscriptSurfaceStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs, q \in SUBSET Validators,
     t \in TranscriptRoots :
    /\ BaseCertEvent(s, b, e, q) \in baseCerts
    /\ collapseState[s] \in {CollapseBase, CollapseObservation}
    /\ ~HasTranscriptSurface(s)
    /\ transcriptSurfaces' =
         transcriptSurfaces \cup {TranscriptSurfaceEvent(s, b, e, t)}
    /\ collapseState' = [collapseState EXCEPT ![s] = CollapseObservation]
    /\ UNCHANGED <<validatorVotes, baseCerts, challengeSurfaces,
                  canonicalCloses, canonicalAborts, sealedFinal>>

ChallengeSurfaceStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots,
     c \in ChallengeRoots :
    /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
    /\ collapseState[s] = CollapseObservation
    /\ ~HasChallengeSurface(s)
    /\ challengeSurfaces' =
         challengeSurfaces \cup {ChallengeSurfaceEvent(s, b, e, c)}
    /\ collapseState' = [collapseState EXCEPT ![s] = CollapseObservation]
    /\ UNCHANGED <<validatorVotes, baseCerts, transcriptSurfaces,
                  canonicalCloses, canonicalAborts, sealedFinal>>

CanonicalCloseStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots :
    /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
    /\ ChallengeSurfaceEvent(s, b, e, EmptyChallengeRoot) \in challengeSurfaces
    /\ collapseState[s] = CollapseObservation
    /\ ~HasCanonicalOutcome(s)
    /\ canonicalCloses' = canonicalCloses \cup {CanonicalCloseEvent(s, b, e, t)}
    /\ UNCHANGED <<validatorVotes, baseCerts, transcriptSurfaces,
                  challengeSurfaces, canonicalAborts, sealedFinal, collapseState>>

CanonicalAbortStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots,
     c \in ChallengeRoots \ {EmptyChallengeRoot} :
    /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
    /\ ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces
    /\ ~HasCanonicalOutcome(s)
    /\ canonicalAborts' =
         canonicalAborts \cup {CanonicalAbortEvent(s, b, e, t, c)}
    /\ collapseState' = [collapseState EXCEPT ![s] = CollapseAbort]
    /\ UNCHANGED <<validatorVotes, baseCerts, transcriptSurfaces,
                  challengeSurfaces, canonicalCloses, sealedFinal>>

SealStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots :
    /\ CanonicalCloseEvent(s, b, e, t) \in canonicalCloses
    /\ ~HasCanonicalAbort(s)
    /\ sealedFinal' = sealedFinal \cup {SealEvent(s, b, e)}
    /\ collapseState' = [collapseState EXCEPT ![s] = CollapseSealed]
    /\ UNCHANGED <<validatorVotes, baseCerts, transcriptSurfaces,
                  challengeSurfaces, canonicalCloses, canonicalAborts>>

StutterStep == UNCHANGED vars

Next ==
  \/ ValidatorVoteStep
  \/ BaseFinalizeStep
  \/ TranscriptSurfaceStep
  \/ ChallengeSurfaceStep
  \/ CanonicalCloseStep
  \/ CanonicalAbortStep
  \/ SealStep
  \/ StutterStep

TypeInvariant ==
  /\ validatorVotes \subseteq ValidatorVoteDomain
  /\ baseCerts \subseteq BaseCertDomain
  /\ transcriptSurfaces \subseteq TranscriptSurfaceDomain
  /\ challengeSurfaces \subseteq ChallengeSurfaceDomain
  /\ canonicalCloses \subseteq CanonicalCloseDomain
  /\ canonicalAborts \subseteq CanonicalAbortDomain
  /\ sealedFinal \subseteq SealedCertDomain
  /\ collapseState \in [Slots -> CollapseStates]

NoDualValidatorVotes ==
  \A v \in Validators, s \in Slots, b1 \in Blocks, b2 \in Blocks,
     e1 \in Epochs, e2 \in Epochs :
    /\ ValidatorVoteEvent(v, s, b1, e1) \in validatorVotes
    /\ ValidatorVoteEvent(v, s, b2, e2) \in validatorVotes
    => /\ b1 = b2
       /\ e1 = e2

NoDualTranscriptSurfaces ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs,
     t1 \in TranscriptRoots, t2 \in TranscriptRoots :
    /\ TranscriptSurfaceEvent(s, b1, e1, t1) \in transcriptSurfaces
    /\ TranscriptSurfaceEvent(s, b2, e2, t2) \in transcriptSurfaces
    => /\ b1 = b2
       /\ e1 = e2
       /\ t1 = t2

NoDualChallengeSurfaces ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs,
     c1 \in ChallengeRoots, c2 \in ChallengeRoots :
    /\ ChallengeSurfaceEvent(s, b1, e1, c1) \in challengeSurfaces
    /\ ChallengeSurfaceEvent(s, b2, e2, c2) \in challengeSurfaces
    => /\ b1 = b2
       /\ e1 = e2
       /\ c1 = c2

BaseCertSoundness ==
  \A s \in Slots, b \in Blocks, e \in Epochs, q \in SUBSET Validators :
    BaseCertEvent(s, b, e, q) \in baseCerts
    => /\ Cardinality(q) >= ValidatorQuorum
       /\ \A v \in q : ValidatorVoteEvent(v, s, b, e) \in validatorVotes

TranscriptAnchored ==
  \A s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots :
    TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
    => \E q \in SUBSET Validators : BaseCertEvent(s, b, e, q) \in baseCerts

ChallengeAnchored ==
  \A s \in Slots, b \in Blocks, e \in Epochs, c \in ChallengeRoots :
    ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces
    => \E t \in TranscriptRoots :
         TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces

CanonicalCloseAnchored ==
  \A s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots :
    CanonicalCloseEvent(s, b, e, t) \in canonicalCloses
    => /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
       /\ ChallengeSurfaceEvent(s, b, e, EmptyChallengeRoot) \in challengeSurfaces

CanonicalAbortAnchored ==
  \A s \in Slots, b \in Blocks, e \in Epochs, t \in TranscriptRoots,
     c \in ChallengeRoots \ {EmptyChallengeRoot} :
    CanonicalAbortEvent(s, b, e, t, c) \in canonicalAborts
    => /\ TranscriptSurfaceEvent(s, b, e, t) \in transcriptSurfaces
       /\ ChallengeSurfaceEvent(s, b, e, c) \in challengeSurfaces

SealedAnchored ==
  \A s \in Slots, b \in Blocks, e \in Epochs :
    SealEvent(s, b, e) \in sealedFinal
    => /\ \E t \in TranscriptRoots : CanonicalCloseEvent(s, b, e, t) \in canonicalCloses
       /\ ~HasCanonicalAbort(s)

BaseSafety ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs,
     q1 \in SUBSET Validators, q2 \in SUBSET Validators :
    /\ BaseCertEvent(s, b1, e1, q1) \in baseCerts
    /\ BaseCertEvent(s, b2, e2, q2) \in baseCerts
    => /\ b1 = b2
       /\ e1 = e2

CanonicalCloseSafety ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs,
     t1 \in TranscriptRoots, t2 \in TranscriptRoots :
    /\ CanonicalCloseEvent(s, b1, e1, t1) \in canonicalCloses
    /\ CanonicalCloseEvent(s, b2, e2, t2) \in canonicalCloses
    => /\ b1 = b2
       /\ e1 = e2
       /\ t1 = t2

AbortDominatesClose ==
  \A s \in Slots :
    HasCanonicalAbort(s)
    => ~(\E b \in Blocks, e \in Epochs, t \in TranscriptRoots :
           CanonicalCloseEvent(s, b, e, t) \in canonicalCloses)

SealedSafety ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs :
    /\ SealEvent(s, b1, e1) \in sealedFinal
    /\ SealEvent(s, b2, e2) \in sealedFinal
    => /\ b1 = b2
       /\ e1 = e2

AbortDominatesSealed ==
  \A s \in Slots, b \in Blocks, e \in Epochs :
    HasCanonicalAbort(s) => SealEvent(s, b, e) \notin sealedFinal

MonotoneCollapse ==
  /\ \A s \in Slots :
       collapseState[s] = CollapseSealed => \E b \in Blocks, e \in Epochs :
         SealEvent(s, b, e) \in sealedFinal
  /\ \A s \in Slots :
       collapseState[s] = CollapseAbort => HasCanonicalAbort(s)

Spec == Init /\ [][Next]_vars

====

NestedGuardian

Witness-augmented layered-threshold model and proof surface.

NestedGuardianProof.tla

Repository path: docs/architecture/protocols/aft/formal/nested_guardian/NestedGuardianProof.tla

---- MODULE NestedGuardianProof ----
EXTENDS Naturals, FiniteSets, TLAPS

CONSTANT Validators, Witnesses, Blocks, Slots, Epochs, QuorumSize, MaxReassignmentDepth,
         InitialWitness

ASSUME InitialWitnessInWitnesses == InitialWitness \in Witnesses
ASSUME MaxReassignmentDepthIsNat == MaxReassignmentDepth \in Nat

ASSUME QuorumIntersection ==
  \A S, T \in SUBSET Validators :
    /\ Cardinality(S) >= QuorumSize
    /\ Cardinality(T) >= QuorumSize
    => S \cap T # {}

VARIABLES votes, witnessCerts, certs, assignedWitness, reassignmentDepth

vars == <<votes, witnessCerts, certs, assignedWitness, reassignmentDepth>>

VoteDomain == Validators \X Slots \X Blocks \X Epochs
WitnessCertDomain == Slots \X Blocks \X Epochs \X Witnesses
CertDomain == Slots \X Blocks \X Epochs \X (SUBSET Validators)

Init ==
  /\ votes = {}
  /\ witnessCerts = {}
  /\ certs = {}
  /\ assignedWitness = [s \in Slots |-> InitialWitness]
  /\ reassignmentDepth = [s \in Slots |-> 0]

HasVote(v, s) ==
  \E b \in Blocks, e \in Epochs : <<v, s, b, e>> \in votes

HasWitnessCert(s) ==
  \E b \in Blocks, e \in Epochs, w \in Witnesses : <<s, b, e, w>> \in witnessCerts

IssueWitnessStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs :
    /\ ~HasWitnessCert(s)
    /\ witnessCerts' = witnessCerts \cup {<<s, b, e, assignedWitness[s]>>}
    /\ UNCHANGED <<votes, certs, assignedWitness, reassignmentDepth>>

ReassignWitnessStep ==
  \E s \in Slots, w \in Witnesses :
    /\ w # assignedWitness[s]
    /\ reassignmentDepth[s] < MaxReassignmentDepth
    /\ assignedWitness' = [assignedWitness EXCEPT ![s] = w]
    /\ reassignmentDepth' = [reassignmentDepth EXCEPT ![s] = @ + 1]
    /\ UNCHANGED <<votes, witnessCerts, certs>>

VoteStep ==
  \E v \in Validators, s \in Slots, b \in Blocks, e \in Epochs :
    /\ ~HasVote(v, s)
    /\ <<s, b, e, assignedWitness[s]>> \in witnessCerts
    /\ votes' = votes \cup {<<v, s, b, e>>}
    /\ UNCHANGED <<witnessCerts, certs, assignedWitness, reassignmentDepth>>

CertifyStep ==
  \E s \in Slots, b \in Blocks, e \in Epochs, Q \in SUBSET Validators :
    /\ Cardinality(Q) >= QuorumSize
    /\ <<s, b, e, assignedWitness[s]>> \in witnessCerts
    /\ \A v \in Q : <<v, s, b, e>> \in votes
    /\ certs' = certs \cup {<<s, b, e, Q>>}
    /\ UNCHANGED <<votes, witnessCerts, assignedWitness, reassignmentDepth>>

Next == IssueWitnessStep \/ ReassignWitnessStep \/ VoteStep \/ CertifyStep

TypeInvariant ==
  /\ votes \subseteq VoteDomain
  /\ witnessCerts \subseteq WitnessCertDomain
  /\ certs \subseteq CertDomain
  /\ assignedWitness \in [Slots -> Witnesses]
  /\ reassignmentDepth \in [Slots -> 0..MaxReassignmentDepth]

WitnessAssignmentSoundness ==
  \A s \in Slots : reassignmentDepth[s] <= MaxReassignmentDepth

NoDualVotes ==
  \A v \in Validators, s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs :
    /\ <<v, s, b1, e1>> \in votes
    /\ <<v, s, b2, e2>> \in votes
    => /\ b1 = b2
       /\ e1 = e2

WitnessCertificatesStayAssigned ==
  \A s \in Slots, b \in Blocks, e \in Epochs, w \in Witnesses :
    <<s, b, e, w>> \in witnessCerts
    => assignedWitness[s] = w \/ reassignmentDepth[s] > 0

CertSoundness ==
  \A s \in Slots, b \in Blocks, e \in Epochs, Q \in SUBSET Validators :
    <<s, b, e, Q>> \in certs
    => /\ Cardinality(Q) >= QuorumSize
       /\ \A v \in Q : <<v, s, b, e>> \in votes

Invariant ==
  /\ TypeInvariant
  /\ WitnessAssignmentSoundness
  /\ NoDualVotes
  /\ WitnessCertificatesStayAssigned
  /\ CertSoundness

Safety ==
  \A s \in Slots,
     b1 \in Blocks,
     b2 \in Blocks,
     e1 \in Epochs,
     e2 \in Epochs,
     Q1 \in SUBSET Validators,
     Q2 \in SUBSET Validators :
    /\ <<s, b1, e1, Q1>> \in certs
    /\ <<s, b2, e2, Q2>> \in certs
    => /\ b1 = b2
       /\ e1 = e2

Spec == Init /\ [][Next]_vars

THEOREM InitImpliesTypeInvariant == Init => TypeInvariant
  BY SMTT(30), InitialWitnessInWitnesses, MaxReassignmentDepthIsNat DEF Init, TypeInvariant, VoteDomain,
                WitnessCertDomain, CertDomain

THEOREM InitImpliesWitnessAssignmentSoundness == Init => WitnessAssignmentSoundness
  BY SMTT(30), MaxReassignmentDepthIsNat DEF Init, WitnessAssignmentSoundness

THEOREM InitImpliesNoDualVotes == Init => NoDualVotes
  BY DEF Init, NoDualVotes

THEOREM InitImpliesWitnessCertificatesStayAssigned == Init => WitnessCertificatesStayAssigned
  BY DEF Init, WitnessCertificatesStayAssigned

THEOREM InitImpliesCertSoundness == Init => CertSoundness
  BY DEF Init, CertSoundness

THEOREM InitImpliesInvariant == Init => Invariant
  BY InitImpliesTypeInvariant, InitImpliesWitnessAssignmentSoundness,
     InitImpliesNoDualVotes, InitImpliesWitnessCertificatesStayAssigned,
     InitImpliesCertSoundness DEF Invariant

THEOREM IssueWitnessPreservesInvariant == Invariant /\ IssueWitnessStep => Invariant'
  BY SMTT(30) DEF Invariant, TypeInvariant, WitnessAssignmentSoundness, NoDualVotes,
                WitnessCertificatesStayAssigned, CertSoundness, IssueWitnessStep,
                HasWitnessCert, WitnessCertDomain

THEOREM ReassignWitnessPreservesInvariant == Invariant /\ ReassignWitnessStep => Invariant'
  BY SMTT(30), MaxReassignmentDepthIsNat DEF Invariant, TypeInvariant, WitnessAssignmentSoundness, NoDualVotes,
                WitnessCertificatesStayAssigned, CertSoundness, ReassignWitnessStep

THEOREM VotePreservesInvariant == Invariant /\ VoteStep => Invariant'
  BY SMTT(30) DEF Invariant, TypeInvariant, WitnessAssignmentSoundness, NoDualVotes,
                WitnessCertificatesStayAssigned, CertSoundness, VoteStep, HasVote,
                VoteDomain

THEOREM CertifyPreservesInvariant == Invariant /\ CertifyStep => Invariant'
  BY SMTT(30) DEF Invariant, TypeInvariant, WitnessAssignmentSoundness, NoDualVotes,
                WitnessCertificatesStayAssigned, CertSoundness, CertifyStep, CertDomain

THEOREM StepPreservesInvariant == Invariant /\ Next => Invariant'
  BY IssueWitnessPreservesInvariant, ReassignWitnessPreservesInvariant,
     VotePreservesInvariant, CertifyPreservesInvariant DEF Next

THEOREM StutterPreservesTypeInvariant ==
  TypeInvariant /\ UNCHANGED vars => TypeInvariant'
  BY DEF TypeInvariant, vars

THEOREM StutterPreservesWitnessAssignmentSoundness ==
  WitnessAssignmentSoundness /\ UNCHANGED vars => WitnessAssignmentSoundness'
  BY DEF WitnessAssignmentSoundness, vars

THEOREM StutterPreservesNoDualVotes ==
  NoDualVotes /\ UNCHANGED vars => NoDualVotes'
  BY DEF NoDualVotes, vars

THEOREM StutterPreservesWitnessCertificatesStayAssigned ==
  WitnessCertificatesStayAssigned /\ UNCHANGED vars => WitnessCertificatesStayAssigned'
  BY DEF WitnessCertificatesStayAssigned, vars

THEOREM StutterPreservesCertSoundness ==
  CertSoundness /\ UNCHANGED vars => CertSoundness'
  BY DEF CertSoundness, vars

THEOREM StutterPreservesInvariant == Invariant /\ UNCHANGED vars => Invariant'
  BY StutterPreservesTypeInvariant, StutterPreservesWitnessAssignmentSoundness,
     StutterPreservesNoDualVotes, StutterPreservesWitnessCertificatesStayAssigned,
     StutterPreservesCertSoundness DEF Invariant

THEOREM NextPreservesInvariant == Invariant /\ [Next]_vars => Invariant'
  BY StepPreservesInvariant, StutterPreservesInvariant DEF vars

THEOREM QuorumCertificatesIntersect ==
  \A s \in Slots,
     b1 \in Blocks,
     b2 \in Blocks,
     e1 \in Epochs,
     e2 \in Epochs,
     Q1 \in SUBSET Validators,
     Q2 \in SUBSET Validators :
    /\ Invariant
    /\ <<s, b1, e1, Q1>> \in certs
    /\ <<s, b2, e2, Q2>> \in certs
    => Q1 \cap Q2 # {}
  BY SMTT(60), QuorumIntersection DEF Invariant, CertSoundness

THEOREM InvariantImpliesSafety == Invariant => Safety
  BY SMTT(60), QuorumCertificatesIntersect DEF Invariant, Safety, NoDualVotes,
                CertSoundness

====

NestedGuardian.tla

Repository path: docs/architecture/protocols/aft/formal/nested_guardian/NestedGuardian.tla

---- MODULE NestedGuardian ----
EXTENDS Naturals, FiniteSets, TLC, TLAPS

CONSTANT Validators, Witnesses, Blocks, Slots, Epochs, QuorumSize, MaxReassignmentDepth,
         InitialEpoch, InitialWitness

ASSUME InitialEpochInEpochs == InitialEpoch \in Epochs
ASSUME InitialWitnessInWitnesses == InitialWitness \in Witnesses

ASSUME QuorumIntersection ==
  \A S, T \in SUBSET Validators :
    /\ Cardinality(S) >= QuorumSize
    /\ Cardinality(T) >= QuorumSize
    => S \cap T # {}

VARIABLES votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, witnessOnline,
          witnessCheckpoint, assignedWitness, reassignmentDepth

vars == <<votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady,
          witnessOnline, witnessCheckpoint, assignedWitness, reassignmentDepth>>

CheckpointLevels == 0..2

VoteEvent(v, s, b, e) == <<v, s, b, e>>
WitnessEvent(w, s, b, e) == <<w, s, b, e>>
Finalization(s, b, e) == <<s, b, e>>

VoteDomain == {VoteEvent(v, s, b, e) : v \in Validators, s \in Slots, b \in Blocks, e \in Epochs}
WitnessDomain == {WitnessEvent(w, s, b, e) : w \in Witnesses, s \in Slots, b \in Blocks, e \in Epochs}
FinalizationDomain == {Finalization(s, b, e) : s \in Slots, b \in Blocks, e \in Epochs}

Init ==
  /\ votes = {}
  /\ witnessCerts = {}
  /\ finalized = {}
  /\ finalizerSets = [f \in FinalizationDomain |-> {}]
  /\ registryEpoch = [v \in Validators |-> InitialEpoch]
  /\ guardianReady = [v \in Validators |-> TRUE]
  /\ witnessOnline = [w \in Witnesses |-> TRUE]
  /\ witnessCheckpoint = [w \in Witnesses |-> 1]
  /\ assignedWitness = [s \in Slots |-> InitialWitness]
  /\ reassignmentDepth = [s \in Slots |-> 0]

HasVote(v, s) ==
  \E b \in Blocks, e \in Epochs : VoteEvent(v, s, b, e) \in votes

HasWitnessCert(w, s) ==
  \E b \in Blocks, e \in Epochs : WitnessEvent(w, s, b, e) \in witnessCerts

CanIssueWitness(w, s, b, e) ==
  /\ w \in Witnesses
  /\ s \in Slots
  /\ b \in Blocks
  /\ e \in Epochs
  /\ witnessOnline[w]
  /\ witnessCheckpoint[w] > 0
  /\ assignedWitness[s] = w
  /\ ~HasWitnessCert(w, s)

IssueWitness(w, s, b, e) ==
  /\ CanIssueWitness(w, s, b, e)
  /\ witnessCerts' = witnessCerts \cup {WitnessEvent(w, s, b, e)}
  /\ UNCHANGED <<votes, finalized, finalizerSets, registryEpoch, guardianReady, witnessOnline,
                witnessCheckpoint, assignedWitness, reassignmentDepth>>

CanReassign(s, w) ==
  /\ s \in Slots
  /\ w \in Witnesses
  /\ w # assignedWitness[s]
  /\ ~witnessOnline[assignedWitness[s]]
  /\ reassignmentDepth[s] < MaxReassignmentDepth

ReassignWitness(s, w) ==
  /\ CanReassign(s, w)
  /\ assignedWitness' = [assignedWitness EXCEPT ![s] = w]
  /\ reassignmentDepth' = [reassignmentDepth EXCEPT ![s] = @ + 1]
  /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady,
                witnessOnline, witnessCheckpoint>>

CanVote(v, s, b, e) ==
  /\ v \in Validators
  /\ s \in Slots
  /\ b \in Blocks
  /\ e \in Epochs
  /\ guardianReady[v]
  /\ registryEpoch[v] = e
  /\ ~HasVote(v, s)
  /\ WitnessEvent(assignedWitness[s], s, b, e) \in witnessCerts

Vote(v, s, b, e) ==
  /\ CanVote(v, s, b, e)
  /\ votes' = votes \cup {VoteEvent(v, s, b, e)}
  /\ UNCHANGED <<witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, witnessOnline,
                witnessCheckpoint, assignedWitness, reassignmentDepth>>

EligibleVoters(s, b, e) ==
  {v \in Validators :
      /\ VoteEvent(v, s, b, e) \in votes
      /\ guardianReady[v]
      /\ registryEpoch[v] = e
      /\ WitnessEvent(assignedWitness[s], s, b, e) \in witnessCerts}

CanFinalize(s, b, e) ==
  /\ s \in Slots
  /\ b \in Blocks
  /\ e \in Epochs
  /\ Cardinality(EligibleVoters(s, b, e)) >= QuorumSize

Finalize(s, b, e) ==
  /\ CanFinalize(s, b, e)
  /\ finalized' = finalized \cup {Finalization(s, b, e)}
  /\ finalizerSets' = [finalizerSets EXCEPT ![Finalization(s, b, e)] = EligibleVoters(s, b, e)]
  /\ UNCHANGED <<votes, witnessCerts, registryEpoch, guardianReady, witnessOnline,
                witnessCheckpoint, assignedWitness, reassignmentDepth>>

AdoptEpoch(v, e) ==
  /\ v \in Validators
  /\ e \in Epochs
  /\ e >= registryEpoch[v]
  /\ registryEpoch' = [registryEpoch EXCEPT ![v] = e]
  /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, guardianReady, witnessOnline,
                witnessCheckpoint, assignedWitness, reassignmentDepth>>

RegistryRollback(v, e) ==
  /\ v \in Validators
  /\ e \in Epochs
  /\ e < registryEpoch[v]
  /\ registryEpoch' = [registryEpoch EXCEPT ![v] = e]
  /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, guardianReady, witnessOnline,
                witnessCheckpoint, assignedWitness, reassignmentDepth>>

GuardianOutage(v) ==
  /\ v \in Validators
  /\ guardianReady[v]
  /\ guardianReady' = [guardianReady EXCEPT ![v] = FALSE]
  /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, registryEpoch, witnessOnline,
                witnessCheckpoint, assignedWitness, reassignmentDepth>>

WitnessOutage(w) ==
  /\ w \in Witnesses
  /\ witnessOnline[w]
  /\ witnessOnline' = [witnessOnline EXCEPT ![w] = FALSE]
  /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady,
                witnessCheckpoint, assignedWitness, reassignmentDepth>>

WitnessRecovery(w) ==
  /\ w \in Witnesses
  /\ ~witnessOnline[w]
  /\ witnessOnline' = [witnessOnline EXCEPT ![w] = TRUE]
  /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady,
                witnessCheckpoint, assignedWitness, reassignmentDepth>>

AdvanceWitnessCheckpoint(w, level) ==
  /\ w \in Witnesses
  /\ level \in CheckpointLevels
  /\ level > witnessCheckpoint[w]
  /\ witnessCheckpoint' = [witnessCheckpoint EXCEPT ![w] = level]
  /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady,
                witnessOnline, assignedWitness, reassignmentDepth>>

WitnessCheckpointRollback(w, level) ==
  /\ w \in Witnesses
  /\ level \in CheckpointLevels
  /\ level < witnessCheckpoint[w]
  /\ witnessCheckpoint' = [witnessCheckpoint EXCEPT ![w] = level]
  /\ UNCHANGED <<votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady,
                witnessOnline, assignedWitness, reassignmentDepth>>

Next ==
  \/ \E w \in Witnesses, s \in Slots, b \in Blocks, e \in Epochs : IssueWitness(w, s, b, e)
  \/ \E s \in Slots, w \in Witnesses : ReassignWitness(s, w)
  \/ \E v \in Validators, s \in Slots, b \in Blocks, e \in Epochs : Vote(v, s, b, e)
  \/ \E s \in Slots, b \in Blocks, e \in Epochs : Finalize(s, b, e)
  \/ \E v \in Validators, e \in Epochs : AdoptEpoch(v, e)
  \/ \E v \in Validators, e \in Epochs : RegistryRollback(v, e)
  \/ \E v \in Validators : GuardianOutage(v)
  \/ \E w \in Witnesses : WitnessOutage(w)
  \/ \E w \in Witnesses : WitnessRecovery(w)
  \/ \E w \in Witnesses, level \in CheckpointLevels : AdvanceWitnessCheckpoint(w, level)
  \/ \E w \in Witnesses, level \in CheckpointLevels : WitnessCheckpointRollback(w, level)

TypeInvariant ==
  /\ votes \subseteq VoteDomain
  /\ witnessCerts \subseteq WitnessDomain
  /\ finalized \subseteq FinalizationDomain
  /\ finalizerSets \in [FinalizationDomain -> SUBSET Validators]
  /\ registryEpoch \in [Validators -> Epochs]
  /\ guardianReady \in [Validators -> BOOLEAN]
  /\ witnessOnline \in [Witnesses -> BOOLEAN]
  /\ witnessCheckpoint \in [Witnesses -> CheckpointLevels]
  /\ assignedWitness \in [Slots -> Witnesses]
  /\ reassignmentDepth \in [Slots -> 0..MaxReassignmentDepth]

WitnessAssignmentSoundness ==
  \A s \in Slots :
    reassignmentDepth[s] <= MaxReassignmentDepth

NoDualVotes ==
  \A v \in Validators, s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs :
    /\ VoteEvent(v, s, b1, e1) \in votes
    /\ VoteEvent(v, s, b2, e2) \in votes
    => /\ b1 = b2
       /\ e1 = e2

WitnessCertificatesStayAssigned ==
  \A w \in Witnesses, s \in Slots, b \in Blocks, e \in Epochs :
    WitnessEvent(w, s, b, e) \in witnessCerts
    => assignedWitness[s] = w \/ reassignmentDepth[s] > 0

FinalizationWitnessSoundness ==
  \A s \in Slots, b \in Blocks, e \in Epochs :
    Finalization(s, b, e) \in finalized
    => /\ Cardinality(finalizerSets[Finalization(s, b, e)]) >= QuorumSize
       /\ \A v \in finalizerSets[Finalization(s, b, e)] :
            VoteEvent(v, s, b, e) \in votes

Invariant ==
  /\ TypeInvariant
  /\ WitnessAssignmentSoundness
  /\ NoDualVotes
  /\ WitnessCertificatesStayAssigned
  /\ FinalizationWitnessSoundness

Safety ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs :
    /\ Finalization(s, b1, e1) \in finalized
    /\ Finalization(s, b2, e2) \in finalized
    => b1 = b2

Spec ==
  Init /\ [][Next]_vars

THEOREM OneInCheckpointLevels == 1 \in CheckpointLevels
  BY SMT DEF CheckpointLevels

THEOREM InitImpliesInvariant == Init => Invariant
PROOF
<1>1. Init => TypeInvariant
  BY SMT, InitialEpochInEpochs, InitialWitnessInWitnesses, OneInCheckpointLevels
     DEF Init, TypeInvariant, VoteDomain, WitnessDomain, FinalizationDomain
<1>2. Init => WitnessAssignmentSoundness
  BY DEF Init, WitnessAssignmentSoundness
<1>3. Init => NoDualVotes
  BY DEF Init, NoDualVotes
<1>4. Init => WitnessCertificatesStayAssigned
  BY DEF Init, WitnessCertificatesStayAssigned
<1>5. Init => FinalizationWitnessSoundness
  BY DEF Init, FinalizationWitnessSoundness
<1>6. QED
  BY <1>1, <1>2, <1>3, <1>4, <1>5 DEF Invariant

THEOREM StepPreservesInvariant == Invariant /\ Next => Invariant'
  BY SMTT(30) DEF Invariant, TypeInvariant, WitnessAssignmentSoundness, NoDualVotes,
             WitnessCertificatesStayAssigned, FinalizationWitnessSoundness, Next,
             IssueWitness, ReassignWitness, Vote, Finalize, AdoptEpoch,
             RegistryRollback, GuardianOutage, WitnessOutage, WitnessRecovery,
             AdvanceWitnessCheckpoint, WitnessCheckpointRollback, CanIssueWitness,
             CanVote, HasVote, CanFinalize, EligibleVoters, VoteEvent,
             WitnessEvent, Finalization, VoteDomain, WitnessDomain, FinalizationDomain

THEOREM StutterPreservesInvariant == Invariant /\ UNCHANGED vars => Invariant'
  BY SMT DEF Invariant, vars

THEOREM NextPreservesInvariant == Invariant /\ [Next]_vars => Invariant'
  BY SMT, StepPreservesInvariant, StutterPreservesInvariant DEF vars

THEOREM FinalizedWitnessesIntersect ==
  \A s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs :
    /\ Invariant
    /\ <<s, b1, e1>> \in finalized
    /\ <<s, b2, e2>> \in finalized
    => \E v \in Validators :
         /\ <<v, s, b1, e1>> \in votes
         /\ <<v, s, b2, e2>> \in votes
PROOF
<1>1. TAKE s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs
<1>2. ASSUME Invariant,
               <<s, b1, e1>> \in finalized,
               <<s, b2, e2>> \in finalized
        PROVE \E v \in Validators :
                /\ <<v, s, b1, e1>> \in votes
                /\ <<v, s, b2, e2>> \in votes
  <2>1. finalizerSets[<<s, b1, e1>>] \subseteq Validators
    BY SMT, <1>2 DEF Invariant, TypeInvariant, FinalizationDomain, Finalization
  <2>2. finalizerSets[<<s, b2, e2>>] \subseteq Validators
    BY SMT, <1>2 DEF Invariant, TypeInvariant, FinalizationDomain, Finalization
  <2>3. Cardinality(finalizerSets[<<s, b1, e1>>]) >= QuorumSize
    BY SMT, <1>2 DEF Invariant, FinalizationWitnessSoundness
  <2>4. Cardinality(finalizerSets[<<s, b2, e2>>]) >= QuorumSize
    BY SMT, <1>2 DEF Invariant, FinalizationWitnessSoundness
  <2>5. finalizerSets[<<s, b1, e1>>] \cap finalizerSets[<<s, b2, e2>>] # {}
    BY <2>1, <2>2, <2>3, <2>4, QuorumIntersection
  <2>6. PICK v \in finalizerSets[<<s, b1, e1>>] \cap finalizerSets[<<s, b2, e2>>] : TRUE
    BY <2>5
  <2>7. <<v, s, b1, e1>> \in votes
    BY SMT, <1>2, <2>6 DEF Invariant, FinalizationWitnessSoundness
  <2>8. <<v, s, b2, e2>> \in votes
    BY SMT, <1>2, <2>6 DEF Invariant, FinalizationWitnessSoundness
  <2>9. QED
    BY SMT, <2>6, <2>7, <2>8
<1>3. QED
  BY <1>2

THEOREM InvariantImpliesSafety == Invariant => Safety
PROOF
<1>1. TAKE s \in Slots, b1 \in Blocks, b2 \in Blocks, e1 \in Epochs, e2 \in Epochs
<1>2. ASSUME Invariant,
               <<s, b1, e1>> \in finalized,
               <<s, b2, e2>> \in finalized
        PROVE b1 = b2
  <2>1. \E v \in Validators :
          /\ <<v, s, b1, e1>> \in votes
          /\ <<v, s, b2, e2>> \in votes
    BY SMT, FinalizedWitnessesIntersect, <1>2
  <2>2. PICK v \in Validators :
          /\ <<v, s, b1, e1>> \in votes
          /\ <<v, s, b2, e2>> \in votes
    BY <2>1
  <2>3. QED
    BY SMT, <1>2, <2>2 DEF Invariant, NoDualVotes
<1>3. QED
  BY <1>2 DEF Safety

====

CanonicalOrdering Companion Witnesses

Executable witness artifacts for omission dominance and recursive continuity.

CanonicalOrderingOmissionTrace.tla

Repository path: docs/architecture/protocols/aft/formal/canonical_ordering/CanonicalOrderingOmissionTrace.tla

---- MODULE CanonicalOrderingOmissionTrace ----
EXTENDS CanonicalOrdering

TargetSlot == 1
TargetCert == {"tx1"}
TargetTx == "tx2"

WitnessState ==
  /\ TargetSlot \in closedCutoffs
  /\ bulletin[TargetSlot] = {"tx1", "tx2"}
  /\ CertEvent(TargetSlot, TargetCert) \in candidateCerts
  /\ OmissionEvent(TargetSlot, TargetCert, TargetTx) \in omissionProofs
  /\ CertEvent(TargetSlot, TargetCert) \notin admittedCerts

NoOmissionDominanceWitness == ~WitnessState

====

CanonicalOrderingOmissionTrace.cfg

Repository path: docs/architecture/protocols/aft/formal/canonical_ordering/CanonicalOrderingOmissionTrace.cfg

SPECIFICATION Spec

CONSTANTS
  Slots = {1}
  Transactions = {"tx1", "tx2"}

INVARIANTS
  TypeInvariant
  AdmittedSoundness
  OmissionSoundness
  RecoveredSoundness
  AdmittedUniqueness
  Recoverability
  OmissionDominates
  NoOmissionDominanceWitness

CanonicalCollapseRecursiveContinuity.tla

Repository path: docs/architecture/protocols/aft/formal/canonical_ordering/CanonicalCollapseRecursiveContinuity.tla

---- MODULE CanonicalCollapseRecursiveContinuity ----
EXTENDS Naturals, Sequences, TLC

CONSTANT MaxHeight

Slots == 1..MaxHeight
Genesis == 1
NonGenesisSlots == Slots \ {Genesis}
NullHash == 0

VARIABLES publishedCollapses, publishedProofs, publishedExtensionCertificates, admittedHeaders

vars ==
  <<publishedCollapses, publishedProofs, publishedExtensionCertificates, admittedHeaders>>

RECURSIVE AccumulatorHash(_), ProofHash(_), ProofChain(_)

PayloadHash(s) == <<"payload", s>>

AccumulatorHash(s) ==
  IF s = Genesis
    THEN <<"accum", s, NullHash, PayloadHash(s)>>
    ELSE <<"accum", s, AccumulatorHash(s - 1), PayloadHash(s)>>

Commitment(s) ==
  [height |-> s,
   continuityAccumulatorHash |-> AccumulatorHash(s),
   resultingStateRootHash |-> <<"state", s>>]

CommitmentHash(s) == <<"commitment-hash", Commitment(s)>>

PreviousCommitmentHash(s) ==
  IF s = Genesis THEN NullHash ELSE CommitmentHash(s - 1)

StatementHash(s) ==
  <<"statement-hash", Commitment(s), PreviousCommitmentHash(s), PayloadHash(s)>>

PreviousProofHash(s) ==
  IF s = Genesis THEN NullHash ELSE ProofHash(s - 1)

ProofBytes(s) ==
  <<"hash-pcd-v1", StatementHash(s), PreviousProofHash(s)>>

ProofStep(s) ==
  [commitment |-> Commitment(s),
   previousCommitmentHash |-> PreviousCommitmentHash(s),
   payloadHash |-> PayloadHash(s),
   previousProofHash |-> PreviousProofHash(s),
   proofBytes |-> ProofBytes(s)]

ProofHash(s) == <<"proof-hash", ProofStep(s)>>

ProofChain(s) ==
  IF s = Genesis
    THEN <<ProofStep(s)>>
    ELSE Append(ProofChain(s - 1), ProofStep(s))

ExtensionCertificate(s) ==
  [coveredHeight |-> s,
   predecessorCommitment |-> Commitment(s - 1),
   predecessorProofHash |-> ProofHash(s - 1)]

Last(seq) == seq[Len(seq)]

Init ==
  /\ publishedCollapses = {}
  /\ publishedProofs = {}
  /\ publishedExtensionCertificates = {}
  /\ admittedHeaders = {}

PublishCollapseStep ==
  \E s \in Slots :
    /\ s \notin publishedCollapses
    /\ publishedCollapses' = publishedCollapses \cup {s}
    /\ UNCHANGED <<publishedProofs, publishedExtensionCertificates, admittedHeaders>>

PublishRecursiveProofStep ==
  \E s \in Slots :
    /\ s \in publishedCollapses
    /\ s \notin publishedProofs
    /\ IF s = Genesis THEN TRUE ELSE s - 1 \in publishedProofs
    /\ publishedProofs' = publishedProofs \cup {s}
    /\ UNCHANGED <<publishedCollapses, publishedExtensionCertificates, admittedHeaders>>

PublishExtensionCertificateStep ==
  \E s \in NonGenesisSlots :
    /\ s \in publishedCollapses
    /\ s - 1 \in publishedProofs
    /\ s \notin publishedExtensionCertificates
    /\ publishedExtensionCertificates' = publishedExtensionCertificates \cup {s}
    /\ UNCHANGED <<publishedCollapses, publishedProofs, admittedHeaders>>

AdmitHeaderStep ==
  \E s \in Slots :
    /\ s \in publishedCollapses
    /\ s \notin admittedHeaders
    /\ IF s = Genesis THEN TRUE ELSE s \in publishedExtensionCertificates
    /\ admittedHeaders' = admittedHeaders \cup {s}
    /\ UNCHANGED <<publishedCollapses, publishedProofs, publishedExtensionCertificates>>

Next ==
  \/ PublishCollapseStep
  \/ PublishRecursiveProofStep
  \/ PublishExtensionCertificateStep
  \/ AdmitHeaderStep

TypeInvariant ==
  /\ publishedCollapses \subseteq Slots
  /\ publishedProofs \subseteq Slots
  /\ publishedExtensionCertificates \subseteq NonGenesisSlots
  /\ admittedHeaders \subseteq Slots

RecursiveProofSoundness ==
  \A s \in publishedProofs :
    /\ s \in publishedCollapses
    /\ IF s = Genesis THEN TRUE ELSE s - 1 \in publishedProofs
    /\ LET step == ProofStep(s) IN
         /\ step.commitment = Commitment(s)
         /\ step.previousCommitmentHash = PreviousCommitmentHash(s)
         /\ step.payloadHash = PayloadHash(s)
         /\ step.previousProofHash = PreviousProofHash(s)
         /\ step.proofBytes = ProofBytes(s)
         /\ step.commitment.continuityAccumulatorHash = AccumulatorHash(s)

RecursiveProofChainSoundness ==
  \A s \in publishedProofs :
    /\ Len(ProofChain(s)) = s
    /\ Last(ProofChain(s)) = ProofStep(s)
    /\ IF s = Genesis
         THEN TRUE
         ELSE /\ ProofChain(s)[Len(ProofChain(s)) - 1] = ProofStep(s - 1)

ExtensionCertificateSoundness ==
  \A s \in publishedExtensionCertificates :
    /\ s \in NonGenesisSlots
    /\ s - 1 \in publishedProofs
    /\ ExtensionCertificate(s).coveredHeight = s
    /\ ExtensionCertificate(s).predecessorCommitment = Commitment(s - 1)
    /\ ExtensionCertificate(s).predecessorProofHash = ProofHash(s - 1)

HeaderAdmissionSoundness ==
  \A s \in admittedHeaders :
    /\ s \in publishedCollapses
    /\ IF s = Genesis
         THEN TRUE
         ELSE /\ s \in publishedExtensionCertificates
              /\ s - 1 \in publishedProofs
              /\ ExtensionCertificate(s).predecessorCommitment = Commitment(s - 1)
              /\ ExtensionCertificate(s).predecessorProofHash = ProofHash(s - 1)

Invariant ==
  /\ TypeInvariant
  /\ RecursiveProofSoundness
  /\ RecursiveProofChainSoundness
  /\ ExtensionCertificateSoundness
  /\ HeaderAdmissionSoundness

Spec == Init /\ [][Next]_vars

====

CanonicalCollapseRecursiveContinuity.cfg

Repository path: docs/architecture/protocols/aft/formal/canonical_ordering/CanonicalCollapseRecursiveContinuity.cfg

SPECIFICATION Spec

CONSTANTS
  MaxHeight = 3

INVARIANTS
  TypeInvariant
  RecursiveProofSoundness
  RecursiveProofChainSoundness
  ExtensionCertificateSoundness
  HeaderAdmissionSoundness

Recovery and Classical-Agreement Bridge

Recurring recovery kernel, finite reduction, totality bridge, and final classical-agreement collapse wrapper.

NestedGuardianRecoveryRecurringInductionCore.tla

Repository path: docs/architecture/protocols/aft/formal/nested_guardian/NestedGuardianRecoveryRecurringInductionCore.tla

---- MODULE NestedGuardianRecoveryRecurringInductionCore ----
EXTENDS Naturals, FiniteSets, TLC

CONSTANT Validators, Witnesses, Blocks, Slots, Epochs, QuorumSize, MaxReassignmentDepth,
         InitialEpoch, InitialWitness, TotalCycles,
         TargetSlotOf(_), TargetBlockOf(_), StableEpochOf(_),
         SmallCommitteeSlot, SmallRecoveryThreshold, LargeRecoveryThreshold,
         SmallRecoveryCommittee, LargeRecoveryCommittee

ASSUME InitialEpoch \in Epochs
ASSUME InitialWitness \in Witnesses
ASSUME QuorumSize \in 1..Cardinality(Validators)
ASSUME TotalCycles \in Nat
ASSUME TotalCycles >= 1
ASSUME \A c \in 1..TotalCycles :
  /\ TargetSlotOf(c) \in Slots
  /\ TargetBlockOf(c) \in Blocks
  /\ StableEpochOf(c) \in Epochs

VARIABLES votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, witnessOnline,
          witnessCheckpoint, assignedWitness, reassignmentDepth, currentCycle, phase, churnStage,
          continuationBoundary, continuationAnchorPublished, continuationAnchorBoundary,
          continuationPagePublished, continuationPageBoundary, continuationFetched,
          shareReceipts, shareConflicts, windowClosed, missingShareClaims,
          missingThresholdCertificates, recovered, recoveredSurfaces,
          recoveryConflicts, aborted

Core ==
  INSTANCE NestedGuardianRecoveryRecurringLivenessCore
  WITH Validators <- Validators,
       Witnesses <- Witnesses,
       Blocks <- Blocks,
       Slots <- Slots,
       Epochs <- Epochs,
       QuorumSize <- QuorumSize,
       MaxReassignmentDepth <- MaxReassignmentDepth,
       InitialEpoch <- InitialEpoch,
       InitialWitness <- InitialWitness,
       TotalCycles <- TotalCycles,
       TargetSlotOf <- TargetSlotOf,
       TargetBlockOf <- TargetBlockOf,
       StableEpochOf <- StableEpochOf,
       SmallCommitteeSlot <- SmallCommitteeSlot,
       SmallRecoveryThreshold <- SmallRecoveryThreshold,
       LargeRecoveryThreshold <- LargeRecoveryThreshold,
       SmallRecoveryCommittee <- SmallRecoveryCommittee,
       LargeRecoveryCommittee <- LargeRecoveryCommittee,
       votes <- votes,
       witnessCerts <- witnessCerts,
       finalized <- finalized,
       finalizerSets <- finalizerSets,
       registryEpoch <- registryEpoch,
       guardianReady <- guardianReady,
       witnessOnline <- witnessOnline,
       witnessCheckpoint <- witnessCheckpoint,
       assignedWitness <- assignedWitness,
       reassignmentDepth <- reassignmentDepth,
       currentCycle <- currentCycle,
       phase <- phase,
       churnStage <- churnStage,
       continuationBoundary <- continuationBoundary,
       continuationAnchorPublished <- continuationAnchorPublished,
       continuationAnchorBoundary <- continuationAnchorBoundary,
       continuationPagePublished <- continuationPagePublished,
       continuationPageBoundary <- continuationPageBoundary,
       continuationFetched <- continuationFetched,
       shareReceipts <- shareReceipts,
       shareConflicts <- shareConflicts,
       windowClosed <- windowClosed,
       missingShareClaims <- missingShareClaims,
       missingThresholdCertificates <- missingThresholdCertificates,
       recovered <- recovered,
       recoveredSurfaces <- recoveredSurfaces,
       recoveryConflicts <- recoveryConflicts,
       aborted <- aborted

vars == Core!vars
CycleRange == Core!CycleRange
PrefixAdvanceRange == Core!PrefixAdvanceRange
RecoveryClosedPrefix(c) == Core!RecoveryClosedPrefix(c)

PriorCycleRange(c) ==
  IF c = 1 THEN {}
  ELSE 1..(c - 1)

RecoveryInductionBase ==
  <>RecoveryClosedPrefix(1)

RecoveryInductionStep(c) ==
  /\ c \in PrefixAdvanceRange
  /\ Core!RecoveryPrefixAdvanceContract(c)

RecoveryInductionPremisesUpTo(c) ==
  /\ c \in CycleRange
  /\ RecoveryInductionBase
  /\ \A i \in PriorCycleRange(c) :
       RecoveryInductionStep(i)

RecoveryRecurringInductionPremises ==
  /\ RecoveryInductionBase
  /\ \A i \in PrefixAdvanceRange :
       RecoveryInductionStep(i)

RecoveryClosedPrefixInductionKernel(c) ==
  /\ c \in CycleRange
  /\ (RecoveryInductionPremisesUpTo(c)
      => <>RecoveryClosedPrefix(c))

RecoveryRecurringInductionKernel ==
  \A c \in CycleRange :
    RecoveryClosedPrefixInductionKernel(c)

====

NestedGuardianRecoveryRecurringProof.tla

Repository path: docs/architecture/protocols/aft/formal/nested_guardian/NestedGuardianRecoveryRecurringProof.tla

---- MODULE NestedGuardianRecoveryRecurringProof ----
EXTENDS Naturals, FiniteSets, TLC, TLAPS

CONSTANT Validators, Witnesses, Blocks, Slots, Epochs, QuorumSize, MaxReassignmentDepth,
         InitialEpoch, InitialWitness, TotalCycles,
         TargetSlotOf(_), TargetBlockOf(_), StableEpochOf(_),
         SmallCommitteeSlot, SmallRecoveryThreshold, LargeRecoveryThreshold,
         SmallRecoveryCommittee, LargeRecoveryCommittee

ASSUME InitialEpochInEpochs == InitialEpoch \in Epochs
ASSUME InitialWitnessInWitnesses == InitialWitness \in Witnesses
ASSUME QuorumSizeInValidatorRange == QuorumSize \in 1..Cardinality(Validators)
ASSUME TotalCyclesIsNat == TotalCycles \in Nat
ASSUME TotalCyclesAtLeastOne == TotalCycles >= 1
ASSUME TargetCycleDomains ==
  \A c \in 1..TotalCycles :
  /\ TargetSlotOf(c) \in Slots
  /\ TargetBlockOf(c) \in Blocks
  /\ StableEpochOf(c) \in Epochs

VARIABLES votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, witnessOnline,
          witnessCheckpoint, assignedWitness, reassignmentDepth, currentCycle, phase, churnStage,
          continuationBoundary, continuationAnchorPublished, continuationAnchorBoundary,
          continuationPagePublished, continuationPageBoundary, continuationFetched,
          shareReceipts, shareConflicts, windowClosed, missingShareClaims,
          missingThresholdCertificates, recovered, recoveredSurfaces,
          recoveryConflicts, aborted

Core ==
  INSTANCE NestedGuardianRecoveryRecurringInductionCore
  WITH Validators <- Validators,
       Witnesses <- Witnesses,
       Blocks <- Blocks,
       Slots <- Slots,
       Epochs <- Epochs,
       QuorumSize <- QuorumSize,
       MaxReassignmentDepth <- MaxReassignmentDepth,
       InitialEpoch <- InitialEpoch,
       InitialWitness <- InitialWitness,
       TotalCycles <- TotalCycles,
       TargetSlotOf <- TargetSlotOf,
       TargetBlockOf <- TargetBlockOf,
       StableEpochOf <- StableEpochOf,
       SmallCommitteeSlot <- SmallCommitteeSlot,
       SmallRecoveryThreshold <- SmallRecoveryThreshold,
       LargeRecoveryThreshold <- LargeRecoveryThreshold,
       SmallRecoveryCommittee <- SmallRecoveryCommittee,
       LargeRecoveryCommittee <- LargeRecoveryCommittee,
       votes <- votes,
       witnessCerts <- witnessCerts,
       finalized <- finalized,
       finalizerSets <- finalizerSets,
       registryEpoch <- registryEpoch,
       guardianReady <- guardianReady,
       witnessOnline <- witnessOnline,
       witnessCheckpoint <- witnessCheckpoint,
       assignedWitness <- assignedWitness,
       reassignmentDepth <- reassignmentDepth,
       currentCycle <- currentCycle,
       phase <- phase,
       churnStage <- churnStage,
       continuationBoundary <- continuationBoundary,
       continuationAnchorPublished <- continuationAnchorPublished,
       continuationAnchorBoundary <- continuationAnchorBoundary,
       continuationPagePublished <- continuationPagePublished,
       continuationPageBoundary <- continuationPageBoundary,
       continuationFetched <- continuationFetched,
       shareReceipts <- shareReceipts,
       shareConflicts <- shareConflicts,
       windowClosed <- windowClosed,
       missingShareClaims <- missingShareClaims,
       missingThresholdCertificates <- missingThresholdCertificates,
       recovered <- recovered,
       recoveredSurfaces <- recoveredSurfaces,
       recoveryConflicts <- recoveryConflicts,
       aborted <- aborted

RecoveryRecurringClosedPrefixes ==
  \A c \in Core!CycleRange :
    <>Core!RecoveryClosedPrefix(c)

RecoveryParametricRecurrenceArgument ==
  /\ Core!RecoveryRecurringInductionPremises
  /\ Core!RecoveryRecurringInductionKernel
  => RecoveryRecurringClosedPrefixes

THEOREM PriorCycleRangeImpliesTotalCyclesNotOne ==
  \A c \in Core!CycleRange :
    \A i \in Core!PriorCycleRange(c) :
      TotalCycles # 1
  BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne
     DEF Core!CycleRange, Core!Core!CycleRange, Core!PriorCycleRange

THEOREM PriorCycleRangeImpliesPrefixAdvanceInterval ==
  \A c \in Core!CycleRange :
    \A i \in Core!PriorCycleRange(c) :
      i \in 1..(TotalCycles - 1)
  BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne
     DEF Core!CycleRange, Core!Core!CycleRange, Core!PriorCycleRange

THEOREM RecoveryInductionPremisesRestrict ==
  \A c \in Core!CycleRange :
    Core!RecoveryRecurringInductionPremises
      => Core!RecoveryInductionPremisesUpTo(c)
PROOF
  <1>1. TAKE c \in Core!CycleRange
  <1>2. ASSUME Core!RecoveryRecurringInductionPremises
        PROVE Core!RecoveryInductionPremisesUpTo(c)
    <2>1. Core!RecoveryInductionBase
          BY <1>2 DEF Core!RecoveryRecurringInductionPremises
    <2>2. \A i \in Core!PriorCycleRange(c) :
             Core!RecoveryInductionStep(i)
      PROOF
        <3>1. TAKE i \in Core!PriorCycleRange(c)
        <3>2. i \in Core!PrefixAdvanceRange
          PROOF
            <4>1. TotalCycles # 1
                  BY PriorCycleRangeImpliesTotalCyclesNotOne, <1>1, <3>1
            <4>2. i \in 1..(TotalCycles - 1)
                  BY PriorCycleRangeImpliesPrefixAdvanceInterval, <1>1, <3>1
            <4>3. TotalCycles # 1
                  BY <4>1
            <4>6. QED
                  BY <4>3, <4>2
                     DEF Core!PrefixAdvanceRange, Core!Core!PrefixAdvanceRange
        <3>3. Core!RecoveryInductionStep(i)
              BY <1>2, <3>2 DEF Core!RecoveryRecurringInductionPremises
        <3>4. QED
              BY <3>3
      <2>3. QED
          BY <1>1, <2>1, <2>2
             DEF Core!RecoveryInductionPremisesUpTo
  <1>3. QED
        BY <1>2

THEOREM RecoveryInductionKernelRestrict ==
  \A c \in Core!CycleRange :
    Core!RecoveryRecurringInductionKernel
      => Core!RecoveryClosedPrefixInductionKernel(c)
  BY DEF Core!RecoveryRecurringInductionKernel,
         Core!RecoveryClosedPrefixInductionKernel,
         Core!CycleRange

THEOREM RecoveryRecurringClosedPrefixFromKernel ==
  \A c \in Core!CycleRange :
    /\ Core!RecoveryRecurringInductionPremises
    /\ Core!RecoveryRecurringInductionKernel
    => <>Core!RecoveryClosedPrefix(c)
PROOF
  <1>1. TAKE c \in Core!CycleRange
  <1>2. ASSUME Core!RecoveryRecurringInductionPremises,
               Core!RecoveryRecurringInductionKernel
        PROVE <>Core!RecoveryClosedPrefix(c)
    <2>1. Core!RecoveryInductionPremisesUpTo(c)
          BY RecoveryInductionPremisesRestrict, <1>1, <1>2
    <2>2. Core!RecoveryClosedPrefixInductionKernel(c)
          BY RecoveryInductionKernelRestrict, <1>1, <1>2
    <2>3. QED
          BY <2>1, <2>2
             DEF Core!RecoveryClosedPrefixInductionKernel
  <1>3. QED
        BY <1>2

THEOREM RecoveryParametricRecurrenceArgumentTheorem ==
  RecoveryParametricRecurrenceArgument
  BY RecoveryRecurringClosedPrefixFromKernel
     DEF RecoveryParametricRecurrenceArgument,
         RecoveryRecurringClosedPrefixes

====

NestedGuardianRecoveryClassicalAgreementReduction.tla

Repository path: docs/architecture/protocols/aft/formal/nested_guardian/NestedGuardianRecoveryClassicalAgreementReduction.tla

---- MODULE NestedGuardianRecoveryClassicalAgreementReduction ----
EXTENDS Naturals, FiniteSets, TLC, TLAPS

CONSTANT Validators, Witnesses, Blocks, Slots, Epochs, QuorumSize, MaxReassignmentDepth,
         InitialEpoch, InitialWitness, TotalCycles,
         TargetSlotOf(_), TargetBlockOf(_), StableEpochOf(_),
         SmallCommitteeSlot, SmallRecoveryThreshold, LargeRecoveryThreshold,
         SmallRecoveryCommittee, LargeRecoveryCommittee

ASSUME InitialEpoch \in Epochs
ASSUME InitialWitness \in Witnesses
ASSUME QuorumSize \in 1..Cardinality(Validators)
ASSUME TotalCycles \in Nat
ASSUME TotalCycles >= 1
ASSUME \A c \in 1..TotalCycles :
  /\ TargetSlotOf(c) \in Slots
  /\ TargetBlockOf(c) \in Blocks
  /\ StableEpochOf(c) \in Epochs

VARIABLES votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, witnessOnline,
          witnessCheckpoint, assignedWitness, reassignmentDepth, currentCycle, phase, churnStage,
          continuationBoundary, continuationAnchorPublished, continuationAnchorBoundary,
          continuationPagePublished, continuationPageBoundary, continuationFetched,
          shareReceipts, shareConflicts, windowClosed, missingShareClaims,
          missingThresholdCertificates, recovered, recoveredSurfaces,
          recoveryConflicts, aborted

Proof ==
  INSTANCE NestedGuardianRecoveryRecurringProof
  WITH Validators <- Validators,
       Witnesses <- Witnesses,
       Blocks <- Blocks,
       Slots <- Slots,
       Epochs <- Epochs,
       QuorumSize <- QuorumSize,
       MaxReassignmentDepth <- MaxReassignmentDepth,
       InitialEpoch <- InitialEpoch,
       InitialWitness <- InitialWitness,
       TotalCycles <- TotalCycles,
       TargetSlotOf <- TargetSlotOf,
       TargetBlockOf <- TargetBlockOf,
       StableEpochOf <- StableEpochOf,
       SmallCommitteeSlot <- SmallCommitteeSlot,
       SmallRecoveryThreshold <- SmallRecoveryThreshold,
       LargeRecoveryThreshold <- LargeRecoveryThreshold,
       SmallRecoveryCommittee <- SmallRecoveryCommittee,
       LargeRecoveryCommittee <- LargeRecoveryCommittee,
       votes <- votes,
       witnessCerts <- witnessCerts,
       finalized <- finalized,
       finalizerSets <- finalizerSets,
       registryEpoch <- registryEpoch,
       guardianReady <- guardianReady,
       witnessOnline <- witnessOnline,
       witnessCheckpoint <- witnessCheckpoint,
       assignedWitness <- assignedWitness,
       reassignmentDepth <- reassignmentDepth,
       currentCycle <- currentCycle,
       phase <- phase,
       churnStage <- churnStage,
       continuationBoundary <- continuationBoundary,
       continuationAnchorPublished <- continuationAnchorPublished,
       continuationAnchorBoundary <- continuationAnchorBoundary,
       continuationPagePublished <- continuationPagePublished,
       continuationPageBoundary <- continuationPageBoundary,
       continuationFetched <- continuationFetched,
       shareReceipts <- shareReceipts,
       shareConflicts <- shareConflicts,
       windowClosed <- windowClosed,
       missingShareClaims <- missingShareClaims,
       missingThresholdCertificates <- missingThresholdCertificates,
       recovered <- recovered,
       recoveredSurfaces <- recoveredSurfaces,
       recoveryConflicts <- recoveryConflicts,
       aborted <- aborted

CycleRange == 1..TotalCycles

ClassicalAgreementDecisionObject(c) ==
  [cycle |-> c,
   slot |-> TargetSlotOf(c),
   block |-> TargetBlockOf(c),
   epoch |-> StableEpochOf(c)]

ClassicalAgreementPrefixObject(c) ==
  [i \in 1..c |-> ClassicalAgreementDecisionObject(i)]

FiniteClassicalAgreementPrefixRealized(c) ==
  /\ c \in CycleRange
  /\ <>Proof!Core!RecoveryClosedPrefix(c)

FiniteClassicalAgreementLiveness ==
  \A c \in CycleRange :
    FiniteClassicalAgreementPrefixRealized(c)

ClassicalAgreementFiniteReduction ==
  Proof!RecoveryRecurringClosedPrefixes
    => FiniteClassicalAgreementLiveness

THEOREM ProofCycleRangeMatchesCycleRange ==
  Proof!Core!CycleRange = CycleRange
  BY DEF Proof!Core!CycleRange, Proof!Core!Core!CycleRange, CycleRange

THEOREM FiniteClassicalAgreementPrefixFromRecurringPrefixes ==
  \A c \in CycleRange :
    Proof!RecoveryRecurringClosedPrefixes
      => FiniteClassicalAgreementPrefixRealized(c)
PROOF
  <1>1. TAKE c \in CycleRange
  <1>2. ASSUME Proof!RecoveryRecurringClosedPrefixes
        PROVE FiniteClassicalAgreementPrefixRealized(c)
    <2>1. c \in Proof!Core!CycleRange
          BY ProofCycleRangeMatchesCycleRange, <1>1
    <2>2. <>Proof!Core!RecoveryClosedPrefix(c)
          BY <1>2, <2>1 DEF Proof!RecoveryRecurringClosedPrefixes
    <2>3. QED
          BY <1>1, <2>2 DEF FiniteClassicalAgreementPrefixRealized
  <1>3. QED
        BY <1>2

THEOREM ClassicalAgreementFiniteReductionTheorem ==
  ClassicalAgreementFiniteReduction
  BY FiniteClassicalAgreementPrefixFromRecurringPrefixes
     DEF ClassicalAgreementFiniteReduction,
         FiniteClassicalAgreementLiveness

====

NestedGuardianRecoveryClassicalAgreementTotality.tla

Repository path: docs/architecture/protocols/aft/formal/nested_guardian/NestedGuardianRecoveryClassicalAgreementTotality.tla

---- MODULE NestedGuardianRecoveryClassicalAgreementTotality ----
EXTENDS Naturals, FiniteSets, TLC, TLAPS

CONSTANT Validators, Witnesses, Blocks, Slots, Epochs, QuorumSize, MaxReassignmentDepth,
         InitialEpoch, InitialWitness, TotalCycles,
         TargetSlotOf(_), TargetBlockOf(_), StableEpochOf(_),
         SmallCommitteeSlot, SmallRecoveryThreshold, LargeRecoveryThreshold,
         SmallRecoveryCommittee, LargeRecoveryCommittee

ASSUME InitialEpochInEpochs == InitialEpoch \in Epochs
ASSUME InitialWitnessInWitnesses == InitialWitness \in Witnesses
ASSUME QuorumSizeInValidatorRange == QuorumSize \in 1..Cardinality(Validators)
ASSUME TotalCyclesIsNat == TotalCycles \in Nat
ASSUME TotalCyclesAtLeastOne == TotalCycles >= 1
ASSUME TargetCycleDomains ==
  \A c \in 1..TotalCycles :
  /\ TargetSlotOf(c) \in Slots
  /\ TargetBlockOf(c) \in Blocks
  /\ StableEpochOf(c) \in Epochs

VARIABLES votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, witnessOnline,
          witnessCheckpoint, assignedWitness, reassignmentDepth, currentCycle, phase, churnStage,
          continuationBoundary, continuationAnchorPublished, continuationAnchorBoundary,
          continuationPagePublished, continuationPageBoundary, continuationFetched,
          shareReceipts, shareConflicts, windowClosed, missingShareClaims,
          missingThresholdCertificates, recovered, recoveredSurfaces,
          recoveryConflicts, aborted

Reduction ==
  INSTANCE NestedGuardianRecoveryClassicalAgreementReduction
  WITH Validators <- Validators,
       Witnesses <- Witnesses,
       Blocks <- Blocks,
       Slots <- Slots,
       Epochs <- Epochs,
       QuorumSize <- QuorumSize,
       MaxReassignmentDepth <- MaxReassignmentDepth,
       InitialEpoch <- InitialEpoch,
       InitialWitness <- InitialWitness,
       TotalCycles <- TotalCycles,
       TargetSlotOf <- TargetSlotOf,
       TargetBlockOf <- TargetBlockOf,
       StableEpochOf <- StableEpochOf,
       SmallCommitteeSlot <- SmallCommitteeSlot,
       SmallRecoveryThreshold <- SmallRecoveryThreshold,
       LargeRecoveryThreshold <- LargeRecoveryThreshold,
       SmallRecoveryCommittee <- SmallRecoveryCommittee,
       LargeRecoveryCommittee <- LargeRecoveryCommittee,
       votes <- votes,
       witnessCerts <- witnessCerts,
       finalized <- finalized,
       finalizerSets <- finalizerSets,
       registryEpoch <- registryEpoch,
       guardianReady <- guardianReady,
       witnessOnline <- witnessOnline,
       witnessCheckpoint <- witnessCheckpoint,
       assignedWitness <- assignedWitness,
       reassignmentDepth <- reassignmentDepth,
       currentCycle <- currentCycle,
       phase <- phase,
       churnStage <- churnStage,
       continuationBoundary <- continuationBoundary,
       continuationAnchorPublished <- continuationAnchorPublished,
       continuationAnchorBoundary <- continuationAnchorBoundary,
       continuationPagePublished <- continuationPagePublished,
       continuationPageBoundary <- continuationPageBoundary,
       continuationFetched <- continuationFetched,
       shareReceipts <- shareReceipts,
       shareConflicts <- shareConflicts,
       windowClosed <- windowClosed,
       missingShareClaims <- missingShareClaims,
       missingThresholdCertificates <- missingThresholdCertificates,
       recovered <- recovered,
       recoveredSurfaces <- recoveredSurfaces,
       recoveryConflicts <- recoveryConflicts,
       aborted <- aborted

CycleRange == 1..TotalCycles

RecoveryRecurringClosedPrefixes == Reduction!Proof!RecoveryRecurringClosedPrefixes
RecoveryRecurringInductionPremises == Reduction!Proof!Core!RecoveryRecurringInductionPremises
RecoveryRecurringInductionKernel == Reduction!Proof!Core!RecoveryRecurringInductionKernel
RecoveryClosedPrefix(c) == Reduction!Proof!Core!RecoveryClosedPrefix(c)

ClassicalAgreementTotalHistoryObject ==
  [i \in CycleRange |-> Reduction!ClassicalAgreementDecisionObject(i)]

ClassicalAgreementTotalHistoryExtendsFinitePrefixes ==
  \A c \in CycleRange :
    [i \in 1..c |-> ClassicalAgreementTotalHistoryObject[i]]
      = Reduction!ClassicalAgreementPrefixObject(c)

TotalClassicalAgreementHistoryRealized ==
  /\ <>RecoveryClosedPrefix(TotalCycles)
  /\ ClassicalAgreementTotalHistoryExtendsFinitePrefixes

TotalClassicalAgreementReduction ==
  Reduction!FiniteClassicalAgreementLiveness
    => TotalClassicalAgreementHistoryRealized

TotalClassicalAgreementFromRecurringPrefixes ==
  RecoveryRecurringClosedPrefixes
    => TotalClassicalAgreementHistoryRealized

TotalClassicalAgreementFromRecurrenceKernel ==
  /\ RecoveryRecurringInductionPremises
  /\ RecoveryRecurringInductionKernel
  => TotalClassicalAgreementHistoryRealized

THEOREM TotalHistoryEntryMatchesDecisionObject ==
  \A c \in CycleRange :
    \A i \in 1..c :
      ClassicalAgreementTotalHistoryObject[i]
        = Reduction!ClassicalAgreementDecisionObject(i)
  BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne
     DEF CycleRange, ClassicalAgreementTotalHistoryObject

THEOREM ClassicalAgreementTotalHistoryExtendsFinitePrefixesTheorem ==
  ClassicalAgreementTotalHistoryExtendsFinitePrefixes
PROOF
  <1>1. \A c \in CycleRange :
           [i \in 1..c |-> ClassicalAgreementTotalHistoryObject[i]]
             = Reduction!ClassicalAgreementPrefixObject(c)
    PROOF
      <2>1. TAKE c \in CycleRange
      <2>2. \A i \in 1..c :
               ClassicalAgreementTotalHistoryObject[i]
                 = Reduction!ClassicalAgreementDecisionObject(i)
            BY TotalHistoryEntryMatchesDecisionObject, <2>1
      <2>3. QED
            BY IsaWithSetExtensionality, <2>1, <2>2
               DEF Reduction!ClassicalAgreementPrefixObject
  <1>2. QED
        BY <1>1 DEF ClassicalAgreementTotalHistoryExtendsFinitePrefixes

THEOREM TotalCyclesInCycleRange ==
  TotalCycles \in CycleRange
  BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne DEF CycleRange

THEOREM TotalFinitePrefixFromFiniteLiveness ==
  Reduction!FiniteClassicalAgreementLiveness
    => Reduction!FiniteClassicalAgreementPrefixRealized(TotalCycles)
PROOF
  <1>1. ASSUME Reduction!FiniteClassicalAgreementLiveness
        PROVE Reduction!FiniteClassicalAgreementPrefixRealized(TotalCycles)
    <2>1. TotalCycles \in Reduction!CycleRange
          BY TotalCyclesInCycleRange DEF CycleRange, Reduction!CycleRange
    <2>2. QED
          BY <1>1, <2>1 DEF Reduction!FiniteClassicalAgreementLiveness
  <1>2. QED
        BY <1>1

THEOREM TotalRecoveryClosedPrefixFromFiniteLiveness ==
  Reduction!FiniteClassicalAgreementLiveness
    => <>RecoveryClosedPrefix(TotalCycles)
  BY TotalFinitePrefixFromFiniteLiveness
     DEF Reduction!FiniteClassicalAgreementPrefixRealized,
         RecoveryClosedPrefix

THEOREM TotalClassicalAgreementReductionTheorem ==
  TotalClassicalAgreementReduction
  BY TotalRecoveryClosedPrefixFromFiniteLiveness,
     ClassicalAgreementTotalHistoryExtendsFinitePrefixesTheorem
     DEF TotalClassicalAgreementReduction,
         TotalClassicalAgreementHistoryRealized

THEOREM ReductionLivenessFromRecurringPrefixes ==
  RecoveryRecurringClosedPrefixes
    => Reduction!FiniteClassicalAgreementLiveness
PROOF
  <1>1. ASSUME RecoveryRecurringClosedPrefixes
        PROVE Reduction!FiniteClassicalAgreementLiveness
    <2>1. \A c \in Reduction!CycleRange :
             Reduction!FiniteClassicalAgreementPrefixRealized(c)
      PROOF
        <3>1. TAKE c \in Reduction!CycleRange
        <3>2. c \in Reduction!Proof!Core!CycleRange
              BY <3>1
                 DEF Reduction!CycleRange,
                     Reduction!Proof!Core!CycleRange,
                     Reduction!Proof!Core!Core!CycleRange
        <3>3. Reduction!Proof!RecoveryRecurringClosedPrefixes
              BY <1>1 DEF RecoveryRecurringClosedPrefixes
        <3>4. <>Reduction!Proof!Core!RecoveryClosedPrefix(c)
              BY <3>2, <3>3 DEF Reduction!Proof!RecoveryRecurringClosedPrefixes
        <3>5. QED
              BY <3>1, <3>4 DEF Reduction!FiniteClassicalAgreementPrefixRealized
    <2>2. QED
          BY <2>1 DEF Reduction!FiniteClassicalAgreementLiveness
  <1>2. QED
        BY <1>1

THEOREM TotalClassicalAgreementFromRecurringPrefixesTheorem ==
  TotalClassicalAgreementFromRecurringPrefixes
PROOF
  <1>1. ASSUME RecoveryRecurringClosedPrefixes
        PROVE TotalClassicalAgreementHistoryRealized
    <2>1. Reduction!FiniteClassicalAgreementLiveness
          BY ReductionLivenessFromRecurringPrefixes, <1>1
    <2>2. Reduction!FiniteClassicalAgreementLiveness
             => TotalClassicalAgreementHistoryRealized
          BY TotalClassicalAgreementReductionTheorem
             DEF TotalClassicalAgreementReduction
    <2>3. QED
          BY <2>1, <2>2
  <1>2. QED
        BY <1>1 DEF TotalClassicalAgreementFromRecurringPrefixes

THEOREM RecoveryRecurringClosedPrefixesFromRecurrenceKernel ==
  /\ RecoveryRecurringInductionPremises
  /\ RecoveryRecurringInductionKernel
  => RecoveryRecurringClosedPrefixes
PROOF
  <1>1. ASSUME RecoveryRecurringInductionPremises,
               RecoveryRecurringInductionKernel
        PROVE RecoveryRecurringClosedPrefixes
    <2>1. \A c \in Reduction!Proof!Core!CycleRange :
             <>Reduction!Proof!Core!RecoveryClosedPrefix(c)
      PROOF
        <3>1. TAKE c \in Reduction!Proof!Core!CycleRange
        <3>2. Reduction!Proof!Core!RecoveryInductionPremisesUpTo(c)
          PROOF
            <4>1. Reduction!Proof!Core!RecoveryInductionBase
                  BY <1>1
                     DEF RecoveryRecurringInductionPremises,
                         Reduction!Proof!Core!RecoveryRecurringInductionPremises
            <4>2. \A i \in Reduction!Proof!Core!PriorCycleRange(c) :
                     Reduction!Proof!Core!RecoveryInductionStep(i)
              PROOF
                <5>1. TAKE i \in Reduction!Proof!Core!PriorCycleRange(c)
                <5>2. TotalCycles # 1
                      BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne, <3>1, <5>1
                         DEF Reduction!Proof!Core!CycleRange,
                             Reduction!Proof!Core!Core!CycleRange,
                             Reduction!Proof!Core!PriorCycleRange
                <5>3. i \in 1..(TotalCycles - 1)
                      BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne, <3>1, <5>1
                         DEF Reduction!Proof!Core!CycleRange,
                             Reduction!Proof!Core!Core!CycleRange,
                             Reduction!Proof!Core!PriorCycleRange
                <5>4. i \in Reduction!Proof!Core!PrefixAdvanceRange
                      BY <5>2, <5>3
                         DEF Reduction!Proof!Core!PrefixAdvanceRange,
                             Reduction!Proof!Core!Core!PrefixAdvanceRange
                <5>5. QED
                      BY <1>1, <5>4
                         DEF RecoveryRecurringInductionPremises,
                             Reduction!Proof!Core!RecoveryRecurringInductionPremises
              <4>3. QED
                    BY <3>1, <4>1, <4>2
                       DEF Reduction!Proof!Core!RecoveryInductionPremisesUpTo
        <3>3. Reduction!Proof!Core!RecoveryClosedPrefixInductionKernel(c)
              BY <1>1, <3>1
                 DEF RecoveryRecurringInductionKernel,
                     Reduction!Proof!Core!RecoveryRecurringInductionKernel
            <3>4. QED
                  BY <3>2, <3>3
                     DEF Reduction!Proof!Core!RecoveryClosedPrefixInductionKernel
    <2>2. QED
          BY <2>1 DEF RecoveryRecurringClosedPrefixes,
                     Reduction!Proof!RecoveryRecurringClosedPrefixes
  <1>2. QED
        BY <1>1
           DEF RecoveryRecurringClosedPrefixes,
               RecoveryRecurringInductionPremises,
               RecoveryRecurringInductionKernel,
               Reduction!Proof!RecoveryRecurringClosedPrefixes

THEOREM TotalClassicalAgreementFromRecurrenceKernelTheorem ==
  TotalClassicalAgreementFromRecurrenceKernel
PROOF
  <1>1. ASSUME RecoveryRecurringInductionPremises,
               RecoveryRecurringInductionKernel
        PROVE TotalClassicalAgreementHistoryRealized
    <2>1. RecoveryRecurringClosedPrefixes
          BY RecoveryRecurringClosedPrefixesFromRecurrenceKernel, <1>1
    <2>2. TotalClassicalAgreementFromRecurringPrefixes
          BY TotalClassicalAgreementFromRecurringPrefixesTheorem
    <2>3. QED
          BY <2>1, <2>2 DEF TotalClassicalAgreementFromRecurringPrefixes
  <1>2. QED
        BY <1>1 DEF TotalClassicalAgreementFromRecurrenceKernel

====

NestedGuardianRecoveryClassicalAgreementCollapse.tla

Repository path: docs/architecture/protocols/aft/formal/nested_guardian/NestedGuardianRecoveryClassicalAgreementCollapse.tla

---- MODULE NestedGuardianRecoveryClassicalAgreementCollapse ----
EXTENDS Naturals, FiniteSets, TLC, TLAPS

CONSTANT Validators, Witnesses, Blocks, Slots, Epochs, QuorumSize, MaxReassignmentDepth,
         InitialEpoch, InitialWitness, TotalCycles,
         TargetSlotOf(_), TargetBlockOf(_), StableEpochOf(_),
         SmallCommitteeSlot, SmallRecoveryThreshold, LargeRecoveryThreshold,
         SmallRecoveryCommittee, LargeRecoveryCommittee

ASSUME InitialEpochInEpochs == InitialEpoch \in Epochs
ASSUME InitialWitnessInWitnesses == InitialWitness \in Witnesses
ASSUME QuorumSizeInValidatorRange == QuorumSize \in 1..Cardinality(Validators)
ASSUME TotalCyclesIsNat == TotalCycles \in Nat
ASSUME TotalCyclesAtLeastOne == TotalCycles >= 1
ASSUME TargetCycleDomains ==
  \A c \in 1..TotalCycles :
  /\ TargetSlotOf(c) \in Slots
  /\ TargetBlockOf(c) \in Blocks
  /\ StableEpochOf(c) \in Epochs

VARIABLES votes, witnessCerts, finalized, finalizerSets, registryEpoch, guardianReady, witnessOnline,
          witnessCheckpoint, assignedWitness, reassignmentDepth, currentCycle, phase, churnStage,
          continuationBoundary, continuationAnchorPublished, continuationAnchorBoundary,
          continuationPagePublished, continuationPageBoundary, continuationFetched,
          shareReceipts, shareConflicts, windowClosed, missingShareClaims,
          missingThresholdCertificates, recovered, recoveredSurfaces,
          recoveryConflicts, aborted

Totality ==
  INSTANCE NestedGuardianRecoveryClassicalAgreementTotality
  WITH Validators <- Validators,
       Witnesses <- Witnesses,
       Blocks <- Blocks,
       Slots <- Slots,
       Epochs <- Epochs,
       QuorumSize <- QuorumSize,
       MaxReassignmentDepth <- MaxReassignmentDepth,
       InitialEpoch <- InitialEpoch,
       InitialWitness <- InitialWitness,
       TotalCycles <- TotalCycles,
       TargetSlotOf <- TargetSlotOf,
       TargetBlockOf <- TargetBlockOf,
       StableEpochOf <- StableEpochOf,
       SmallCommitteeSlot <- SmallCommitteeSlot,
       SmallRecoveryThreshold <- SmallRecoveryThreshold,
       LargeRecoveryThreshold <- LargeRecoveryThreshold,
       SmallRecoveryCommittee <- SmallRecoveryCommittee,
       LargeRecoveryCommittee <- LargeRecoveryCommittee,
       votes <- votes,
       witnessCerts <- witnessCerts,
       finalized <- finalized,
       finalizerSets <- finalizerSets,
       registryEpoch <- registryEpoch,
       guardianReady <- guardianReady,
       witnessOnline <- witnessOnline,
       witnessCheckpoint <- witnessCheckpoint,
       assignedWitness <- assignedWitness,
       reassignmentDepth <- reassignmentDepth,
       currentCycle <- currentCycle,
       phase <- phase,
       churnStage <- churnStage,
       continuationBoundary <- continuationBoundary,
       continuationAnchorPublished <- continuationAnchorPublished,
       continuationAnchorBoundary <- continuationAnchorBoundary,
       continuationPagePublished <- continuationPagePublished,
       continuationPageBoundary <- continuationPageBoundary,
       continuationFetched <- continuationFetched,
       shareReceipts <- shareReceipts,
       shareConflicts <- shareConflicts,
       windowClosed <- windowClosed,
       missingShareClaims <- missingShareClaims,
       missingThresholdCertificates <- missingThresholdCertificates,
       recovered <- recovered,
       recoveredSurfaces <- recoveredSurfaces,
       recoveryConflicts <- recoveryConflicts,
       aborted <- aborted

CycleRange == Totality!CycleRange

ClassicalAgreementDecision(c) ==
  [cycle |-> c,
   slot |-> TargetSlotOf(c),
   block |-> TargetBlockOf(c),
   epoch |-> StableEpochOf(c)]

ClassicalAgreementHistory(history) ==
  \A i \in CycleRange :
    history[i] = ClassicalAgreementDecision(i)

OrdinaryClassicalAgreementHistory(history) ==
  /\ ClassicalAgreementHistory(history)
  /\ <>Totality!RecoveryClosedPrefix(TotalCycles)

UnconditionalClassicalAgreementSentence ==
  OrdinaryClassicalAgreementHistory(
    Totality!ClassicalAgreementTotalHistoryObject
  )

THEOREM TotalHistoryMatchesCollapsedClassicalHistory ==
  ClassicalAgreementHistory(Totality!ClassicalAgreementTotalHistoryObject)
PROOF
  <1>1. \A i \in CycleRange :
           Totality!ClassicalAgreementTotalHistoryObject[i]
             = ClassicalAgreementDecision(i)
    PROOF
      <2>1. TAKE i \in CycleRange
      <2>2. QED
            BY <2>1
               DEF ClassicalAgreementDecision,
                   CycleRange,
                   Totality!ClassicalAgreementTotalHistoryObject,
                   Totality!Reduction!ClassicalAgreementDecisionObject
  <1>2. QED
        BY <1>1 DEF ClassicalAgreementHistory

THEOREM TotalityCyclePrefixEntriesStayInCycleRange ==
  \A c \in Totality!CycleRange :
    \A i \in 1..c :
      i \in Totality!CycleRange
  BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne
     DEF Totality!CycleRange

THEOREM TotalityReductionCorePriorCycleRangeImpliesPrefixAdvanceRange ==
  \A c \in Totality!Reduction!Proof!Core!CycleRange :
    \A i \in Totality!Reduction!Proof!Core!PriorCycleRange(c) :
      i \in Totality!Reduction!Proof!Core!PrefixAdvanceRange
  BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne
     DEF Totality!Reduction!Proof!Core!CycleRange,
         Totality!Reduction!Proof!Core!Core!CycleRange,
         Totality!Reduction!Proof!Core!PriorCycleRange,
         Totality!Reduction!Proof!Core!PrefixAdvanceRange,
         Totality!Reduction!Proof!Core!Core!PrefixAdvanceRange

THEOREM LocalReductionLivenessFromRecurringPrefixesTheorem ==
  Totality!RecoveryRecurringClosedPrefixes
    => Totality!Reduction!FiniteClassicalAgreementLiveness
PROOF
  <1>1. ASSUME Totality!RecoveryRecurringClosedPrefixes
        PROVE Totality!Reduction!FiniteClassicalAgreementLiveness
    <2>1. \A c \in Totality!Reduction!CycleRange :
             Totality!Reduction!FiniteClassicalAgreementPrefixRealized(c)
      PROOF
        <3>1. TAKE c \in Totality!Reduction!CycleRange
        <3>2. c \in Totality!Reduction!Proof!Core!CycleRange
              BY <3>1
                 DEF Totality!Reduction!CycleRange,
                     Totality!Reduction!Proof!Core!CycleRange,
                     Totality!Reduction!Proof!Core!Core!CycleRange
        <3>3. <>Totality!Reduction!Proof!Core!RecoveryClosedPrefix(c)
              BY <1>1, <3>2
                 DEF Totality!RecoveryRecurringClosedPrefixes,
                     Totality!Reduction!Proof!RecoveryRecurringClosedPrefixes
        <3>4. QED
              BY <3>1, <3>3
                 DEF Totality!Reduction!FiniteClassicalAgreementPrefixRealized
      <2>2. QED
            BY <2>1 DEF Totality!Reduction!FiniteClassicalAgreementLiveness
  <1>2. QED
        BY <1>1

THEOREM LocalTotalClassicalAgreementHistoryFromFiniteLivenessTheorem ==
  Totality!Reduction!FiniteClassicalAgreementLiveness
    => Totality!TotalClassicalAgreementHistoryRealized
PROOF
  <1>1. ASSUME Totality!Reduction!FiniteClassicalAgreementLiveness
        PROVE Totality!TotalClassicalAgreementHistoryRealized
    <2>1. TotalCycles \in Totality!Reduction!CycleRange
          BY SMT, TotalCyclesIsNat, TotalCyclesAtLeastOne
             DEF Totality!Reduction!CycleRange
    <2>2. Totality!Reduction!FiniteClassicalAgreementPrefixRealized(TotalCycles)
          BY <1>1, <2>1 DEF Totality!Reduction!FiniteClassicalAgreementLiveness
    <2>3. <>Totality!RecoveryClosedPrefix(TotalCycles)
          BY <2>2
             DEF Totality!Reduction!FiniteClassicalAgreementPrefixRealized,
                 Totality!RecoveryClosedPrefix
    <2>4. Totality!ClassicalAgreementTotalHistoryExtendsFinitePrefixes
      PROOF
        <3>1. \A c \in Totality!CycleRange :
                 [i \in 1..c |-> Totality!ClassicalAgreementTotalHistoryObject[i]]
                   = Totality!Reduction!ClassicalAgreementPrefixObject(c)
          PROOF
            <4>1. TAKE c \in Totality!CycleRange
            <4>2. \A i \in 1..c :
                     Totality!ClassicalAgreementTotalHistoryObject[i]
                       = Totality!Reduction!ClassicalAgreementDecisionObject(i)
              PROOF
                <5>1. TAKE i \in 1..c
                <5>2. c \in 1..TotalCycles
                      BY <4>1 DEF Totality!CycleRange
                <5>3. i \in Totality!CycleRange
                      BY TotalityCyclePrefixEntriesStayInCycleRange, <4>1, <5>1
                <5>4. QED
                      BY <5>3
                         DEF Totality!ClassicalAgreementTotalHistoryObject
              <4>3. QED
                    BY IsaWithSetExtensionality, <4>1, <4>2
                       DEF Totality!Reduction!ClassicalAgreementPrefixObject
        <3>2. QED
              BY <3>1 DEF Totality!ClassicalAgreementTotalHistoryExtendsFinitePrefixes
    <2>5. QED
          BY <2>3, <2>4 DEF Totality!TotalClassicalAgreementHistoryRealized
  <1>2. QED
        BY <1>1

THEOREM LocalRecurringPrefixesFromRecurrenceKernelTheorem ==
  /\ Totality!RecoveryRecurringInductionPremises
  /\ Totality!RecoveryRecurringInductionKernel
  => Totality!RecoveryRecurringClosedPrefixes
PROOF
  <1>1. ASSUME Totality!RecoveryRecurringInductionPremises,
               Totality!RecoveryRecurringInductionKernel
        PROVE Totality!RecoveryRecurringClosedPrefixes
    <2>1. \A c \in Totality!Reduction!Proof!Core!CycleRange :
             <>Totality!Reduction!Proof!Core!RecoveryClosedPrefix(c)
      PROOF
        <3>1. TAKE c \in Totality!Reduction!Proof!Core!CycleRange
        <3>2. /\ Totality!Reduction!Proof!Core!RecoveryRecurringInductionPremises
              /\ Totality!Reduction!Proof!Core!RecoveryRecurringInductionKernel
              BY <1>1
                 DEF Totality!RecoveryRecurringInductionPremises,
                     Totality!RecoveryRecurringInductionKernel
        <3>3. Totality!Reduction!Proof!Core!RecoveryInductionPremisesUpTo(c)
          PROOF
            <4>1. Totality!Reduction!Proof!Core!RecoveryInductionBase
                  BY <3>2
                     DEF Totality!Reduction!Proof!Core!RecoveryRecurringInductionPremises
            <4>2. \A i \in Totality!Reduction!Proof!Core!PriorCycleRange(c) :
                     Totality!Reduction!Proof!Core!RecoveryInductionStep(i)
              PROOF
                <5>1. TAKE i \in Totality!Reduction!Proof!Core!PriorCycleRange(c)
                <5>2. i \in Totality!Reduction!Proof!Core!PrefixAdvanceRange
                      BY TotalityReductionCorePriorCycleRangeImpliesPrefixAdvanceRange,
                         <3>1, <5>1
                <5>3. QED
                      BY <3>2, <5>2
                         DEF Totality!Reduction!Proof!Core!RecoveryRecurringInductionPremises
            <4>3. QED
                  BY <3>1, <4>1, <4>2
                     DEF Totality!Reduction!Proof!Core!RecoveryInductionPremisesUpTo
        <3>4. Totality!Reduction!Proof!Core!RecoveryClosedPrefixInductionKernel(c)
              BY <3>1, <3>2
                 DEF Totality!Reduction!Proof!Core!RecoveryRecurringInductionKernel
        <3>5. <>Totality!Reduction!Proof!Core!RecoveryClosedPrefix(c)
              BY <3>3, <3>4
                 DEF Totality!Reduction!Proof!Core!RecoveryClosedPrefixInductionKernel
        <3>6. (/\ Totality!Reduction!Proof!Core!RecoveryRecurringInductionPremises
                /\ Totality!Reduction!Proof!Core!RecoveryRecurringInductionKernel)
                => <>Totality!Reduction!Proof!Core!RecoveryClosedPrefix(c)
              BY <3>5
        <3>7. QED
              BY <3>5
    <2>2. QED
            BY <2>1
               DEF Totality!RecoveryRecurringClosedPrefixes,
                   Totality!Reduction!Proof!RecoveryRecurringClosedPrefixes
  <1>2. QED
        BY <1>1

THEOREM UnconditionalClassicalAgreementFromTotalHistoryTheorem ==
  Totality!TotalClassicalAgreementHistoryRealized
    => UnconditionalClassicalAgreementSentence
PROOF
  <1>1. ASSUME Totality!TotalClassicalAgreementHistoryRealized
        PROVE UnconditionalClassicalAgreementSentence
    <2>1. ClassicalAgreementHistory(Totality!ClassicalAgreementTotalHistoryObject)
          BY TotalHistoryMatchesCollapsedClassicalHistory
    <2>2. <>Totality!RecoveryClosedPrefix(TotalCycles)
          BY <1>1 DEF Totality!TotalClassicalAgreementHistoryRealized
    <2>3. QED
          BY <2>1, <2>2
             DEF UnconditionalClassicalAgreementSentence,
                 OrdinaryClassicalAgreementHistory
  <1>2. QED
        BY <1>1

THEOREM UnconditionalClassicalAgreementFromRecurringPrefixesTheorem ==
  Totality!RecoveryRecurringClosedPrefixes
    => UnconditionalClassicalAgreementSentence
PROOF
  <1>1. ASSUME Totality!RecoveryRecurringClosedPrefixes
        PROVE UnconditionalClassicalAgreementSentence
    <2>1. Totality!Reduction!FiniteClassicalAgreementLiveness
          BY LocalReductionLivenessFromRecurringPrefixesTheorem, <1>1
    <2>2. Totality!TotalClassicalAgreementHistoryRealized
          BY LocalTotalClassicalAgreementHistoryFromFiniteLivenessTheorem, <2>1
    <2>3. QED
          BY UnconditionalClassicalAgreementFromTotalHistoryTheorem, <2>2
  <1>2. QED
        BY <1>1

THEOREM UnconditionalClassicalAgreementFromRecurrenceKernelTheorem ==
  /\ Totality!RecoveryRecurringInductionPremises
  /\ Totality!RecoveryRecurringInductionKernel
  => UnconditionalClassicalAgreementSentence
PROOF
  <1>1. ASSUME Totality!RecoveryRecurringInductionPremises,
               Totality!RecoveryRecurringInductionKernel
        PROVE UnconditionalClassicalAgreementSentence
    <2>1. Totality!RecoveryRecurringClosedPrefixes
          BY LocalRecurringPrefixesFromRecurrenceKernelTheorem, <1>1
    <2>2. Totality!Reduction!FiniteClassicalAgreementLiveness
          BY LocalReductionLivenessFromRecurringPrefixesTheorem, <2>1
    <2>3. Totality!TotalClassicalAgreementHistoryRealized
          BY LocalTotalClassicalAgreementHistoryFromFiniteLivenessTheorem, <2>2
    <2>4. QED
          BY UnconditionalClassicalAgreementFromTotalHistoryTheorem, <2>3
  <1>3. QED
        BY <1>1

====

References

1. Maofan Yin, Dahlia Malkhi, Michael K. Reiter, Guy Golan-Gueta, and Ittai Abraham. HotStuff: BFT Consensus in the Lens of Blockchain. arXiv:1803.05069. https://arxiv.org/abs/1803.05069
2. George Danezis, Lefteris Kokoris-Kogias, Alberto Sonnino, and Alexander Spiegelman. Narwhal and Tusk: A DAG-based Mempool and Efficient BFT Consensus. arXiv:2105.11827. https://arxiv.org/abs/2105.11827
3. Ittai Abraham, Dahlia Malkhi, Kartik Nayak, Ling Ren, and Alexander Spiegelman. Bullshark: DAG BFT Protocols Made Practical. arXiv:2201.05677. https://arxiv.org/abs/2201.05677
4. Andrew Miller, Yu Xia, Kyle Croman, Elaine Shi, and Dawn Song. The Honey Badger of BFT Protocols. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. https://eprint.iacr.org/2016/199.pdf
5. Bingyong Guo, Zhenliang Lu, Qiang Tang, Jing Xu, and Zhenfeng Zhang. Dumbo: Faster Asynchronous BFT Protocols. Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security. https://dblp.org/rec/conf/ccs/GuoL0XZ20
6. Alistair Stewart and Eleftherios Kokoris-Kogias. GRANDPA: a Byzantine Finality Gadget. arXiv:2007.01560. https://arxiv.org/abs/2007.01560
7. Jelena Dosenovic, Roger Wattenhofer, and others. Accountable Safety Implies Finality. arXiv:2308.16902. https://arxiv.org/abs/2308.16902
8. Chainlink Labs. Chainlink CCIP's Defense-In-Depth Security and the Risk Management Network. Chainlink blog, 2023. https://blog.chain.link/ccip-risk-management-network/
9. John P. Conley. Proof of Honesty: Coalition-Proof Blockchain Validation without Proof of Work or Stake. Geeq technical paper, version 2.0, 2019. https://geeq.io/wp-content/uploads/GEEQ-OFFICIAL-TECHNICAL-PAPER.pdf
10. Sean Bowe, Jack Grigg, and Daira Hopwood. Halo: Recursive Proof Composition without a Trusted Setup. IACR ePrint 2019/1021. https://eprint.iacr.org/2019/1021
11. Benedikt B{"u}nz, Alessandro Chiesa, Pratyush Mishra, and Nicholas Spooner. Proof-Carrying Data from Accumulation Schemes. IACR ePrint 2020/499. https://eprint.iacr.org/2020/499