Six Birds Verified IX: Closed Networks

In plain words

Put a controller and a plant in a loop, joined by channels that sometimes fail. Each part is easy to specify alone, but each specification assumes something about the others, and "A works if B does, B works if A does" proves nothing. This paper builds such a loop exactly for a small finite system. Each stage receives the actual output of the stage before it, so every assumption is discharged by a real input, never by a circular guess. Success probabilities come out exact. The worst cases are one half, three eighths and one quarter for clean, noisy and erasing channels with fresh random tickets.

Two habits run through the paper. A failure keeps its probability and is never quietly deleted. Whether a program read hidden data depends on what it actually consulted, not on what it returned: a program that reads a secret and outputs a constant still read the secret. One example shows why the law of each ticket must be stated. Correlating the tickets while each stays uniform on its own drops the noisy case from three eighths to one quarter. The same channel can also carry a short program that repairs the receiver's view, and a committed recipe keeps working after the sender is gone.

The second part closes the loop through a delay register. The wiring is a cycle, yet the order of events in every run has no cycle. If the scheduler may insert at most one wait between two services, a long enough run commits or faults within fourteen steps. For each fixed local policy, the paper computes the largest set of states that stays safe whatever the scheduler does and whatever outcome occurs. For one policy that set has 944 states inside a checked region of 964. Lean 4 formalizations accompany both parts.

What it shows

• Noncircular composition: each stage's assumption is met by an actual earlier input or by the stated start.
• Exact acknowledged success probabilities, and proof that uniform tickets alone do not fix them.
• Access is decided by the consultations a program makes, not by its output.
• A cyclic wiring with acyclic event order, and a bound of fourteen steps when waits are limited to one.
• Robustly safe states computed as a greatest fixed point; 944 for the complement policy.

What it does not claim

The 944 states are the exact safe set inside a declared closed region, not the safe set of the whole ambient network. Receipts do not show that events physically happened or that a random source really is uniform. Eventual fairness alone bounds no response time.

Cite

Tsiokos, I. (2026). Six Birds Verified IX: Closed Networks. Zenodo. https://doi.org/10.5281/zenodo.23097932