When Regulatory Actions Do Not Commute: Order, Outcome, and Sixty Normal Forms

TL;DR

• Several standards already define enforcement commands. What none of them define is what happens when those commands overlap. This article pins that down. Regulatory action composition was mechanized before the normative design of our security-token enforcement standard (ERC-TRUST) was frozen, so the Isabelle/HOL theory assumes no particular implementation language and no downstream program verifier.
• Send a freeze and a seizure at a restricted asset and the freeze-first order applies the seizure, while the seizure-first order leaves it rejected on the record. The final state differs, and so does the modelled outcome of the seizure command itself.
• All twenty-one distinct pairs of the seven transition labels are classified. Twelve commute on final state, nine do not, and every non-commuting pair carries a witness start state where the two orders come apart.
• Rejection and operational failure are kept apart, and so are state idempotence and trace idempotence. Send the same command twice and the state holds still while the log carries two events.
• Action words are unbounded, yet the state transformations number exactly sixty. They give a finite specification-side regression basis, while the refinement obligations that carry this into the standard are registered with zero discharged.
• Five places pushed back, and all five made our claim smaller. Theorems that passed a green build were leaning on computation outside the kernel, and we nearly wrote “classified all of them” with no theorem that the list was complete.
• Everything sits in the public repository. Not a request to be trusted, but a result anyone can build and check.

---

Plenty of standards already attach enforcement commands to tokenized assets: freeze, seize, confiscate, restrict. What each command does on chain is mostly settled. So what is left?

Two things. First, what those commands mean legally goes undefined at the standard layer. An irreversible confiscation and a reversible custodial transfer surface as the same call. Second, what happens when the commands overlap is something no standard addresses. Each command has a validity rule; the space between commands is empty.

We are building a security-token enforcement standard on top of that layer (ERC-TRUST). The first gap is filled by that standard together with the regulatory vocabulary standard it references. The second gap had to close before the standard’s normative design was frozen. Once an interface hardens and a proof follows it, the proof becomes a device for justifying decisions already made.

Earlier work built a reference machine of five regulatory states and seven transition labels, and proved that a regulatory transition raised in one domain is faithfully reflected in another (Cross-Domain State Preservation Proofs). That result covered a single transition.

Real systems do not receive regulatory commands one at a time. Authorities in different jurisdictions issue orders against the same asset days apart, sometimes inside the same block. At that point the question a system has to answer shifts: from whether each command is valid, to what semantics this sequence of commands carries.

That question is now pinned to a finite executable algebra. Where order changes meaning and how many such places exist are classified exhaustively, and each place comes with a witness that reproduces it and a finite reference basis that implementation verification can consume.

Two Valid Commands, One Order-Dependent Result

The case comes before the explanation.

An asset sits in the restricted state (RESTRICTED). Two enforcement commands arrive. One is a freeze (FREEZE), the other a seizure (SEIZE).

Both are transition labels the reference machine knows, and both are commands this model accepts as input. Only the arrival order differs.

Order	First command	Second command	Final regulatory state	What became of the seizure
Freeze first	Applied, RESTRICTED to FROZEN	Applied, FROZEN to SEIZED	SEIZED	It took effect
Seizure first	Rejected, state stays RESTRICTED	Applied, RESTRICTED to FROZEN	FROZEN	It never took effect

The difference between the two runs does not stop at the final state. The same seizure command takes effect under one order and is rejected under the other. The reference machine defines no transition from RESTRICTED on SEIZE; seizure only becomes defined once the freeze has moved the asset to FROZEN. The command that executed first changed whether the next command was defined at all.

This pair is one of the nine non-commuting pairs we proved, and RESTRICTED is the machine-checked witness attached to it. From the point of view of the authority that issued the seizure, the command was accepted and logged, yet the asset was never seized. A system that swallows that outcome quietly leaves two authorities holding different pictures of the world.

So the question changes. Instead of checking whether each action is valid, we have to ask what semantics the sequence carries.

Why We Proved This Now

Start with what was already in hand. The transition table over five states and seven labels had been mechanized long before. That confiscation is terminal and that confiscation is reachable from every non-terminal state were closed as theorems, and determinism follows the moment the transition is defined as a function. On top of that sits the homomorphism result carrying a regulatory transition from one domain into another. What was settled was the rule for a single command.

What was missing lived between commands. The reference machine answered “is this action defined in this state?” and said nothing about “what happens when that action follows this one?” Order, the meaning of a rejection, the execution record, and the transfer-permission decision had no place in the model.

Approving a drug one at a time and testing what two drugs do together are separate procedures. However careful the individual approvals, they do not stand in for the interaction study. Regulatory actions sat in the same position. What a freeze does and what a seizure does were already defined, and the empty spot was what happens when you use both. That spot is now filled by a finite list, and no human hand checked the list; the machine did.

