This post follows Informed Diffusion: making home builders publish fast (2026).
Author: @cskiraly
Update, 29 October 2026: this post stays as published. Its text is kept current, with the latest results, on notes.ethereum.org, and each version, with its data and scripts, at eth-networking-studies. SEACAST’s specification and its releases are at informed-diffusion-spec; news is posted as replies to this topic.
TL;DR
- Ethereum has more and more large objects to broadcast, and little time for each. Today’s payloads are small and datacenters carry them, which is much of why mainnet is in time, but payloads grow (with gas increase and block-level access lists, BALs) and timelines shrink (with quick slots). Execution proofs and consensus blocks with post-quantum signatures may soon join the large-message club too.
- Today’s delivery method (gossipsub) sits far from being optimal: every node waits for the whole object before passing it on, and receives several copies of it. From a builder at home, the last nodes receive a 1 MiB payload seconds late.
- Not every node needs every byte. With data-availability sampling, a node is to receive its samples of an object, not the object. PeerDAS’s 128 column topics are only one way of doing sampled diffusion; RowDAS and FullDAS are other examples. Moreover, broadcast is just the special case of sampled diffusion in which each node’s sample is the whole object.
- SEACAST (Segmented, Encoded, Availability-sampled broadCAST) is a protocol for handling both sampled diffusion and broadcast. It builds on the principles of Informed Diffusion, the protocol of our last post, and on FullDAS, our earlier design.
- SEACAST is elastic. Cut every uplink from 50 to 10 Mbps, to a fifth, and SEACAST takes under three times as long (1.8 s instead of 0.64), with the same bytes. Gossipsub takes five and a half times as long, 25 s, and sends more.
- SEACAST has an executable specification, which, to the best of our knowledge, none of the protocols it is compared with has. The pseudocode runs as written in a small simulator, and it is checked rule by rule against the Go implementation the post’s numbers come from.
- SEACAST has a formal model. A formal model of the specification checks some of its safety rules. The model is not exhaustive and is still a first version, but it has already allowed us to find gaps in delivery, promise handling and expiry. The model is published with the specification.
- It is measured, across multiple simulators, and against today’s gossipsub and ECBroadcast. SEACAST is faster and lighter than both, on every simulated network. On a network of 50 Mbps nodes, 99 % of the nodes hold a 1 MiB payload after 0.64 s with SEACAST, 0.97 s with ECBroadcast and 4.5 s with gossipsub, and SEACAST uses about 33 % of either one’s bytes. With a datacenter builder, the times are 0.45 s, 0.58 s and 1.6 s, and SEACAST uses about 60 % of ECBroadcast’s bytes and less than 50 % of gossipsub’s.
1. The name, and where it comes from
Informed Diffusion was a description that served as a name: every node learns what its peers hold and sends accordingly. The protocol now does more than the earlier post described, and others are to implement, compare and cite it, so it gets a name of its own, SEACAST:
- Segmented: an object travels as chunks, and a node forwards each chunk as it arrives, before it holds the whole.
- Encoded: the chunks are coded, so that a node needs enough of them, not particular ones. The code is Reed–Solomon today and may change; the E could as well read Elastic, the protocol’s delay and bytes following the bandwidth it is given, as §4 shows.
- Availability-sampled: a node may want a sample of an object rather than the whole, the columns its custody assigns or the cells it samples, and the protocol delivers what each node wants. Every chunk carries its own proof, so a sample is checked on its own.
- broadCAST: from one source to every node that wants the object, or a part of it.
Figure 1: SEACAST in one picture. Left, how a chunk travels: the source sends each chunk to a few peers; a node forwards a chunk as soon as it arrives, pushing it to a few peers (here one more, since the peer it came from already holds it) and announcing it to the rest; a peer that lacks the chunk asks for it, one peer at a time; a peer whose holdings show it already has it gets nothing; and a window sized from the node’s uplink caps its outstanding chunks. Any 4 of the 8 coded chunks rebuild the object. Right, what each node receives: a node’s interest (all of an object, its custody columns, or the cells it samples) is set apart from its duty to forward, as the draft of the next version writes it.
Informed Diffusion remains the name of how SEACAST diffuses, and the earlier post keeps its title. One earlier protocol shares the name: SEACAST, a peer-to-peer video streaming protocol with multiple description coding (Zezza, Magli, Olmo and Grangetto, IEEE ICME 2009). Ours is unrelated to it. Nor is SEACAST EIP-8411 at 41ba25cc, which specifies a smaller protocol, close to SEACAST’s first tier.
Most of SEACAST’s mechanisms are not new on their own; they come from decades of work on distributing content over peer-to-peer networks. Forwarding chunks before the whole is held, and scheduling which chunk goes to which peer, is what P2P live streaming did in the 2000s (SplitStream, Castro et al., SOSP 2003; CoolStreaming, Zhang et al., INFOCOM 2005; PULSE, Pianese et al., 2007), with its trade-offs worked out in theory (Bonald et al., SIGMETRICS 2008; Abeni, Kiraly and Lo Cigno, NETWORKING 2009). Coding the content so that no piece is the last comes from erasure codes for networking and digital fountains (Rizzo, CCR 1997; Byers et al., SIGCOMM 1998). Push and pull have epidemic roots (Demers et al., PODC 1987; Karp et al., FOCS 2000); pushing data eagerly on some links and announcing it lazily on the others is Plumtree’s split (Leitão et al., SRDS 2007), which gossipsub’s mesh and gossip follow. Telling peers what one holds is BitTorrent’s bitfield (Cohen, 2003) and CoolStreaming’s buffer map (Zhang et al., 2005), and sizing what is in flight to the uplink is rate control for P2P streaming (Birke et al., P2P 2011). Delivering each node its samples rather than the whole object, sampled diffusion, comes from our FullDAS design (Kiraly et al., 2024), which built on data-availability sampling (Al-Bassam, Sonnino and Buterin, 2018) and also proposed holding bitmaps for gossipsub. The earlier post’s broadcast was its special case, every node wanting the whole object; SEACAST is the one protocol for both that the earlier post promised. We have found no earlier source for a few of the fourth tier’s rules: a push budget of two; projection; paced gossip; and a push budget set by the node’s uplink. Projection skips a push to a peer expected to reach enough chunks without that push. Paced gossip releases the heartbeat’s announcements one peer at a time. What is new above all is the combination, fitted to Ethereum’s constraints: one source, often at home; a deadline within the slot; nodes that may lie or withhold; a proof on every chunk; and sampling. Segmented payload diffusion, card by card cites the literature behind each mechanism.
2. What it carries
Ethereum has several large objects that one node must get to many, fast: the execution payload, which the earlier post measured at 1 MiB, about three quarters of that once compressed; the data-availability columns and rows of blobs; and, as they come, execution proofs that travel with the block and consensus blocks with post-quantum signatures. Their sizes and deadlines differ, and so does who needs what: every node needs the whole payload, but a node needs only the columns its custody assigns, or the cells it samples.
SEACAST’s next version, in its draft, separates the questions a gossipsub topic answers all at once. A node’s interest is what it wants: the whole object, the columns its node id assigns, or the cells it declares. Its duty is whether it forwards what it receives. Its relations say to whom it pushes and to whom it announces. A subscription bundles all four into one; kept apart, they let a node forward only what it is to forward, and let a sampler receive its samples without joining a topic per column.
SEACAST is not bound to gossipsub. It is defined on its own messages (holdings, a node’s bitmap of the chunks it has; asks; chunks), and a binding maps them onto a transport. The next version’s draft writes out three: SEACAST as a libp2p protocol of its own; SEACAST onto gossipsub, through gossipsub’s Partial Messages extension, which keeps a rollout inside the existing topics; and the wire of the research implementation, a modified gossipsub. Another transport needs only another binding.
SEACAST does not hide the source. Every copy of an object starts at its source. The source’s neighbours can tell which node is the source, as they can in today’s whole-message gossip. In the early draft Hiding the source of a segmented payload (2026), none of the changes tried in how the source sends hides it, and the draft expects none can. It also looks at letting the object enter the network at another node instead.
What is shown, and how. Times below run until a node holds enough chunks to rebuild the object; checking the chunks’ proofs, waiting for the block and decoding are outside them.
- Payloads, measured in the earlier post at about 70 connections per node: on a network where every node is at home (50 Mbps up, 100 down), a 1 MiB payload reaches 99 % of the nodes in about 0.6 s, against 6.3 s for today’s gossip, and each node receives 1.7 copies of it instead of 4.4, control included.
- Data-availability columns, measured on a stand-in: the same mechanisms, given an object type shaped like PeerDAS’s columns in our simulator, deliver each node the eight columns its custody assigns, and forward nothing else. With a 1 Gbps source and every other node at home, 99 % of the nodes hold their columns about 0.7 s after the source publishes, and the median node receives about 1.3 copies of its columns’ data (Figure 2). This is a proxy in our simulator, with checking a cell taken as free, not PeerDAS.
- Sampling, rows and other object types. A draft of SEACAST’s next version is published with this post. In the draft, the object type is an interface the consensus side supplies. The interface gives the indices and the chunks needed, and says how a chunk is checked and decoded. Execution payloads, PeerDAS columns and RowDAS rows (EIP-8371) are written out. Blobs travel as columns and rows. Its small simulator runs payloads, custody, rows and sampling; with half of the columns withheld, the custody and row settings still complete, through supernodes that rebuild or through the custodian links a row member needs. No client or full simulation runs it yet, and its open decisions are listed in it.
Figure 2: the column proxy: SEACAST’s measured version carrying an object shaped like PeerDAS’s columns in our simulator (a block of 32 blobs as 128 columns of 32 cells, each node taking the eight columns its custody assigns), with checking a cell taken as free; not PeerDAS. 500 nodes, a 1 Gbps source and every other node at home (50 Mbps up, 100 down), ten simulated networks. Each small point is one network, the average of the two blocks after the first; each bar is the median over the networks. Left, the time after the source publishes by which half, 90 %, 99 % and all of the 499 other nodes hold all of their columns; right, the data a node receives until then, in copies of its columns, for the median node and at the 99th percentile.
Which version is where. What this post measures, specifies, checks and drafts is not yet one version of SEACAST:
| Version | Run or checked by | |
|---|---|---|
| Measured (Figures 2 to 5) | The research implementation. It lacks the two fixes described in §5 and version 0.5’s fixes. | Prysm with a modified gossipsub library, on a virtual clock. The earlier designs also ran under Shadow. |
| Specified (§5) | Version 0.5 of the protocol text (release v0.6). | The specification’s small simulator. |
| Checked (§6) | Version 0.5, sections 4 to 7, for one object. One penalty rule at any size, under §6’s assumption. | Small instances: Quint and TLC on three or four nodes. The penalty rule’s proof: Veil. |
| Drafted (§2) | The next version: interest and duty, sampling, the bindings. | The specification’s small simulator only. |
3. How it compares
The comparisons below rest on a larger body of simulation: the real Prysm and gossipsub code on a virtual clock, each result named here the median over ten simulated networks. EIP-8411: what segmented payload diffusion is made of (2026) built the first three tiers (chunks forwarded at once; announcements and asks in place of blind pushes; the code) one rule at a time, across payload sizes, thin links, datacenter nodes and withholding. Informed Diffusion: making home builders publish fast (2026) and its companion, Informed Diffusion, measured (2026), added the fourth tier and ran it through lost data, an omitting source, uneven links, every kind of faulty node we modelled up to half of the network, and uplinks thinned to 10 Mbps: every node received every payload after the first within three seconds. EIP-8411 payload segmentation under the Shadow simulator (2026) reran that post’s main comparison in a second simulator, over QUIC and TCP, and on the Linux kernel’s stack; under Shadow, the design it recommended came within 6 % of the first simulator. The fourth tier itself has been measured only in the first simulator, at 500 nodes, with payloads up to 2 MiB. The specification’s own simulator also runs the fourth tier’s rules. §5 describes a rule-by-rule comparison between an earlier version of the text and the implementation. The earlier designs have also run on larger networks, in the first simulator and under Shadow.
Figure 3, from the earlier post (its Figure 1, where every point is explained): the measured design built up one mechanism at a time, from today’s gossip (0) to the fourth tier (16, and 17 with fast nodes), in the all-home network and in the mixed-bandwidth network with a home or a datacenter builder, at about 70 connections per node. Across, the time for 99 % of the nodes (ms, log scale, warm payloads); up, the bytes each node receives, data and control, in copies of the compressed payload (log scale); bars, one standard deviation across the simulated networks; lower left is better.
Broadcast protocols are usually compared across papers, each on its own simulator and link model. We ran three in one: today’s gossipsub, ECBroadcast’s Reed–Solomon mode and SEACAST, on the same links, queues, latencies, graph and payload. ECBroadcast runs on its own engine, unmodified, behind an adapter to libp2p’s streams; only the adapter is ours, and all three run over the same QUIC stack, libp2p’s, inside the simulator.
Figure 4: today’s gossipsub, ECBroadcast’s Reed–Solomon mode and SEACAST in one simulator: 500 nodes with 16 connections each, a 1 MiB payload, ten simulated networks per panel. The all-home network has every node at 50 Mbps up and 100 down; the mixed-bandwidth network has a fifth of the nodes at 1 Gbps, the builder among them. Each small point is one protocol on one network, the median over the five payloads after the first; a grey line joins the three protocols on the same network; the large markers are the medians over the networks. Open circles on a dashed line are the earlier posts’ first three tiers at the same settings (their medians), the steps that lead to SEACAST. Time is plotted on a log scale. It runs until 99 % of the nodes hold enough chunks to rebuild the payload; for gossipsub, until 99 % of the nodes hold the whole payload. Bytes are the average a node receives on the wire until the last node completes. They include QUIC headers and control, so they are a little more than the copies counted elsewhere in this post.
- Against today’s gossipsub, with 16 connections per node: on the all-home network, 99 % of the nodes hold the payload after 0.64 s with SEACAST and 4.5 s with gossipsub, and each node receives 1.3 MiB against 4.2 MiB; with a datacenter builder, 0.45 s against 1.6 s, and 1.7 MiB against 3.8 MiB. SEACAST is faster and lighter on each of the ten networks, on both. The earlier post, at about 70 connections per node, found a wider gap: 0.63 s against 6.3 s on the all-home network, 0.41 s against 1.8 s with a datacenter builder.
- Against ECBroadcast’s Reed–Solomon mode, with 16 connections per node: on the all-home network, 99 % of the nodes hold the payload after 0.64 s with SEACAST and 0.97 s with ECBroadcast, and each node receives 1.3 MiB against 3.7 MiB; SEACAST is faster and lighter on each of the ten simulated networks, and the byte ranges do not overlap. With a datacenter builder the gap narrows, 0.45 s against 0.58 s and 1.7 MiB against 2.9 MiB, and SEACAST is again faster and lighter on all ten. Both cut the payload into coded chunks, forward before decoding and exchange bitmaps; the difference is in what enters flight. ECBroadcast’s sessions span every connection. A node sends each chunk to up to four peers whose bitmaps lack it; the source has no such limit and sends to all its peers. A node cancels sends that a later bitmap makes redundant. It also cancels incoming copies of a chunk it has already accepted. In these runs, most of ECBroadcast’s bytes are duplicates that arrive before a cancellation takes effect. As we read it, the useful chunks wait behind those duplicates. SEACAST pushes to a few peers, announces to the rest and lets each receiver ask for what it lacks, one announcer at a time, under a window sized to the sender’s uplink. The chunk, coding and bitmap settings are ECBroadcast’s benchmark settings. Its own benchmarks connect each node to 8 peers; our simulator runs no fewer than 16 connections per node. Sessions that span every connection matter more as a node’s connections grow. At about 70 connections per node, the earlier post’s setting, ECBroadcast takes 2.2 times SEACAST’s time and four times its bytes on the all-home network, and SEACAST is faster and lighter on each of the ten networks. A sender-side window or sessions on fewer connections would move it toward SEACAST.
- Against our own tiers (Figure 4’s open circles), ECBroadcast falls between the first and second tiers on the all-home network. This holds for both time and bytes on each of the ten networks. With a datacenter builder, its time is close to the third tier’s. In that setting, it uses more bytes than the second or third tier on each of the ten networks.
- Waggle, a libp2p proposal (libp2p/specs#732) for objects reconstructed piece by piece, exchanges pieces with application-defined metadata and uses its view of each peer to decide where pieces go. Its draft leaves byte-level pacing unspecified, and it has no published results; carrying SEACAST’s schedule would mean mapping its asks and its choice of peers onto that interface.
4. Elastic
A protocol for nodes at home must degrade gracefully as links thin: take longer, but in proportion, and spend no more bytes doing so. We ran the three protocols of Figure 4 on the all-home network with every node’s uplink cut from 50 to 25, 20 and 10 Mbps (the downlink at twice that), at 16 connections per node, ten simulated networks at each.
Figure 5: today’s gossipsub, ECBroadcast’s Reed–Solomon mode and SEACAST as links thin, in one simulator: the all-home network, 500 nodes with 16 connections each, a 1 MiB payload, ten simulated networks per point (markers: medians; bars: their range). Left, the time for 99 % of the nodes, against the lower bound the links set (its median over the networks); right, the bytes each node receives on the wire, with a dotted line at one copy of the compressed payload. Below 50 Mbps, gossipsub’s payloads, which take it tens of seconds there, are 40 s apart instead of 12, so successive broadcasts do not overlap. The series are set a little apart sideways so their bars do not overlap.
- SEACAST’s delay follows the bandwidth. The time for 99 % of the nodes grows from 0.64 s at 50 Mbps to 1.8 s at 10 Mbps. For each network, we divide this time by the lower bound its links set for chunked delivery. The median of those ratios over the ten networks stays between 2.6 and 3.2. The source must first send enough distinct chunks to rebuild the payload. Every node that completes needs at least one chunk sent that late. The bound takes the larger of two times: the time those late chunks need to spread by doubling, and the time they need to reach 99 % of the nodes over their fastest paths. Those paths cost about one chunk time per forwarding node. The total upload and each node’s downlink set further floors. The bound is for links that carry only the payload, at full rate from the first byte, and for a scheduler that knows at every moment what every node holds. SEACAST has neither: it pays, in bytes and in time, to learn what its peers hold, which the bound gets for free. How much of the gap that explains is still open; we are measuring it. ECBroadcast’s delay follows too, at nearly five times the bound. Today’s gossipsub falls further behind as links thin, from 22 to 37 times the bound.
- SEACAST’s bytes stay put, at about 1.3 MiB per node on the wire. ECBroadcast’s bytes fall from 3.7 to 2.8 MiB. As we read it, this is because less is in flight on a thinner link. ECBroadcast still uses at least twice SEACAST’s bytes. Gossipsub’s bytes grow from 4.2 to 5.5 MiB. SEACAST is faster and lighter than both on every one of the ten networks, at every uplink.
- The window is what does it. A node keeps in flight only as many chunks as its uplink sends in about 130 ms. In the earlier post’s setting, about 70 connections per node, runs without the window (which also dropped the guard on push targets) had a tail 12 % longer at 50 Mbps and nearly half again as long at 10.
- SEACAST’s bytes do not yet fall with the link: a node waits a fixed 200 ms for an answer before asking another holder, and on a thin link a slow answer is asked for again and both arrive. The next version’s draft scales that wait with the uplink. In the earlier post’s setting, at 10 Mbps, the draft is faster and lighter on every one of ten networks: about 5 % off the tail and 0.2 fewer copies per node. At 25 Mbps it changes little.
We read gossipsub’s slowdown this way. Each node forwards the whole payload to all its mesh peers at once. The copies share the node’s uplink, so each takes longer. The notice that a peer already has the payload arrives after the node has started sending that peer a copy.
5. A specification that runs
Gossipsub’s specification is prose; Ethereum’s networking specification is prose with some helper functions, beside a consensus specification that runs as Python; ECBroadcast has prose specifications and Go code, and Waggle a draft specification and a prototype. In none of them does the text run as the protocol. SEACAST’s specification, Informed Diffusion: the protocol in pseudocode (release v0.6 of the repository, whose protocol text is version 0.5), writes every rule as Python-like code, in the style of the consensus specs, with the wire fields and the constants beside it. A small simulator in the same repository takes the document’s code blocks in order and runs them once per simulated node, so the document is the program: change a rule, and the next run executes the change. It needs nothing but Python:
cd toy
python3 run.py --net home --seed 7 # 500 nodes, all at home, six payloads
python3 check.py # the document still behaves as recorded
check.py runs twelve small networks and compares a hash of every event each node processes with a recorded one, so an edit meant to change nothing is seen to change nothing, and one that changes behaviour shows where. The next version’s draft runs in the same simulator.
The simulator is a check of the text, not a measurement; the numbers in this post come from the research implementation (Prysm with a modified gossipsub library) in a simulator of its own. We compared an earlier version of the text with that implementation on the same networks. We loaded the implementation’s topology into the specification’s simulator and counted each rule’s actions on both sides. We checked the same invariants: no node goes past its push budget or its window, and no second ask for a chunk is made while the first is open. Twice it was the implementation, not the text, that was wrong: a stale ask erased a newer holding, and the source sent each mesh peer a holding per chunk, 128 of them, where the text had one. Both were fixed to match the text; the code behind this post’s figures does not have those fixes yet. Most remaining differences come from the simpler transport in the specification’s simulator, which takes every write at once. Some differences remain unexplained. The simulator’s nodes send about a fifth fewer holdings than the implementation’s nodes. With a datacenter builder, the specification’s simulator has a shorter tail.
6. A formal model, checked on small instances, and one rule proved at any size
We wrote sections 4 to 7 of the specification, for one object, as a model in Quint, and checked it by random simulation and, translated to TLA+, with the TLC model checker. The model leaves timing free: a link delivers and a timer fires at any moment, so every interleaving is a schedule the checker may pick. The instances are small: three or four nodes and an object of at most two data and two parity chunks, with and without an adversary that forges chunks, withholds them, equivocates or sends an inconsistent code.
Safety. For each property below, the checks that apply found no violation. Random simulation used up to five thousand traces per configuration, and twenty thousand where a case is rare. TLC searched the three-node triangle: every state at one data chunk, and to a bounded depth at two. Some properties also had monitors on the simulator’s own runs of the text. The table in formal/ says which check covers which property.
- no honest node is penalised by another honest node, and a forged chunk counts only against its forger;
- no ask leaves for a chunk the node holds, after it has stopped pulling, or past the object’s lifetime;
- a node’s window of chunks in flight keeps its slots and loses no wake-up;
- the source’s holdings name only chunks it has sent, apart from each peer’s first chunk just ahead of its push; this removes one certain sign of which node is the source;
- once an object is dropped, nothing of it but holdings is sent.
The smallest instance is a triangle with one data chunk, where a node’s sending of all it can to one peer is taken as a single step. For this instance, TLC explored every reachable state (3.3 million). It showed that, under weak fairness, every run ends with every node complete. Nobody asks in that instance, and nothing expires or disconnects. The asking rules therefore rest on the bounded search and the simulation. The rules for refused copies, closed connections and expiry rest on the simulation. The wire’s arithmetic (chunk sizes, lengths, proof and bitmap bounds) was checked for every data-chunk count up to 128 and every compressed length in Snappy’s range.
One rule at any size. The checks above stop at four nodes. Suppose a peer claims a chunk to a node on their connection, then asks that node for the chunk. One rule penalises the peer in this case. Under the assumption below, we also have a proof that this rule never penalises an honest node. The proof covers any number of nodes, objects and chunks, and every interleaving.
The proof uses an inductive invariant in Veil, a framework for verifying distributed protocols in the Lean proof assistant. Lean’s kernel checks every obligation. The solver’s answers are rebuilt as proofs rather than trusted. In the model, a transport may coalesce RPCs, objects expire and connections close. Every lifetime may end at any time, with one exception. The proof assumes that a node keeps an expired object’s id until none of that node’s claims for the object remain. While it keeps the id, the node does not take the object up again. Version 0.5 does not ensure this assumption. To meet it, the specification could keep the id longer than any claim can last, or never take an expired object up again.
Each of the rules the proof rests on is needed. Without the writer’s filter on queued asks, Veil finds a run in which an honest node is penalised. It also finds such a run if IDONTWANT is handled before IWANT, or if RPCs are handled out of order, and again if both of version 0.5’s expiry rules are absent. Version 0.4 lacked both expiry rules. Two other reasons for a penalty are outside the proof: a chunk that fails its check, and a malformed holding.
Liveness is where it found problems. The model found ten gaps in delivery, promise handling and expiry. The first was a push the sender skipped but still counted, so that its target was never offered the chunk: a triangle, a ring or a node with one peer never completed. Version 0.5 fixes eight of the ten. Two stay open, with candidate rules: a node that switches from the proposer’s other block to the builder’s block, and a new connection that is never offered what the old one lost. How often the ten bite in a real network is not measured, and the implementation the numbers in this post come from predates the fixes; the specification’s §9 lists what it lacks.
The limits are those of small instances: no exhaustive check at two data chunks has completed, and the model does not include heartbeat gossip, several objects at once or restarts. The model, its instances, and a table of every property with how it was checked are published with the specification (formal/), and the proof beside them (formal/veil/).
