TL;DR
The first substantive decision in formal verification is not tool selection but the choice of expression language. The property we aim to prove (cross-chain regulatory homomorphism) requires the proposition that “every chain’s state transition function preserves regulatory structure.” The moment the function itself becomes the subject of quantification, we enter a domain structurally beyond the expressiveness of First-Order Logic (FOL). Higher-Order Logic (HOL) is the logical system that crosses this boundary, and Isabelle/HOL is the tool that mechanically verifies proofs within it. This article derives why HOL is an essential expression language for our problem directly from Oraclizer’s regulatory state synchronization challenge, introduces the core constructs of Isabelle/HOL in the context of regulatory state modeling, and illuminates the functor concept that forms the theoretical foundation of the Regulatory State Functor.
Learning a Tool vs. Seeing Through a Tool
In the previous article, we presented the rationale for starting formal verification, the grounds for choosing Isabelle/HOL, three target verification properties, and a core design idea we called the Regulatory State Functor. This article follows naturally from the next question: what exactly does Isabelle/HOL enable us to express?
There are two ways to answer this. One is to systematically enumerate the tool’s syntax and features. The other is to look at the problem we need to solve through the lens of the tool, understanding the tool in the process. We choose the latter.
The reason is straightforward. Isabelle/HOL is new to our team. At the time of writing, we are learning HOL’s syntax for the first time and have not yet completed a single proof. But we already possess something: cross-chain regulatory homomorphism as a proof target, OSS’s state transition rules as a formalization subject, and the Regulatory State Functor as a design hypothesis. At every stage of tool learning, these serve as our compass.
We believe this is more than a matter of learning methodology. The boundaries of expressiveness that a tool provides directly determine the boundaries of verifiable properties. The fact that the point where HOL exceeds first-order logic coincides precisely with the point where our problem becomes inexpressible in first-order logic suggests that this tool selection is not mere preference but a necessary choice arising from the structure of the problem itself.
The Wall of First-Order Logic: The Expressiveness Our Problem Demands
The starting point of formal verification is stating the property to be proved precisely. Let us revisit the first property we aim to prove: cross-chain regulatory homomorphism.
Natural-language specification: “When OSS receives a FREEZE message, the state of all chains linked to the target asset ID transitions to FROZEN within bounded time.”
To formalize this statement, we must first define each chain’s state transition function. Let \(\delta_A\) be the state transition function of Chain A, and \(\delta_B\) that of Chain B. Cross-chain regulatory homomorphism means there exists a map \(\varphi\) satisfying:
$$\varphi(\delta_A(s, a)) = \delta_B(\varphi(s), a) \tag{1}$$
Condition (1) is the core of “structure preservation.” Transforming the result of applying regulatory action \(a\) to state \(s\) on Chain A via \(\varphi\) must equal applying the same action on Chain B after first transforming via \(\varphi\). This is the homomorphism condition introduced in our previous article.
A critical question emerges here. Can this condition be expressed in first-order logic (FOL)?
In First-Order Logic (FOL), quantification is possible only over individuals. We can say “for all states \(s\)…” or “there exists an action \(a\) such that…” But to generalize condition (1) to hold for all chains, we must write:
$$\forall \delta. \; (\delta \text{ is a valid state transition function}) \Rightarrow \exists \varphi. \; \forall s, a. \; \varphi(\delta(s, a)) = \ldots$$
Here, \(\forall \delta\) is quantification over the function itself. \(\delta\) is not an individual but a function of type \(S \times A \to S\). Quantification over functions is not permitted in first-order logic [1].
This is not a problem that can be circumvented. We could treat each chain’s state transition function as a fixed constant and prove the property individually: once for Chain A, once for Chain B, once for Chain C. But this provides individual guarantees for enumerated chains, not a universal guarantee that it holds “for all chains.” Every time a new chain is added, a new proof would be required.
The core idea of the Regulatory State Functor (defining a chain-independent abstract functor, treating each chain as an instance, so that existing proofs automatically extend) requires quantifying over relationships between functions (natural transformations), which is impossible in principle within the expressiveness of first-order logic.
This is exactly why Higher-Order Logic is necessary.
Higher-Order Logic: A Logic That Treats Functions as Citizens
Higher-Order Logic (HOL) is rooted in the simple theory of types proposed by Alonzo Church in 1940 [1]. The core extension is concise: allowing functions and predicates themselves to be subjects of quantification.
In first-order logic, writing \(\forall x. \; P(x)\) means \(x\) ranges over individuals. In HOL, we can write \(\forall P. \; P(x)\), where \(P\) ranges over predicates. Going further, \(\forall f. \; (\text{if } f \text{ satisfies some property…})\) enables universal quantification over functions themselves.
Why is this extension decisive? Let us return to our problem.
The universal statement of cross-chain regulatory homomorphism is: “for any state transition function \(\delta\), as long as it satisfies the regulatory state transition rules, the homomorphism condition is preserved.” This is not a statement about a specific chain but a statement about the structure of state transition functions as such. In HOL, this can be expressed directly:
$$\forall \delta : S \times A \to S. \; \text{valid\_transition}(\delta) \Rightarrow \exists \varphi. \; \text{homomorphism}(\delta, \varphi)$$
Furthermore, the natural transformation required by the Regulatory State Functor (a structure-preserving map from functor \(F_A\) to functor \(F_B\)) is a statement about “maps between functors,” which means statements about functions of functions. This is naturally expressible only in higher-order logic.
An important point is that HOL’s expressiveness expansion is not free. By a result of Kurt Gödel, HOL with standard semantics cannot simultaneously possess a complete, sound, and effective proof calculus [1]. This contrasts with first-order logic, which has a complete proof system by Gödel’s completeness theorem. Isabelle/HOL resolves this by adopting Henkin semantics, an approach proposed by Leon Henkin that restricts the range of higher-order types to appropriate subsets rather than full powersets. Under Henkin semantics, HOL admits a sound and complete proof system while retaining expressiveness essentially richer than first-order logic [2].
Isabelle/HOL’s Building Blocks: Through the Lens of Regulatory State Modeling
We now examine the core constructs of Isabelle/HOL. Each is introduced not through generic examples but in the context of the regulatory state model we will actually formalize. The code fragments in this section are not finished models but directional sketches. The actual model may differ substantially during the modeling process.
datatype: Defining a Finite State Space
In Isabelle/HOL, algebraic data types are defined with the datatype keyword. A first approximation of the regulatory state space can be expressed as:
datatype reg_state = ACTIVE | FROZEN | SEIZED | CONFISCATED | RESTRICTED
The implications of this single-line declaration are substantial. Isabelle automatically generates the following from this definition:
Distinctness: ACTIVE ≠ FROZEN, FROZEN ≠ SEIZED, …; all constructor pairs are distinct. Exhaustiveness: every reg_state value is one of these five. Structural induction: to prove a property over reg_state, examining five cases suffices.
In the regulatory domain, this finiteness is a crucial advantage. As mentioned in our previous article, this is precisely why we scoped verification to “regulatory states” rather than “general states”: regulatory states can be finitely enumerated, their transition rules are legally well-defined, and these automatically generated properties directly serve as proof building blocks.
To represent a cross-chain environment, we need the concept of chains:
datatype chain_id = ChainA | ChainB | ChainC
And the global system state becomes a function mapping each chain and asset to a regulatory state:
type_synonym global_state = "chain_id ⇒ asset_id ⇒ reg_state"
Here ⇒ is the function type. global_state is a type that takes a chain ID, then an asset ID, and returns a regulatory state. This is the first point where HOL’s essential advantage (the ability to treat functions as first-class objects) becomes practically visible.
fun and inductive: Two Ways to Define State Transitions
State transition rules can be formalized in two ways: as a total function, or as an inductive relation.
The total function approach:
fun apply_action :: "reg_state ⇒ reg_action ⇒ reg_state" where "apply_action ACTIVE FREEZE = FROZEN" | "apply_action ACTIVE SEIZE = SEIZED" | "apply_action FROZEN SEIZE = SEIZED" | "apply_action _ CONFISCATE = CONFISCATED" | "apply_action s _ = s" (* undefined transitions: state unchanged *)
The fun keyword defines functions via pattern matching, and Isabelle automatically verifies termination. Since results must be defined for all inputs, a “default” like the last line is necessary.
The inductive relation approach:
inductive can_transition :: "reg_state ⇒ reg_action ⇒ reg_state ⇒ bool" where freeze_active: "can_transition ACTIVE FREEZE FROZEN" | seize_active: "can_transition ACTIVE SEIZE SEIZED" | seize_frozen: "can_transition FROZEN SEIZE SEIZED" | confiscate: "can_transition s CONFISCATE CONFISCATED"
inductive enumerates only the permitted transitions. Unlisted transitions are impossible. This approach naturally captures negative properties like “no transition is possible from this state under this action.”
The choice between these approaches is a modeling decision. Total functions suit deterministic systems, while inductive relations are advantageous for nondeterministic systems or those with complex preconditions. Regulatory state transitions are deterministic in the legal sense, making total functions a natural fit, but asynchronous cross-chain message propagation may introduce nondeterministic elements. This tension is a design decision to be resolved during actual modeling.
theorem and proof: Stating and Proving Properties
Once definitions are complete, we state and prove properties. One of the most basic properties in the regulatory state model is irreversibility (that once a certain state is reached, there is no return to a previous state):
theorem confiscation_irreversible: "apply_action CONFISCATED a = CONFISCATED" by (cases a) auto
by (cases a) auto is a proof strategy: split on all possible cases of regulatory action \(a\) (cases), then prove each case automatically (auto). Isabelle’s auto is an automated proof tool combining simplification rules with basic logical rules.
A more interesting property involves reachability:
theorem no_return_from_confiscated: assumes "can_transition* s₀ CONFISCATED" shows "¬ (can_transition* CONFISCATED ACTIVE)"
Here can_transition* is the reflexive transitive closure of the transition relation. This theorem states: “regardless of the starting state, once CONFISCATED is reached, no path back to ACTIVE exists.”
This property matters because of its legal meaning. CONFISCATE represents permanent forfeiture of ownership, so confiscated assets must not have any system path back to active status. If this theorem’s proof fails during modeling, that is a signal of a design flaw in our state transition rules; this is the core value of performing formal verification before writing code.
Sledgehammer: Borrowing the Machine’s Power for Proofs
One of Isabelle/HOL’s practical strengths is an automated proof tool called Sledgehammer [3]. Sledgehammer translates proof goals into first-order logic and simultaneously dispatches them to multiple external ATPs (Automated Theorem Provers: E, Vampire, Z3, CVC4, and others) to search for proofs.
Usage is remarkably simple:
theorem some_property: "..." sledgehammer
If one of the external provers finds a proof, Sledgehammer reconstructs it in Isabelle’s internal proof language. Crucially, this reconstructed proof is independently verified by Isabelle’s kernel: the structure does not trust external provers but re-verifies the proof idea they discovered internally.
This automation level is practically significant for a team like ours, entering theorem proving for the first time: if humans provide the core proof strategy idea, the machine can fill a substantial portion of the detailed logical steps.
The Pattern of Invariants: Proving “What Always Holds”
The central technique in state transition system verification is proving invariants. An invariant is a principle stating that if some property holds in the initial state and is preserved by every transition, then it holds in every reachable state.
Formally, for property \(P\) to be an invariant of state transition system \((S, \delta, s_0)\):
$$P(s_0) \wedge \forall s, a. \; P(s) \Rightarrow P(\delta(s, a)) \tag{2}$$
If condition (2) is satisfied, then \(P\) holds in every reachable state.
Let us see concretely how this pattern works in regulatory state verification. One invariant we want to prove is regulatory state consistency: “if an asset’s regulatory state is FROZEN on one chain, that asset cannot be freely traded on any chain.”
In Isabelle/HOL:
definition regulatory_consistent :: "global_state ⇒ bool" where
"regulatory_consistent gs ≡
∀ aid. (∃ c. gs c aid = FROZEN) ⟶
(∀ c'. gs c' aid ∈ {FROZEN, SEIZED, CONFISCATED, RESTRICTED})"
This definition says: “for any asset ID aid, if it is FROZEN on some chain c, then it must not be ACTIVE on any chain c'.”
To prove this is an invariant, we apply condition (2). Initial state: all assets are ACTIVE (or not yet registered), so the premise “\(\exists c. \; gs(c, aid) = \text{FROZEN}\)” is false; therefore the entire proposition is trivially true. Transition preservation: if OSS processes a FREEZE message by transitioning the target asset’s state to FROZEN simultaneously on all linked chains, consistency is preserved.
A critical question emerges here: what does “simultaneously” mean in a distributed system? Due to network delays, there can be moments where an asset is already FROZEN on Chain A but the message has not yet arrived on Chain B. During this moment, the invariant is temporarily violated.
How this problem is resolved depends on how the model’s assumptions are set. Under synchronous network assumptions, “simultaneously” holds literally. Under asynchronous networks, the invariant itself may need modification, for instance, to an eventual consistency form: “consistency is restored within bounded time.”
The interplay between assumptions and invariants will be among the most important design decisions in the upcoming modeling process. Clearly recognizing this question at this point is itself a value of formalization.
Functors: The Mathematics of Structure-Preserving Maps
In the previous article, we presented the Regulatory State Functor as a core design idea, noting its inspiration from Lochbihler’s Merkle Functor. This section addresses what functors are mathematically, and why this abstraction is a fitting tool for verifying regulatory state synchronization.
Categories and the Intuition Behind Functors
Category Theory is the field that studies relationships between mathematical structures. A category consists of three things: objects (mathematical structures: sets, groups, topological spaces, …), morphisms (structure-preserving transformations between objects: functions, homomorphisms, continuous maps, …), and composition (an operation connecting morphisms).
A functor is a morphism between categories. It is a “structure-preserving transformation” from one category to another, mapping objects to objects and morphisms to morphisms while preserving composition structure.
Formally, a functor \(F : \mathcal{C} \to \mathcal{D}\) from category \(\mathcal{C}\) to category \(\mathcal{D}\) satisfies:
$$F(\text{id}_A) = \text{id}_{F(A)} \tag{3}$$
$$F(g \circ f) = F(g) \circ F(f) \tag{4}$$
Condition (3) is identity preservation; condition (4) is composition preservation. These two conditions are the functor laws.
Merkle Functor: Lochbihler’s Precedent
Lochbihler and Marić created the concept of Merkle Functors to formally verify Canton’s authenticated data structures [5]. Their key insight was this: rather than verifying complex transaction trees as a single monolithic structure, decompose them into small, reusable building blocks (functors), prove each block’s properties independently, then derive the overall properties through composition theorems.
The class of Merkle Functors includes sums, products, and function spaces, and is closed under composition and least fixpoints. This means Canton’s hierarchical transaction structures can be naturally expressed as compositions of these building blocks.
The reason this pattern matters is modularity. When a new type of transaction node is added, defining it as a new Merkle Functor instance means existing composition theorems automatically extend.
Regulatory State Functor: Our Hypothesis
The Regulatory State Functor we aim to explore brings this pattern into the regulatory domain.
The idea is as follows. View each chain’s regulatory state transition system as a category: objects are regulatory states (ACTIVE, FROZEN, SEIZED, …), morphisms are state transitions induced by regulatory actions (FREEZE: ACTIVE → FROZEN, …), and composition is sequential application of regulatory actions.
The Regulatory State Functor is a structure-preserving map from Chain A’s regulatory state category to Chain B’s. Satisfying the functor laws means: “doing nothing” is preserved (condition 3), and “FREEZE then SEIZE” equals “propagate FREEZE then propagate SEIZE” (condition 4).
And a natural transformation (a structure-preserving map between two functors) corresponds precisely to OSS’s state synchronization. The condition that natural transformation \(\eta\) satisfies is:
$$\eta_B \circ F_A(f) = F_B(f) \circ \eta_A \tag{5}$$
for all morphisms \(f\). This is the category-theoretic generalization of the homomorphism condition (1) seen earlier.
There is something we must honestly acknowledge at this point. We do not yet know whether this functor approach represents an appropriate level of abstraction or an excessive one. As we noted in the previous article, cross-chain regulatory homomorphism (Property 1) can be proved directly without functors. Functors are a design choice for extensibility, not a prerequisite for proof. This judgment will be made during the actual modeling process.
One thing, however, is clear. In a logical system that cannot even express this level of abstraction, the choice itself does not exist. What HOL provides is not just direct expressiveness but an expansion of the design space.
Expressing Functors in Isabelle/HOL
Expressing functors in Isabelle/HOL is different from directly transcribing textbook definitions from category theory. Since Isabelle/HOL is type-theory-based rather than set-theory-based, categories and functors are encoded via type classes or locales.
The key technique in Lochbihler’s approach is shallow embedding using Isabelle’s datatype package and BNF (Bounded Natural Functor) framework [5]. Rather than defining functors on top of a separate category theory library, this approach lets Isabelle’s built-in type system itself provide functorial structure.
For instance, the simplest form of a regulatory state functor sketch might look like:
locale regulatory_state_functor =
fixes map_state :: "('a ⇒ 'b) ⇒ 'a reg_system ⇒ 'b reg_system"
assumes identity: "map_state id = id"
assumes composition: "map_state (g ∘ f) = map_state g ∘ map_state f"
A locale is Isabelle’s mechanism for theories with explicit assumptions. Here map_state is polymorphic over type variables 'a and 'b, and the two assumptions correspond precisely to functor laws (3) and (4).
Instantiating this locale for a specific chain:
interpretation evm_functor: regulatory_state_functor evm_map_state by (standard) (auto simp: evm_map_state_def)
If this structure works, adding a new chain requires only a single interpretation line and the corresponding chain’s map_state definition; existing theorems become automatically available. This is the practical advantage of the functor approach.
We emphasize again: these code fragments are pre-modeling sketches. Whether this structure fits our problem must be verified during the modeling process. In particular, the definition of the reg_system type, how map_state transforms regulatory actions, and how asynchronous message propagation is reflected are open questions.
What Can We Build With This Tool
We have established three things so far.
First, the property of cross-chain regulatory homomorphism requires quantification over functions, which lies outside the expressiveness of first-order logic. HOL is the minimal extension that crosses this boundary.
Second, Isabelle/HOL’s datatype, fun/inductive, and theorem/proof constructs directly express regulatory state spaces, transition rules, and property proofs. The finiteness of regulatory states and the clarity of transition rules align well with this tool’s automation capabilities.
Third, the functor concept provides the theoretical foundation for the Regulatory State Functor, and Isabelle/HOL’s locale mechanism offers a viable path for implementing this abstraction. Whether this represents the right level of abstraction remains an open question.
The next step is clear. Fixing the scope, assumptions, and threat model of cross-chain regulatory homomorphism (Property 1). Whether the network is modeled as synchronous, asynchronous, or partially synchronous; whether Byzantine nodes are included; what level of message delivery is guaranteed: these decisions determine the model’s shape and, consequently, the scope and meaning of the proof.
Throughout that process, we will honestly record what we tried, where we hit walls, and how we resolved them (or did not). We remind ourselves once more that the true value of formal verification lies not in the final theorem but in the design flaws discovered and corrected along the way.
References
[1] Church, A. (1940). “A Formulation of the Simple Theory of Types.” The Journal of Symbolic Logic, 5(2), 56–68. https://doi.org/10.2307/2266170
[2] Nipkow, T., Paulson, L.C. & Wenzel, M. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer LNCS 2283. https://isabelle.in.tum.de/doc/tutorial.pdf
[3] Blanchette, J.C., Bulwahn, L. & Nipkow, T. (2011). “Automatic Proof and Disproof in Isabelle/HOL.” In: Frontiers of Combining Systems (FroCoS 2011), pp. 12–27. https://doi.org/10.1007/978-3-642-24364-6_2
[4] Nipkow, T. & Klein, G. (2014). Concrete Semantics: With Isabelle/HOL. Springer. http://concrete-semantics.org/
[5] Lochbihler, A. & Marić, O. (2020). “Authenticated Data Structures As Functors in Isabelle/HOL.” In: FMBC 2020. OASIcs vol. 84, 6:1–6:15. https://doi.org/10.4230/OASIcs.FMBC.2020.6