The immediate reason for filling it now came from the standard side. At a deeper level, inverting the order only works if this work stays independent of the standard. Bend the model for the standard’s convenience and the proof turns back into a justification device.

So the theory imports neither Solidity nor any particular implementation verification framework, and assumes nothing about storage layout or function signatures. Change the implementation plan or swap the downstream verifier and these theorems survive. Rather than leaving behind residue shaped to fit the standard, we put down the stronger canonical result the standard will have to follow.

Scope was fixed by a single test: “if we do not verify it here, is there anywhere else it gets verified?” Sweeping the product cycle end to end against that test turned up an item we did not expect. The transfer-permission decision qualifies. How a frozen asset should treat an ordinary transfer differently from an authority’s enforcement transfer had no home in the regulatory state algebra, in locking, or in cross-chain propagation. Having nowhere else to live is the entire reason it became one of the results below.

The result attaches in three directions. Downward it lands on the existing reference machine. The transition table is reused rather than redefined, and the cross-chain theorem calls the synchronization-validity preservation already proved by the state-preservation work directly inside its own proof body. Beyond citing the literature, this is code calling code.

Sideways it attaches to the regulatory vocabulary. The names and meanings of the six legal effects belong to a separate standards proposal, and the theorems show that the vocabulary does not drift from the state machine. Vocabulary written first and a machine built later can come apart; that they do not is now fixed mechanically.

Upward it crosses into the enforcement standard. Crossing and arriving are separate matters, though. Supplying a formal result as reference semantics and discharging an actual implementation refinement are two different states of affairs.

The Reference Machine We Actually Checked

The size of the object under test comes first. The machine here ends at five regulatory states and seven transition labels.

The states are ACTIVE, FROZEN, SEIZED, CONFISCATED, and RESTRICTED. The labels are four escalations (FREEZE, SEIZE, CONFISCATE, RESTRICT) and their three de-escalations (UNFREEZE, UNRESTRICT, RELEASE). Of the 5 x 7 = 35 cells, twelve carry a defined transition and the remaining twenty-three are empty. The table itself was published in earlier work and is unchanged here.

This work is an independent session that takes that verified transition table as it stands. In the public repository it is a separate Isabelle session, its only direct import is the existing regulatory instance, and not one line of the existing theories was touched. The sessions were split so the two results can be reviewed separately. If regulatory action composition turns out wrong, the state-preservation theorems still stand, and the same holds in reverse.

One boundary goes down early. These five states are not an ontology of actual law, and the seven labels are not the full inventory of actions a product will support. The reference machine is deliberately small so that it can carry the effects regulatory enforcement leaves on asset state, while jurisdictional doctrine, authority hierarchy, and evidentiary requirements stay outside it. Small is not a loss here. The object has to be finite and small for exhaustive classification to be possible, and exhaustive classification is what lets “which pairs are dangerous?” be answered with a list.

Rejected Is Not Operationally Failed

The outcome type of a single command comes first. Group the branches wrong here and every result downstream is contaminated.

datatype command_outcome =
    Applied reg_state
  | Rejected legal_rejection_reason
  | Operational_Failure operational_failure_reason

Three branches. Applied covers a defined transition where the state actually moved. Rejected covers the case where the transition from this state on that action is undefined in the reference machine, so the model rejects it normatively. Operational_Failure covers a missing asset, an unavailable lock, or an external system error, where execution ran aground before the transition was ever judged.

definition legal_outcome :: "reg_state ⇒ reg_action ⇒ command_outcome" where
  "legal_outcome s a =
    (case reg_transition s a of
       Some s' ⇒ Applied s'
     | None ⇒ Rejected Undefined_Transition)"

The function layers need separating here. legal_outcome itself produces only two branches, Applied and Rejected. Operational_Failure is introduced one layer up, by the command executor execute_command, when it checks command status and execution preconditions. The three branches are the observation boundary of command processing as a whole, not the actual output range of legal_outcome alone.

Rejection and operational failure do exactly nothing to the state, in the same way. Both leave the asset’s regulatory state untouched. So why keep them apart?

Because they mean different things at three layers. For retry, an operational failure leaves room for the same command to succeed once its cause is removed, while a rejection in the model gives the same answer for the same state and the same action. For audit, a rejection is the model fact “that transition is not defined at this reference state,” and an operational failure is the operational fact “the execution precondition was not met.” For recovery, an operational failure can feed a recovery procedure, while a rejection in the model does not clear on re-execution unless the transition table or the current state changes. Collapse the three into one failure and the records you can report to a regulator become indistinguishable from the records your operations team has to act on.

