TL;DR
- The cross-domain state preservation proofs are closed. Four results, state-preservation homomorphism, functor completion, a natural-transformation tower over the sync degrees, and unconditional bounded convergence, stand on one another inside a single entry. Ten theory files, not one
sorryoroops. - What this article records is not the process but what closed and what it was for. The short version: these theorems are a safety specification for the product, a basis of assurance for institutional asset operation, and an asset for formal verification. Those are not three things. They are three faces of the same theorem.
- The road was not smooth. Closing theorems took less time than checking whether a closed theorem says what we claimed. At one point the whole functor tower turned out to be trivial. True, and saying nothing. Making it a genuine functor cost 295 lines.
- These are the old traps of the field. Vacuously true theorems, degenerate witnesses, idle assumptions all pass the prover while saying nothing. The first external comment our entry ever received landed on exactly that point.
- Every correction that mattered went against us. We withdrew deadlock freedom as unproved, deleted dead ownership fields despite ownership being core to the product, and rebound the liveness witness inside the roster. Each retreat left the remainder firmer.
- It is all in the public repository. Not a request to be trusted, but a result anyone can build and check.
The earlier post, Three Category Axioms, One Proved Functor, deferred one thing at its close. There is a separate place to lay out, in order, what was proven and what it means, and which assumptions still remain. This is that place.
The two posts before this recorded process. A reserved keyword that broke seven builds, a finiteness wall that forced the natural transformation to be redefined, a belief that the glue predicate gives validity that turned out wrong in front of the code. Records like that have their own worth, but they leave one question unanswered. What ended up in hand?
This article answers it. It puts the four results of the cross-domain state preservation proofs side by side as one body and says what they mean for the product, for the industry, and for the field. And why a team building a product came this far.
Why the Four Are One Body
One misreading needs clearing first. The entry holds several theorems, but they are not a list of independent achievements. The later ones stand on the earlier ones, and the earlier ones only acquire their meaning once the later ones exist. Laid out in order, that structure shows.
Where the Cross-Domain State Preservation Proofs Begin
At the base sits the result that one domain’s transition is faithfully reflected in another. When a regulatory action fires on one chain, every connected chain holding that asset reaches the same regulatory state with the structure of the transition preserved (regulatory_homomorphism). This was the starting point of the whole series, and it has since widened in three directions.
First, from a single action to arbitrary action sequences (sequential_preservation). Naturality holding for one step and naturality holding across a whole sequence of steps are different claims. You need the latter before you can talk about a real asset lifecycle.
Second, the failure direction is preserved too (sequential_preservation_none). If a transition is impossible on one side, it is impossible on the other. Without this, an asymmetry opens where one domain accepts an action another domain refused.
Third, synchronization is isolated per asset (sync_isolation). Synchronizing one asset does not touch the state of another.
Onto this attaches the irreversibility of regulation. Confiscation is absorbing (confiscated_terminal), reachable from every non-terminal state (confiscate_universal), and no transition maps a state to itself (no_self_loops).
Functor Completion: Where a Title Becomes a Theorem
Above it sit three category axioms. preservation_id, preservation_compose, preservation_assoc. With these closed, the word functor moved from rhetoric in a title to a proposition the code forces. The earlier posts covered that story, so only the result is cited here.
Where the completion earns its keep does need saying. The evidence that composition is used in earnest is in the code.
theorem daml_to_chain_b_composed:
"state_preservation daml_states escalation_actions daml_transition daml_terminal
reg_states chain_b_actions chain_b_transition reg_terminal
(id ∘ daml_to_reg) (escalation_action_map ∘ id)"
using preservation_compose[OF daml_to_reg_escalation_bridge
escalation_preservation_bundle] .
From a DAML permission record through a regulatory state to another chain’s action vocabulary, three heterogeneous domains joined with no fresh naturality argument. The point is that the proof body ends in a single application of preservation_compose. With a composition law in hand, you stop re-proving naturality every time you lay a new bridge. That is how functor completion actually earns its living.
valid_state premise. BFT threshold and fair leadership are carried by the locale context.Figure 1: The four results and the order in which they stand on one another
The Degree Tower: What It Means for a Hierarchy to Cohere
Third is the sync degree hierarchy raised into a tower of functors. A preservation functor sits at each degree, and degree demotion is defined as a natural transformation between them (degree_natural_transformation). Demotion discards information, which lines up with the direction in which ADS_Functor‘s blinding was lifted to the state level.
What decides things here is composition closure.
theorem nt_compose:
"natural_transformation (F (Suc (Suc k))) (F k)
(degree_forget (Suc k) ∘ degree_forget (Suc (Suc k)))"
This theorem is what makes the S₃ ⇒ S₂ ⇒ S₁ ⇒ S₀ ladder one coherent hierarchy rather than a loose collection of pointwise forgetful maps. Without a guarantee that descending two rungs equals descending one rung twice, the word “hierarchy” is not available.
What each degree’s functor is a functor over turns out to be decisive. Regulatory action sequences form a free monoid, the degree-k functor acts on whole action words, and the naturality of the forgetful map holds beyond a single generator, across the entire action category (degree_forget_natural_run). How it came to take that shape comes later. The point for now is that without it the tower is a shell.
This is also exactly where we part from ADS_Functor. Lochbihler and Marić proved that functors are closed under composition. But a hierarchy of functors and the natural transformations between them is territory that entry did not enter. Sitting on the same axis and standing on ground they did not walk are different claims, and our contribution is the latter.
One thing to be clear about. What this hierarchy actually blocks inside the product is not this article’s subject. The four processing paths and the type-level enforcement were covered in Sync Degree Enforcement: What Turns a Classification Into a Constraint. What is discussed here is the mathematical object that enforcement stands on.
Unconditional Bounded Convergence: The Premise Comes Off
At the top sits what the first article of this series promised. What the two completed properties gave was conditional safety. Start from a valid state and you stay valid after synchronization. Initial validity was a premise.
The convergence result takes that premise off.
theorem oraclizer_guarded_bounded_convergence:
assumes fin: "finite_domain gs⇩0"
and unlocked: "no_locked_without_reason gs⇩0"
shows "∃t ≤ oss.convergence_bound gs⇩0. ∃gs⇩t.
oss.evolves_to gs⇩0 t gs⇩t ∧ valid_state gs⇩t"
There is no valid_state gs⇩0 among the assumptions. Starting from an arbitrary inconsistent state, a valid state is reached within a bounded number of steps. This is the shape of result the self-stabilization literature deals in, and why it matters for regulatory infrastructure is plain. Systems do not always start clean.
Honesty is owed at one point here. The statement above shows no Byzantine threshold and no fairness assumption. They did not vanish; they moved. Those assumptions are carried by the converging_composition locale and the dquencer_liveness context it lives in, and the theorem is read inside that context. Assumptions descending from a theorem header into a locale is ordinary structuring in formal verification, but for anyone citing it, the shape invites the misreading that the assumptions got weaker. So, stated plainly: this convergence is unconditional under the BFT threshold and a fair-leadership assumption. It is unconditional in initial validity, not in the network.
The VRF probability argument is not formalized. A deterministic fairness_bound stands in its place. This is assume-guarantee reasoning that abstracts probabilistic leader election into a deterministic residue, and calling it a “network-level liveness guarantee” would be an overstatement.
The Hard Places
Listing results is easy. But the work that consumed the most time before this list existed was not closing theorems; it was checking whether a closed theorem says what we claimed. Several corrections came out of that, all of them against us, and looking back they are what made the remainder solid.
When the Functor Was Trivial
Start with the one that stung. Tower built, natural transformation proved, composition closure closed, and we believed we had a functor tower. The build passed and the theorems were true.
Then, rereading what that functor was defined over, the actions were bare indices. No identity, no composition. If the morphisms between objects carry no structure, a functor over them has nothing to preserve. The functoriality obligations were not being met automatically. There was nothing being asked in the first place. And the natural transformation was proving only a single-step square. Naturality holding for one generator and naturality holding across the category are different statements.
Mathematics calls this trivial. True, and saying nothing.
To anyone who has done formal verification, the trap is familiar. In a locale with nothing satisfying its assumptions, anything follows; a system with n = 1 and zero Byzantine nodes satisfies any BFT threshold you like; an obligation whose premise is always false is never checked. All true, all passing the build. Recognizing a vacuously true proposition is the oldest homework in this field, and the first comment our entry received when it first went out for external review landed on precisely that.
So the problem was not that we did not know the trap. We knew it and still failed to recognize it in another guise. We had understood it as an instance problem, and we had filled in nineteen instances. That the morphism side of a functor could be the empty part never occurred to us.
Ship it in that state and what happens? The title says “functor tower,” and a reviewer who reads the definition twice sees the shell. The very thing we wrote about in an earlier post, turning “Functor” from rhetoric into a theorem, we were doing again one level up.
There were two options. Leave it trivial and lower the sentence, or make the functor real. We took the second.
We gave the actions a free monoid structure. A sequence of regulatory actions is the composition, and the empty word is the identity. Then the degree-k functor has to act on whole action words, and whether that action survives passage through the broadcast and degree structure has to be proved.
lemma deg_run_collapse:
assumes "get_reg_state gs 0 aid = Some s0"
shows "deg_run k aid (a # w) gs
= (case reg_run s0 (a # w) of None ⇒ None
| Some sn ⇒ Some (broadcast_le k aid sn gs))"
The result says that a whole word of degree-k synchronizations equals broadcasting the composite regulatory state once. Whether that is trivial is settled by trying to prove it. The overwrite property of nested broadcasts would not close under auto and needed a structural proof, hub tracking had to be established as its own lemma, and the induction consumed both. Trivial things close automatically. That it did not close was itself the evidence that it was not trivial.
Then the identity and composition laws attached (deg_run_Nil, deg_run_append), naturality rose from the generators to the whole category (degree_forget_natural_run), and a non-degeneracy witness landed showing that the two-action word FREEZE then CONFISCATE yields a different result from a one-action word (deg_run_nondegenerate). Plus 295 lines, with not one prior theorem changed.
There is a lesson in this. “It is proved” and “it proves something” are different. A trivial theorem passes the prover too. That there is no sorry, that the build is green, says nothing about this distinction. The machine checks only whether the proposition we stated is true; whether that proposition is worth stating, it does not check. That judgment stays with people to the end. This series has told several stories of the prover correcting our intuition. This time it ran the other way. The place where the prover raised no complaint was the most dangerous one.
Deleting the Ownership Fields
The second is short but a principle rides on it.
The asset record carried an owner field and a lock field. A full sweep showed nobody read them. Written, never read. The lock side duplicated the global lock map, and the owner side was referenced nowhere.
An objection arises naturally here. Ownership is a core product concept. The Oracle Session is keyed on the owner, and confiscation and recovery are transfers of ownership. Is deleting that acceptable?
We deleted it. The reasoning settled like this. That ownership matters in the product is a reason to model ownership properly later, not a reason to keep a dead field now. A field nobody reads is not modeling ownership. It is pretending to. And that pretense gives the reader precisely the wrong impression: that this model handles ownership.
Deleting only the fields broke the build, because nine construction literals were writing to them. So the nine went too, and the build passed. That it passed is the demonstration that all nine were write-only. The asset record shrank to two fields, the asset identifier and the regulatory state.
The same principle applied elsewhere. There was machinery for timeout-based lock expiry that ran only over an abstract time model, with not a single theorem connecting it to the actual lock. A structure that advertises and cannot deliver. 135 lines went, and this is the other face of the same event as the deadlock withdrawal below.
Keep something dead because you might use it later and what remains is not code but debt. Better to delete now and build it properly when it is needed.
Withdrawing Deadlock Freedom
The largest withdrawal. Dealing with the second property, we had spoken of determinism, deadlock freedom, and starvation freedom together. Deadlock freedom is now absent from that claim.
The reason came from looking at the model again. The atomic synchronization model has no contending lock holders. gs_locks is one boolean per asset, and neither time nor interleaving exists in the model. Stand “no deadlock occurs” on such a model as a theorem and the theorem is true, but it becomes a sentence claiming more than the model supports. Proving deadlock freedom where deadlock has no structure to arise from is, strictly, not proof but tautology.
So the generic locking machinery came out of the corpus and the second property was restated as determinism and starvation freedom. Deadlock stepped down from being a theorem and stayed as a scope note. Forced lock release under contention belongs to follow-up work on preemptive locking.
The retreat bought something. The boundary between the two remaining claims got sharper. Determinism is carried by select_highest_deterministic and starvation freedom by starvation_bound. Each stands on its own theorem, with no third claim wedged between them that the model does not support.
When a Name Was Inflating a Sentence
The third concerns a name. For a while the theorem covering safety and liveness together carried the name combined safety-liveness. Follow what it actually does, though, and the proof body uses only the safety side. It never invokes the liveness interpretations and makes no Byzantine or determinism claim of its own.
A name larger than its content gets misread by whoever cites it. So we matched the name to the content. That theorem is now conditional_safety_preservation, and it says exactly that: conditional safety. From a valid, unlocked state, synchronization succeeds and the result is valid.
theorem conditional_safety_preservation:
assumes valid: "valid_state gs"
and current: "get_reg_state gs source aid = Some s"
and trans: "reg_transition s action = Some s'"
and not_locked: "¬ is_locked gs aid"
shows "∃gs'. sync source action aid gs = Some gs' ∧ valid_state gs'"
Not a character of the statement changed. Only the name did. And the rename surfaced the fact that the real fusion is elsewhere. The place where safety is freed of its initial-validity hypothesis and genuinely meets liveness is the bounded convergence theorem above, not this one. That is what to cite as the headline.
Where the Strength of Monotonicity Actually Was
The fourth is on the degree hierarchy side. We had a picture in which monotonicity stood as one theorem and grounded the hierarchy. Following the code, the picture did not fit.
Validity preservation holds independently of degree (processing_preserves_validity). Attach a provisioning hypothesis to that and state it so it looks like monotonicity, and the hypothesis does no work in the proof. A theorem with an idle premise looks stronger than it is when cited.
The real strength was in a pair.
theorem over_provisioning_guarantees: assumes deg: "asset_degree aid ≤ d" and val: "valid_state gs" shows "guarantees_preservation d gs aid" theorem no_downward_safety: assumes "asset_degree aid > system_degree" shows "¬ (∀gs. guarantees_preservation system_degree gs aid)"
In the positive direction the provisioning hypothesis actually does work, and the negative direction constructs a concrete counterexample state where ACTIVE and FROZEN diverge, showing a state exists that defeats every preservation guarantee. The ground on which the hierarchy carries force is these two theorems standing together, not one name reading “monotonicity.” Once the name came down from theorem to auxiliary fact, what to cite became clear.
When the Liveness Witness Lived Outside the Roster
The latest correction, and the subtlest.
We were showing that the liveness locale is not vacuous, that a schedule satisfying its assumptions exists, by way of a witness. Look closely at that witness and the range of the schedule was not tied to the node roster. A schedule constant on one honest node satisfies the fairness condition. Even if that node is a ghost outside the system.
Why does that matter? We were saying the Byzantine threshold (n ≥ 3f + 1) holds this result up. But if out-of-roster schedules are admitted, a witness can be built without going through the threshold at all. We were invoking the threshold as grounds while it was carrying nothing. The build passes. The theorem is true. The sentence was simply stronger than the theorem.
One line, and the witness had to be a schedule drawn from the system’s own roster. Only then did the Byzantine threshold start doing any work.
The fix strengthened the conclusion.
theorem liveness_inhabitable:
"∃(ls :: nat ⇒ node_info) (pc :: nat ⇒ nat).
range ls ⊆ nodes ∧ dquencer_liveness nodes f_max fairness_bound ls pc"
range ls ⊆ nodes. With that line attached, the witness must be a schedule drawn from the system’s own roster. And where does the guarantee of an honest node inside the roster come from? From the Byzantine threshold (honest_majority → honest_nonempty). Only then did the threshold begin doing work.
What we did here was not add an assumption but strengthen a conclusion. Adding a hypothesis to narrow a theorem is a retreat; adding a conjunct to the conclusion is an advance. The same problem could have been blocked the first way, but that would have been weakening the theorem to save the sentence.
In the same spirit we built a non-degenerate witness. The locale is instantiated on the tight bound 4 ≥ 3·1 + 1, with n = 4, f = 1, and one real Byzantine node (bft_quorum). Escaping vacuity through a degenerate f = 0, n = 1 case and escaping it in a quorum with an actual Byzantine node carry different weight.
The same pitfall showed up once more in that witness. The pending-request count started as constantly zero, which makes the premise of the obligation “an honest node makes progress” always false. The obligation never fires, so it is vacuously satisfied. Changing the count to a function decreasing each epoch made the premise true and the strict-decrease obligation start being checked. One argument.
A threshold that gets bypassed, an obligation that never fires, a functor with nothing to require. These three have one name. A vacuously true proposition. Anyone who has done formal verification for long will smile here. This is not a newly discovered trap but the oldest one in the field, and the first sentence that came back when our entry first went out for external review was the observation that theorems in an uninstantiated locale are close to vacuously true. We understood it then as an instance problem. That the same illness reappears with different faces in a functor’s morphisms, in a witness’s range, and in an obligation’s premise, we learned afterward.
Here too there is a place we stepped back. The scope of what the threshold contributes to this result is narrow. The headline convergence theorem consumes the fairness assumption directly and does not route through this witness, and honest majority beyond non-emptiness is not consumed. Writing that scope down precisely beats hanging the threshold on the headline.
Figure 2: Five faces of vacuous truth, and what each correction left behind
A Zero That Is Filled In
That sorry and oops count zero gets cited often and means little by itself. Theorems in a locale with no instances are vacuously true. With nothing satisfying the assumptions, anything follows from them.
That observation is also what the editor sent us on our first submission. So we set a standard for the cross-domain state preservation proofs: zero open gates has to mean a zero filled in with content.
The entry now carries nineteen interpretations. Every generic locale is instantiated with a concrete object, and not only inside the regulatory domain.
One deserves separate mention. External_Instance covers preservation between the TCP connection state machine (a subset of RFC 793) and Linux conntrack. A domain with nothing to do with regulation. And that file does not import Regulatory_Instance. It takes only the generic locale layer and the proof automation.
What does that prove? It is the code showing that the framework carries no hidden regulatory assumptions. Anyone can write the sentence “our framework is general.” When an instance that imports not one line of regulatory vocabulary closes over the same locales, the sentence becomes a checkable fact. Down to the reuse of the action-scoping pattern and the layer-crossing pattern outside their original domain.
The counterexample regression lemmas serve the same end. guard_is_load_bearing presents, in four parts, the state where naturality breaks if the guard is removed, and rogue_join_excluded shows an inconsistent merged state is excluded by the glue predicate. These lemmas do not make the theorems stronger. They nail the boundary in place permanently. If someone later mistakes the guard for an optimization and strips it, the build stops.
Proof automation attaches here (Eisbach methods such as discharge_preservation). It closes instance obligations without repetition, and it has one property that matters for trust. A method can only fail; it cannot forge a pass. More automation does not enlarge the trusted base.
Regulatory Irreversibility Closes the Recovery Path Too
One result deserves its own place. It did not appear in the earlier posts.
The convergence theorem says an arbitrary inconsistent state goes to a valid one. But what that recovery path does to get there is a separate matter. Taken to an extreme, confiscate every asset and the state becomes consistent. Demand consistency alone and such a recovery is legitimate.
So the recovery path needed a proof of its own.
theorem recovery_no_fresh_terminal:
assumes carr: "gs⇩0 ∈ oss_carrier"
and nt: "¬ terminal_present gs⇩0 aid"
and ev: "oss.evolves_to gs⇩0 t gs⇩t"
shows "¬ terminal_present gs⇩t aid"
For an asset with no confiscation on it, self-repair cannot invent one. The other direction is closed as well, so the recovery process cannot revive an already confiscated asset either.
From a regulatory standpoint this is the point. Confiscation is a legally irreversible disposition, and if so, the system repairing itself must neither manufacture a confiscation that was not there nor erase one that was. That regulatory actions are preserved on the normal path and that they are preserved on the failure-recovery path are different claims. Without the latter, “we were recovering” becomes an excuse for a regulatory breach.
What Were These Theorems For?
That covers what closed. Now the second question.
We are a team building a product, not a formal methods lab. And still we stayed with this proof a long time. Why, in three layers, with the point of this section being that the three were never separate goals.
Product: Having an Answer Key
A verified model becomes the implementation specification for its corresponding component. That is the most direct benefit.
State-preservation homomorphism and its extensions say what OSS’s cross-domain state transitions must satisfy. Determinism and starvation freedom are the specification for the D-quencer consensus core. The two directions of the degree hierarchy say which routings the Sync Degree Router must admit and which it must refuse. The absorbing property of regulatory actions and the recovery invariant say what the RWA Registry must hold.
Why does that differ? Implement without a specification and the standard of correctness becomes the implementation itself. Tests check the scenarios we thought of and not the ones we did not. With the specification standing as a theorem, the standard lives outside the implementation. When implementation and specification diverge, there are grounds to say the implementation is wrong.
The assumptions of the proof do not simply vanish either. They become conditions the runtime must guarantee. The atomic synchronization assumption is something the BVC pattern must hold to, and the fair-leadership assumption is something VRF leader election must actually satisfy. Writing assumptions down explicitly is an act of humility and at the same time a requirements list handed to the engineering team.
Industry: Not Trust Us, But Check It
Institutions fail to cross from tokenization pilot to production for several reasons. One of them is regulatory-consistency assurance. In a pilot it suffices to demonstrate “here is how it behaves,” but the moment real assets go on, the question changes. “Under what circumstances does this break?”
Test results cannot answer that. Tests show the cases that passed; they do not show the absence of failing ones. Audit reports are the same. They show the vulnerabilities found, not that none exist.
A machine-checked proof answers differently. Inside the model, under stated assumptions, the property holds for all states. And since the assumptions are stated, the answer to “under what circumstances does it break” comes with it. When the assumptions fail.
The subject itself, preservation of regulatory effect across heterogeneous domains, hangs on this. Public chains, institutional ledgers such as Canton, and off-chain systems each carry different verification regimes. The proposition that a regulatory action is atomically preserved across them, guaranteed mathematically, is an answer to the kind of question institutional participants actually ask.
That the Canton connection exists as a fact of code attaches here. Our functor layer genuinely imports Lochbihler and Marić’s merkle_interface and calls its lemmas in proof bodies. Precisely, in one file, Functor_Laws.thy. Across the submission it is a ROOT dependency, but the place bearing mathematical load is that file, and blurring the distinction would be an overstatement. On top of it, the authenticity of Canton transaction trees and selective disclosure are handled down to recursive faithfulness, and the ADS composition laws are lifted to the state level (cdsp_ads_compose, cdsp_ads_merge_assoc).
Academic: Which Ground Was Unwalked
Measure the contribution honestly and it has three axes.
The number of heterogeneous domains. ADS_Functor handles the authenticity of data structures within one domain. We handle preservation of state transitions across N domains with differing verification regimes. Same functor language, different axis.
Fusing safety with Byzantine liveness. Plenty of work proves each separately. Freeing safety from its initial-validity hypothesis inside one corpus and joining it to a fairness assumption in a Byzantine setting to close as bounded convergence is uncommon.
A natural-transformation hierarchy. Stacking a tower of functors and the natural transformations between them on top of composition closure. As written above, that region is one ADS_Functor did not enter.
To avoid overstating, something belongs alongside. What we proved is a model. What Isabelle/HOL checked is the abstract model of a design specification, not the Rust implementation. Refinement between model and implementation is a separate track and has not been done. “Proved” is not “the system is safe.” This series has repeated that sentence many times, and it repeats here.
Three Out of One Theorem
Now the point of this section. The three above are not three projects. They are the same theorem read from three directions.
Take the over_provisioning_guarantees and no_downward_safety pair. Academically it is the result that a hierarchy organized by a reduction relation is formally well defined. Industrially it is the basis for judging whether the system actually meets the synchronization strength an asset demands. For the product it is the specification of which pairings the router must refuse. One theorem, three faces.
recovery_no_fresh_terminal is the same. Academically a self-stabilization result carrying an added terminal-faithfulness condition, industrially the assurance that the legal irreversibility of confiscation survives failure, and for the product the invariant the recovery routine must hold.
This is why we stayed with the proof. Were product safety, industrial assurance, and academic contribution to come from separate places, we would have had to pick one of the three. The argument that a product team is better off writing code than papers is correct in that case. But if the three come out of the same theorem, the story changes. Closing one theorem pays in three directions.
We argued earlier, in From Isabelle/HOL to Compliance-Aware Infrastructure, that RWA infrastructure has to move toward formally verified rules. An argument carries an obligation. If we believe that standard is right, we should be the first to meet it. This entry is the record of paying that obligation. Without evidence that the one arguing did the thing, the argument is just advice.
Figure 3: Reading one theorem at three layers
What Remains
Close by writing down what did not close. A proof report that does not say what it failed to prove is only half honest.
The atomic synchronization assumption still stands. An intermediate state propagated to only one domain is outside this model. Releasing this assumption belongs to subsequent properties, and when it releases, the atomicity assumption weakens for the functor laws and the degree hierarchy together.
Fair leadership is not removed entirely. Abstracting VRF’s probabilistic character into a deterministic bound is its present form; refinement can weaken it but will not make it disappear.
Partially synchronous networks, dynamic domain topologies, and open systems are untreated. The current model is a closed system.
Mid-lifecycle degree promotion is closed only as far as static reassignment. When a regulatory action raises an asset’s degree while a synchronization cycle is in flight, whose rules that cycle follows is open.
A single-hub topology is assumed. The partiality wall in the naturality square was cleared by fixing the hub at chain 0, so moving to multiple hubs requires reproving naturality.
Refinement between model and implementation is the largest. Our position on it has three layers: model-level verification has independent value on its own (the Heard-Of model tradition being the case in point), the repository publishes the model-to-Rust correspondence in FORMAL_MODEL_MAPPING.md, and subsequent properties release the assumptions incrementally.
Conclusion
In the first article of the series we wrote down two jobs. Lifting conditional safety to unconditional convergence, and drawing an externally posited honest-progress assumption inside as a system-internal property. Both closed. Functor completion and degree stratification landed on top, and an out-of-domain instance and a Canton bridge arrived unplanned.
Yet looking back, the most valuable moments in this work were not the moments theorems closed. They were the moments we noticed a sentence was stronger than its theorem. Where the functor was trivial, where deadlock freedom was withdrawn, where a name was matched to its content, where the strength of monotonicity actually sat, where a witness was bound inside the roster. Each time our claim got a little smaller and each time what remained got a little firmer.
Those places have one thing in common. The prover raised no complaint. A trivial functor is true, a bypassed threshold is true, an obligation that never fires is true. When we started formal verification we expected the machine to catch what was wrong, and it did. The belief that the glue predicate gives validity was broken by the prover. But what this round taught runs the other way. The machine checks only whether a proposition is true, never whether it says anything. A red build gives information. A build green for no reason gives nothing. So a share remains in this field that no prover can take over: asking whether the proposition I stated is vacuous. Better tools will not make that go away.
Doing formal verification means, in the end, volunteering to have my intuition questioned without pause. It is uncomfortable. But better that the build stops and says “that step does not hold” than that we publish carrying a false belief. And that the same question has to be asked of ourselves when the build does not stop is what this round added. What we are proudest of in this entry may not be the number of theorems closed but the number of claims withdrawn.
The cross-domain state preservation proofs are all public. Install Isabelle/HOL 2025-2, build it, and check for yourself whether what we wrote here is so. This is one of the values of formal verification: you do not have to trust the author. The entry currently stands at proofs complete, published on GitHub, awaiting AFP registration.
One question is left. Every place we stepped back, the code told us. So how do we find the places the code does not tell us about? When a model abstracts reality wrongly, the prover says nothing, because inside the model everything is true. We do not have an answer to that yet, and it is probably the question anyone doing formal verification carries for a lifetime.
The broader system context lives in the Oraclizer documentation.
References
- Lochbihler, A., & Marić, O. (2020). Authenticated Data Structures as Functors in Isabelle/HOL. FMBC 2020, OASIcs vol. 84, pp. 6:1-6:16. Archive of Formal Proofs entry: ADS_Functor. doi:10.4230/OASIcs.FMBC.2020.6
- Kim, J. (2026). The Cross-Domain State Preservation Functor: A Mechanized Theory of Regulatory State Synchronization in Isabelle/HOL. arXiv:2604.03844.
- Charron-Bost, B., & Schiper, A. (2009). The Heard-Of model: computing in distributed systems with benign faults. Distributed Computing, 22(1), 49-71.
- Mac Lane, S. (1998). Categories for the Working Mathematician (2nd ed.). Graduate Texts in Mathematics, vol. 5. Springer.
- Nipkow, T., Paulson, L. C., & Wenzel, M. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer.
- Lamport, L. (1978). Time, Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM, 21(7), 558-565.