We treated these three as the observation boundary an implementation must expose rather than as internal convenience. That is also why the enforcement standard we are building declares the result of a regulatory command as a typed value instead of a boolean. This model fixes only what the type has to distinguish. How to shape the concrete error ABI, the storage effect, and the revert behaviour is left open, with one requirement: the implementation must not blur the three together.

Figure 1: One command, three outcome classes, and why the same state effect carries different meaning

The same distinction splits once more under repeated commands. The state effect of an action is idempotent.

theorem action_state_idempotent:
  "state_effect (state_effect s a) a = state_effect s a"

Send a freeze at an already frozen asset and the state does not move. Duplicate delivery and re-sending cannot corrupt asset state. The record, however, is not idempotent.

theorem repeated_message_has_idempotent_state_and_distinct_trace:
  "fst (execute_command FROZEN repeated_message) = FROZEN ∧
   event_outcome (snd (execute_command FROZEN repeated_message)) =
     Rejected Undefined_Transition ∧
   snd (execute_command ACTIVE concrete_message) ≠
     snd (execute_command FROZEN repeated_message)"

The first command is logged as Applied and the second as Rejected. Same state, different record. That distinction is what lets a system answer “why did two freeze commands arrive for this asset?” In a system that only looks at state, the question cannot even be posed.

Classifying Every Pair in Regulatory Action Composition

Order sensitivity now becomes a list. There are twenty-one ways to choose two distinct labels from seven. We split all twenty-one into commuting and non-commuting with nothing left over, and proved the classification complete.

Commutativity is defined on final state.

definition commutes :: "reg_action ⇒ reg_action ⇒ bool" where
  "commutes a b ⟷
    (∀s. state_effect (state_effect s a) b =
         state_effect (state_effect s b) a)"

A universal statement over every state s. Since there are only five states, that universal statement is equivalent to an executable predicate that actually walks the five, and the equivalence is itself proved (pair_commutes_iff). The classification can therefore be computed as a filter while the computation is guaranteed not to drift from the universal statement.

theorem commuting_pairs_complete:
  "filter pair_commutes all_unordered_pairs = commuting_pairs"

theorem noncommuting_pairs_complete:
  "filter (Not ∘ pair_commutes) all_unordered_pairs = noncommuting_pairs"

theorem pair_classification_cardinality:
  "length commuting_pairs = 12 ∧
   length noncommuting_pairs = 9 ∧
   length all_unordered_pairs = 21"

What “complete” covers deserves spelling out. The list holds no duplicates (all_unordered_pairs_distinct), contains no pair of a label with itself (all_unordered_pairs_irreflexive), and holds any two distinct labels in one direction or the other (all_unordered_pairs_complete). With those three attached, twenty-one shifts in meaning from “we picked twenty-one” to “there are twenty-one possible pairs.”

The nine non-commuting pairs come with witnesses.

theorem noncommuting_witnesses_sound:
  "list_all witness_valid noncommuting_witnesses"

theorem noncommuting_witnesses_complete:
  "map fst noncommuting_witnesses = noncommuting_pairs"

Soundness says the nine witnesses offered are start states that genuinely pull the two orders apart. Completeness says every one of the nine non-commuting pairs has a witness and that the two lists match exactly. Say only “this pair does not commute” and a reviewer has to hunt for the state where it breaks. With the witness attached, one state reproduces it.

Figure 2: The complete twenty-one pair classification with the witness state for each non-commuting pair

A caveat has to travel with this. Commutativity for the twelve is about final state, not about the record. Freeze paired with restrict is the example. Put the freeze first on an ACTIVE asset and the restrict command is logged as Rejected; put the restrict first and both commands are logged as Applied. The final state is FROZEN either way, while the per-command outcome distribution differs.

So there are two ways to read the classification. Asked whether reordering leaves the asset in the same state, the twelve answer yes. This list on its own cannot decide trace reordering safety, though. Some pairs differ even in the per-command split between Applied and Rejected, and where that split matches, the identity of an ordered trace can still differ. The theory does not close a complete classification of the latter as a separate theorem.

In practice the list works as a sequence review checklist. When a design point admits two or more enforcement commands landing on the same asset, and the combination sits among the nine, an explicit ordering rule has to exist. Missing rule, defect. When the combination sits among the twelve, the final state is settled and what remains is deciding how the record order is kept.

On the implementation side the list becomes two things: the nine pairs become an order-sensitivity registry, and the nine witnesses become pairwise regression vectors. One condition rides along. A deployment has to declare which of the seven labels each of its public commands binds to before the witness vectors mean anything. Without that mapping between command names and transition labels, the classification says nothing about that deployment.

Terminality and Provenance

After order sensitivity come two strong invariants. Both say something stronger than “what state is it in now?”

First, the terminality of confiscation.

theorem confiscated_word_absorbing:
  "run_word as CONFISCATED = CONFISCATED"

theorem confiscated_word_rejections:
  "snd (action_outcome_queue as CONFISCATED) =
   map (λ_. Rejected Undefined_Transition) as"

Here as is an arbitrary action word. The first theorem says a confiscated asset stays at CONFISCATED no matter how many commands arrive. The second says every one of those commands is logged as a rejection, without exception. Without the second, terminality is half a result. Knowing the state did not move tells you nothing about whether those commands vanished quietly or landed in the record, and a vanished command is an incident on its own in regulatory enforcement.

Second, the provenance of restrictive states.

theorem frozen_word_provenance:
  assumes "run_word as s = FROZEN" and "s ≠ FROZEN"
  shows "FREEZE ∈ set as"

Theorems of the same shape cover seizure and confiscation (seized_word_provenance, confiscated_word_provenance). The reading runs like this: if an unfrozen asset arrives at the frozen state through some sequence of commands, a freeze command has to appear in that sequence. No clever composition of the other actions manufactures the frozen state.

This is a stronger audit invariant than plain reachability because of its time direction. Reachability says “can this state be reached?” A provenance theorem says “if it is in this state, what must have happened before?” Auditors mostly ask the second. If an asset sits in the confiscated state with no confiscation command on record, inside this model the record is what is wrong.

One boundary rides along. A provenance theorem speaks about where a state effect came from, never about the authorization of whoever issued the command. Who had standing to send that freeze belongs to the authority model and sits outside this one.

How far the enforcement standard can lean on this theorem stops at exactly that line. The check “if this asset is confiscated, a confiscation command must be on record” is supported by the result. The check “whoever sent that confiscation had standing to do so” depends on caller identity, signature, and jurisdictional judgment, all outside the model. Write the two checks as one sentence and the standard ends up claiming more than the proof does.

Legal Effects Are Typed, Transfers Are Gated

Two lists diverge here. The legal-effect vocabulary of regulatory actions has six entries, and the state transition labels number seven. Neither list is a subset of the other.

The six legal effects are freeze, seize, confiscate, restrict, recover, and liquidate, each carrying three coordinates: reversibility, ownership effect, and finality.

Legal effect	Reversibility	Ownership effect	Finality
Freeze	Reversible	Retained	Provisional
Seize	Conditional	Retained	Interim_Custodial
Confiscate	Irreversible	Transferred	Final
Restrict	Configurable	Retained	Conditional_Finality
Recover	One_Time	Restored	Restorative
Liquidate	Irreversible	Terminated	Final

theorem legal_action_descriptor_inventory:
  "set all_legal_actions = UNIV ∧
   length all_legal_actions = 6 ∧
   inj legal_descriptor"

The part of this theorem doing real work is the injectivity at the end (inj). The three-coordinate combinations of the six legal effects do not overlap. The closest pair is confiscation and liquidation: both irreversible, both final, split only by ownership effect, transferred against terminated. A single coordinate separates the two.

This is exactly the spot today’s standards leave empty. ERC-7943 states why it chose a neutral name for its forced transfer. Names like confiscation or recovery describe a particular motivation, whereas forcedTransfer denotes the act of transferring alone, independent of the reason. That is a deliberate choice by the standard’s authors and sound at the standard layer. The cost is that an irreversible confiscation and a reversible custodial transfer look like the same call on chain.

ERC-3643 is the case on the other side. It gives freeze, forced transfer, and recovery separate functions, yet those names only carry meaning inside that standard, and the reversibility and ownership effect of each operation go normatively undefined. What we verified is that the distinction can be raised into a type a machine can decide. The normative definition of this vocabulary is handled in a separate standards proposal (ERC-8319), and what happens here is a proof that the vocabulary and the state machine agree.

theorem descriptor_transition_compatibility:
  assumes "transition_label_of k = Some a"
      and "reg_transition s a = Some s'"
  shows "descriptor_target k = Some s'"

When the transition label matching a legal effect actually fires and the state moves, the state it arrives at is the target that legal effect declared. Declaration and behaviour cannot drift apart.

The same theorem exposes why the two lists differ. Recovery and liquidation have no corresponding transition label at all (recover_and_liquidate_are_not_state_transitions). Instead of changing regulatory state, both move or extinguish the asset at a separate layer.

In the other direction, the three de-escalation labels have no matching legal effect, because de-escalation reads less as an independent legal effect than as the counterpart of an escalation. Force the two lists into one and something on one side gets distorted.

Transfer gates split the same way.

theorem restricted_transfer_uses_current_condition:
  "transfer_allowed RESTRICTED
     ⦇transfer_path_value = Ordinary_Transfer,
      baseline_clear = baseline,
      restriction_clear = restriction,
      enforcement_approved = authorization⦈
   ⟷ baseline ∧ restriction"

theorem enforcement_transfer_is_a_separate_path:
  "transfer_allowed s
      ⦇transfer_path_value = Authorized_Enforcement k,
       baseline_clear = baseline,
       restriction_clear = restriction,
       enforcement_approved = authorization⦈
   ⟷ authorization ∧ enforcement_transfer_action k"

An ordinary transfer has to clear both the baseline compliance gate and the regulatory state gate. Unlike a freeze, the restricted state is not a blanket block; it passes once the current restriction condition is met. An enforcement transfer takes a completely different path. It never consults the regulatory state gate and looks only at whether the action is authorized and whether that legal effect is of a kind that moves assets.

One consequence changes a design decision. A frozen asset blocks ordinary transfers while authorized enforcement transfers pass. What a freeze blocks is disposal by the holder, never enforcement by an authority. Implement the two behind one gate and confiscation and recovery become impossible after a freeze, which is not a functioning regulatory enforcement system.

How this gate ended up in this article is worth recording. The transfer-permission decision belongs neither to the regulatory state algebra nor to locking nor to propagation, so it had no home in any verification target. Yet an enforcement standard cannot ship without it. It came in through the “is there anywhere else this gets verified?” test, and on the implementation side it becomes the dispatcher separating the ordinary path from the enforcement path. The boundary is clean: caller identity, signature, jurisdictional judgment, and the correctness of the policy oracle all sit outside this model, and what is proved here is only the structure in which the two paths consult different conditions.

A Command Processor Needs a Trace Contract

So far the semantics of state and outcome. A real command processor also has to promise what it keeps on the record.

theorem command_queue_preserves_order_and_length:
  "map event_identity (snd (run_command_queue cmds s)) =
     map command_identity cmds ∧
   length (snd (run_command_queue cmds s)) = length cmds"

The run_command_queue in this theorem is an abstract queue folding one regulatory state cell in order. It models neither a dispatcher updating a whole per-asset store nor the interleaving of commands across assets. Within that scope, the trace events the queue emits carry the same order and the same count as the input commands. No reordering, no dropping, no arbitrary merging. Alongside sit theorems that each event preserves the original command’s identity, asset, actor, source chain, and action (command_trace_preserves_input), and records which of the three branches the execution ended in (command_trace_records_execution_outcome).

What these three become on the standard side is clear enough. They turn into the conformance conditions an event schema and an audit log have to satisfy, and into the floor under any design that wants to leave a typed receipt for an enforcement outcome. Record integrity itself and signature authenticity stay outside. The proved range reaches the processor does not change order, count, or content when it moves input into the record, and any guarantee that the record is not forged later belongs to another layer.

The per-asset frame condition is closed alongside.

theorem other_asset_unchanged:
  assumes "other ≠ command_asset cmd"
  shows "fst (execute_on_store cmd store) other = store other"

A regulatory command against one asset does not touch the state of another. Obvious looking, and exactly the kind of property that breaks quietly later when the storage layout changes, unless it is proved explicitly.

On the cross-domain side, consistency between completed atomic steps is closed.

theorem completed_prefixes_are_consistent:
  assumes "valid_state gs"
  shows "list_all consistent_state (completed_states cmds gs)"

Run a regulatory command queue from a valid global state and, at every point you cut after a completed step, all chains holding the asset agree on the same regulatory state. Validity itself is preserved across the whole queue as well (sync_queue_preserves_valid_state).

The scope of this result has to be stated precisely. A command here is modelled as an atomic step, and what the theorem guarantees is consistency between those steps. Moments during a step’s execution, intermediate states propagated to only some chains, interleaving across commands, timeouts, and rollback are all untreated. That territory belongs to follow-up work on preemptive locking and propagation.

Unbounded Words, Sixty Normal Forms

The last result concerns the size of this model.

Action words are unbounded. Seven labels give 7ⁿ words of length n, with no ceiling on n. What those unbounded words do to asset state is not unbounded, though. Apply each word to the five start states and read off the resulting five-slot state transformation vector, and exactly sixty distinct vectors occur.

theorem normal_forms_cardinality:
  "length normal_forms = 60"

theorem normal_forms_are_distinct:
  "distinct normal_forms"

theorem normal_forms_closed:
  assumes "v ∈ set normal_forms"
  shows "vector_step v a ∈ set normal_forms"

theorem every_word_has_normal_form:
  "state_vector as ∈ set normal_forms"

Four theorems make one closure story. The sixty are pairwise distinct, appending any of the seven actions keeps you inside the sixty, and an arbitrary action word lands on one of them. A theorem showing each of the sixty is reachable by an actual word (normal_forms_reachable) confirms the list is not vacuous. The longest representative word runs to nine actions.

Figure 3: Unbounded action words, exactly sixty state-transformation normal forms

Algebraically, the transformation monoid generated by the seven actions has order sixty, and the identity (the empty word) sits among them. Finite transformation monoids are an old subject. We did not mechanize that general theory; we computed the monoid of this specific regulatory machine and proved the computation complete.

What this hands to implementation verification is not a theorem that sixty tests fully replace unbounded implementation traces. What is proved is that inside the reference machine, the state effect of every action word equals one of the sixty vectors. The sixty representative words therefore serve as a finite specification-side regression basis and a reference oracle.

Extending that finite basis to full word effects requires more: the implementation must match the reference machine on the one-step effect of each label, plus a refinement or equivalent inductive argument that command composition preserves that step relation. Without the connection, a history-dependent implementation can pass all sixty representative words and still diverge on a longer word belonging to the same reference vector. What crosses to the enforcement standard is a checkable finite basis, never an automatic closure of implementation conformance.

What the basis does not guarantee is equally clear. Agreement on the sixty vectors is a state-transformation-layer classification of the reference model, not agreement on records, events, authorization, or storage layout. Within this model’s scope, discharge against real code stands at zero. Implementation conformance stays work for a separate track once the code is frozen, step relation and composition preservation included.

Where We Got Stuck

Listing results is easy. Before the list existed, the work that ate the most time was not closing theorems. It was checking whether a closed theorem says what we claimed. Five places caught us, and all five made our claim a little smaller.

We Set Out to Prove Authority and Ended Up Proving Provenance

The first design carried an axis that assigned a strength number to each action and built authority levels on top. The plan was to prove that a weak authority cannot produce a strong effect.

The trouble sat in the ground we meant to stand on. The public standard defining the legal-effect vocabulary of regulatory actions deliberately leaves the ranking among authorities undefined. It fixes only the finality ordering of the actions and stays silent on who outranks whom, because that varies by jurisdiction. The silence is not a defect in the standard. It is design.

Which means a theorem we proved over an authority hierarchy of our own construction would be a theorem about a hierarchy we invented, not about the standard. We dropped the axis.

The same worry moved onto a different axis. What we wanted to block was “composing weak actions into a strong effect,” and that proposition is expressible without authority at all. The confiscated state does not come into being without a confiscation command. State provenance theorems took over from the discarded axis, and the result landed closer to the question auditors actually ask. Fill a space the standard left empty and prove something there, and the subject of the theorem changes.

Saying the Final State Matches and Saying the Record Matches

The early design tried to carry “these two actions commute” as a single predicate. An independent audit asked us to separate commutativity of the final state from observational equivalence of the execution record, and we took the point.

Without that separation this article would have carried the sentence “the twelve are safe to reorder,” and that sentence is false. Even with matching final states, which command took effect and which was rejected varies with the order, and in regulatory enforcement that difference is not small.

Two errors of our own surfaced in the same audit. A relation between two states had been written as an equivalence when only one direction holds, and one sentence about atomicity was claiming more than its theorem, so it came down.

The Build Was Green and the Kernel Had Not Checked It

During development some properties of the sixty-transformation list were closed with an evaluator, computing the table and confirming it matched. The build was green.

Inspecting the trust boundary showed those theorems leaning on an oracle outside the kernel. We were trusting a computation in place of a proof. All of it came out, the sixty vectors were listed explicitly, and closure under each of the seven actions was rebuilt as kernel proof. In the final version every named theorem carries zero oracles.

One lesson came out of it. A green build says “this proposition is true” and stops there. It does not say “the kernel checked it.” The gap between those two sentences stays invisible until you actually inspect the trust boundary.

The same theorems a green build had already accepted, queried again for what stood behind them.

“We Picked Twenty-One” Against “There Are Twenty-One”

The twenty-one pair list was written out in the source, and for a while there was no theorem saying the list was complete.

Write “we classified all twenty-one pairs” in that state and the real claim is “we classified the twenty-one we wrote down.” The moment a reviewer doubts the list, the whole classification loses its ground. We filled in the theorem that there are no duplicates, the theorem that no label pairs with itself, and the theorem that any two distinct labels appear in the list.

The same illness was in the sixty-item list. Only the direction saying an arbitrary word lands inside the list was present; the reverse, that each element is reachable by an actual word, was missing. So “exactly sixty” was larger than the theorem. Representative words, their evaluation, and reverse reachability were attached until the phrasing and the theorem matched.

Both times we raised the proof instead of lowering the requirement. Weakening the sentence also makes the problem disappear, and what you are left with is a weaker result.

As a check, we deleted one vector from the sixty-item list and rebuilt. The cardinality theorem and the closure proof collapsed together. Demonstration that the list is load-bearing rather than decorative.

Where the Model Diverged From the Product, the Prover Said Nothing

The last one was the quietest. An independent verification pass caught the transfer gate for the restricted state set to block unconditionally.

In the product documentation and the standard text, restriction means conditional trading permission. Meet the condition and ordinary trading proceeds, and that is the substantive difference between a freeze and a restriction. The model was locking harder than the product, and left that way it would later make the implementation look wrong when the two were compared.

There were two ways out: fit the article’s sentence to the model, or fit the model to the product meaning. We took the second, adding one abstract input for whether the current restriction condition is met, and attaching concrete witnesses on both the allowed and the blocked side. Nothing was lowered.

The path this defect came out on matters. It did not come from reading code; it came from comparing against product meaning. The prover said nothing from start to finish. Where a model abstracts reality incorrectly, the prover stays silent, because inside the model everything is true.

The model’s rule for a restricted transfer set against the product text that defines restriction.

What Changes in Product Engineering

The verification results generate a few candidate design requirements for a regulatory command processor. Candidates that follow from the mathematics, with no claim that our implementation already satisfies them.

Split the command result type three ways. A success-failure dichotomy cannot distinguish retry, audit, and recovery meaning. The result type itself has to separate Applied, Rejected, and Operational_Failure, with a rejection reason on the first and a failure reason on the second.

Make command order deterministic per asset. While nine non-commuting pairs exist, order is not a free variable. Whatever ordering rule is used, it has to exist explicitly, and any place without one is a defect.

Keep the record independent of state. State idempotence and trace idempotence differ, so a design that answers audits by reading the state store alone does not hold up. Rejected commands belong in the record too.

Type the transfer paths. Ordinary transfers and authorized enforcement transfers clear different conditions. Hide that behind unstructured conditionals inside a single transfer function with no path tag, and the difference stops showing up in the types and the interface.

Hold the per-asset frame. A regulatory command on one asset must not reach the state of another, and that belongs in regression testing whenever the storage design changes.

Adopt the sixty transformation vectors as the specification-side regression basis. Closing full implementation conformance takes separate step-level refinement and composition-preservation evidence.

Between this list and a real implementation there is no bridge yet. Between a verified model and a verified product sits a register of refinement obligations, and every entry in that register currently stands registered with no implementation evidence.

What Crossed to the Enforcement Standard and What Did Not

Where regulatory action composition finally has to arrive is the security-token enforcement standard. That standard unifies the meaning, authority, state transitions, outcomes, and receipts of regulatory actions as a common norm while leaving policy, identity, and deployment structure to fit the environment, and its normative design is already frozen.

The relationship deserves precision. The proof in this article is not the formal verification of that standard. It is an independent result that presupposes no standard, and it is the reference semantics the standard has to follow. Change the tooling or the deployment structure of the standard’s implementation and these theorems do not move.

Start with what crossed.

What the formal result fixes	What it becomes on the standard and implementation side
Three-branch outcome type	Typed result of the regulatory command evaluator
Transition evaluation function	Pure reference evaluator shared by contract and service tests
21-pair classification and nine witnesses	Order-sensitivity registry and pairwise regression vectors
Dual transfer gate	Dispatcher separating ordinary from enforcement transfers
Trace contract	Event-schema and audit-log conformance tests
Sixty transformation vectors	Finite reference oracle and specification-side regression basis

This correspondence is written row by row in the public model mapping, each row carrying its open boundary alongside. The outcome type corresponds, while the concrete error ABI, storage effect, and revert behaviour remain unpinned. The 21-pair classification is confined to this five-state, seven-label machine. Using the witness vectors requires a deployment to bind each of its public commands to the matching label first.

What did not cross matters more. The mapping describes itself as a planned correspondence. No concrete source revision is designated, and not one model-to-code refinement has been discharged. Completing the correspondence requires immutable implementation targets for the command result type, the transition evaluator, the transfer dispatcher, the event schema, the asset storage update, and the queue boundary, plus bidirectional coverage of every modelled label and outcome, plus an explicit disposition for each open boundary. Neither a green build nor a machine-generated specification-side corpus discharges that refinement.

So what can and cannot be said divides cleanly. On the sayable side: the abstract regulatory action algebra and the trace properties are proved within their declared scope, and the obligations running toward implementation are registered as a list. On the unsayable side: the correctness of Solidity functions, the safety of bytecode and deployment configuration, and the existence of actual legal authority.

One point is worth marking. The decision to split the outcome of a regulatory command into applied, rejected, and operationally failed also lives in the normative design of the enforcement standard. The standard declares the type, and the formal model shows that the state effects and records of command ordering can be analysed while that outcome distinction is preserved. A type declaration in a standards document does not by itself deliver the properties of command composition.

What Remains

Writing down what did not close.

Authority and identity. Who has standing to issue which command, and how authority ranks across jurisdictions, sit outside this model. Provenance theorems say where a state effect came from, never whether its issuance was authorized.

Replay protection. State idempotence guarantees that duplicate commands do not corrupt state, while blocking the resubmission of a stale command belongs to a separate layer handling command identifiers and validity windows.

Concrete policy decisions. The condition deciding whether a restricted state lets a transfer through is left as an abstract boolean. Connecting actual jurisdictional rules to that boolean is a policy-oracle problem, and what is proved here stops at how the condition enters the gate.

Concurrency and partial propagation. Only the space between completed steps is treated, on the premise that a command is atomic. Interleaving, intermediate states that reached only some chains, timeouts, and rollback belong to subsequent properties.

Refinement between model and code. The largest item, written out entry by entry in the previous section. In one line: saying the sixty transformation vectors sit in a good place to build a bridge is different from saying the bridge is built.

Restriction history. In the published reference machine, restricting then freezing then unfreezing returns the asset to ACTIVE without restoring the prior restriction (restricted_freeze_unfreeze_loses_history). This information loss is not a defect in the model. It is a fact about how the model is defined, and the reference machine says honestly that it holds no history at this point.

An obligation for the enforcement standard follows. An implementation unfreezing an asset has to re-evaluate the current compliance policy and any live restrictions, and has to forbid both the silent erasure of a valid restriction and the blind revival of an expired one. That the reference machine does not restore history says nothing about an implementation being free to skip the re-evaluation. The obligation is registered and undischarged.

---

Conclusion

The question we started with was simple. When regulatory commands land on top of each other, where do the accidents happen?

The answer is now a list. Of the twenty-one pairs, nine let order change the result, and each of those nine carries a start state where the two orders come apart. The twelve reach the same final state, though that fact alone does not deliver trace reordering safety. Confiscation absorbs every subsequent command while leaving all of them on the record as rejections, and a restrictive state never comes into being without its own command. What unbounded command sequences do to asset state amounts to sixty possibilities.

That list is now the reference the enforcement standard can point to when it asks about conformance. Part of what the standard used to demand in prose crossed over in a finite, machine-checkable form, and the rest, the part joining an implementation to that basis, stays as undischarged refinement obligations.

Four tensions showed up in the modelling. Split rejection from operational failure or not. Merge the seven transition labels and the six legal effects into one list or not. Handle state idempotence and record distinction at which layer. Turn unbounded words into a finite basis how. All four times, merging made the code shorter and the model dishonest. We split, and every split cost one more theorem.

Looking back, those choices were not where the time went. Checking whether a closed theorem is as large as our sentence took far longer. The five places above share one thing: at none of them did the prover complain.

A theorem over an invented authority hierarchy is true. A proposition closed by an evaluator is true. A classification over the twenty-one we wrote down is true. True, only not as large as what we said.

Closing the earlier work, we left one question open. How do you find the places the code does not tell you about?

This round showed half an answer. That the transfer gate for the restricted state was locking harder than the product meaning came neither from the code nor from the prover; it came from reading the model against the product text line by line. Where a model abstracts reality incorrectly the machine stays silent, so finding those places is left to comparison outside the machine. Not a complete answer, and the only method we currently know.

One thing gets stated plainly. The conclusion of this article is not that regulatory command processing became safe. We now know precisely where order changes meaning, and the finite basis for those places. The distance from here to a real product is the refinement obligation, and we chose to measure that distance accurately before closing it. The most dangerous sentence in formal verification is not a false one; it is one larger than its own theorem.

The theory source, the session PDF, and the build instructions all sit in the public repository. Install per the official Isabelle2025-2 documentation, build both sessions, and check for yourself whether the numbers in this article hold. Twenty-one, twelve, nine, and sixty are not numbers we counted; they are numbers the machine confirmed.

---

References

1. Oraclizer. (2026). Regulatory_Action_Composition.thy. Oraclizer formal-verification repository.
2. Oraclizer. (2026). Regulatory Action Composition session document. Oraclizer formal-verification repository, 27 pp.
3. Kim, J. (2026). The Cross-Domain State Preservation Functor: A Mechanized Theory of Regulatory State Synchronization in Isabelle/HOL. arXiv:2604.03844.
4. Kim, J., & Hong, J. (2026). A Regulatory Compliance Protocol for Asset Interoperability Between Traditional and Decentralized Finance in Tokenized Capital Markets. arXiv:2603.29278.
5. Lo Buglio, D., Martinez Molina, T., & Colceriu, M. (2025). ERC-7943: uRWA – Universal Real World Asset Interface. Ethereum Improvement Proposals.
6. Lebrun, J., Malghem, T., Thizy, K., Falempin, L., & Boudjemaa, A. (2021). ERC-3643: T-REX – Token for Regulated EXchanges. Ethereum Improvement Proposals.
7. 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.