Formal verification artifacts for the Oraclizer oracle state machine, verified in Isabelle/HOL.
This repository contains machine-checked proofs of safety and liveness properties for cross-domain state synchronization in Byzantine environments. The proofs establish two independent but complementary guarantees:
- Safety — Regulatory actions (freeze, seize, confiscate, etc.) applied on one blockchain network are faithfully reflected across all connected networks, preserving the structure of state transitions.
- Liveness — Under Byzantine faults (f < n/3), regulatory actions are resolved deterministically, no asset can be permanently locked, and no pending request is starved indefinitely.
The core abstractions are two hierarchies of Isabelle/HOL locales:
- Cross-Domain State Preservation Functor (Property 1): Models state synchronization as a functor between categories of state machines, where the naturality condition guarantees structural preservation of transitions.
- Priority Resolution and Liveness Locales (Property 2): Captures deterministic ordering, deadlock avoidance, and starvation freedom as reusable abstractions for leader-based Byzantine consensus systems.
The two properties are connected via an assume-guarantee pattern: the liveness proof of Property 2 discharges the honest-node assumption in Property 1's safety proof, lifting conditional safety into unconditional guarantee under the Byzantine model.
Design lineage. Inspired by Lochbihler's Merkle Functor (AFP), which abstracted authenticated data structures into composable building blocks. This work extends that pattern along two complementary axes: cross-domain state preservation (safety) and priority-based liveness under Byzantine faults.
Status: Complete (2026-02-28). No sorry or oops. AFP submission under editor review.
What is proven:
| Theorem | Statement |
|---|---|
regulatory_homomorphism |
After synchronization, all connected chains agree on the regulatory state |
valid_state_preservation |
Synchronization preserves the global validity invariant (consistency ∧ no spurious locks) |
reg_multi_domain_instantiation |
The generic framework applies parametrically to the regulatory model for any finite domain set |
sequential_preservation |
State preservation extends from single actions to arbitrary action sequences (naturality generalization) |
confiscated_terminal |
CONFISCATED is an absorbing terminal state |
confiscate_universal |
CONFISCATE is reachable from every non-terminal state |
no_self_loops |
No transition maps a state to itself |
sync_isolation |
Synchronization on one asset does not affect other assets |
Model:
- 5 regulatory states: ACTIVE, FROZEN, SEIZED, CONFISCATED, RESTRICTED
- 7 regulatory actions: FREEZE, SEIZE, CONFISCATE, RESTRICT, UNFREEZE, UNRESTRICT, RELEASE
- 35 transition rules (deterministic, partial)
- Preemptive locking for concurrent regulatory action prevention
- Synchronization protocol: lock → update all connected chains → unlock
Status: Complete (2026-04-02). No sorry or oops. Ready for AFP entry update after Property 1 acceptance.
What is proven:
| Theorem | Statement |
|---|---|
select_highest_deterministic |
Given a finite non-empty message set with injective priorities, the highest-priority message is uniquely determined |
select_highest_in_set |
The selected message is always a member of the input set |
select_highest_is_max |
The selected message has the maximum priority among all messages in the set |
lock_eventually_expires |
Every lock has a bounded lifetime; no resource is locked indefinitely |
deadlock_freedom |
Any lock released within the timeout bound; no circular wait can persist |
starvation_bound |
Under the fair leader assumption, if there are pending requests, at least one is processed within fairness_bound epochs |
eventual_completion |
All pending requests are eventually processed (by well-founded induction on pending count) |
priority_key_injectivity |
The D-quencer priority key uniquely identifies messages given distinct authority/timestamp/action/node |
honest_majority |
Under the BFT threshold n ≥ 3f + 1, the number of honest nodes exceeds 2f |
combined_safety_liveness |
Connects Property 1's safety with Property 2's liveness: under Byzantine faults, cross-domain regulatory state is synchronized deterministically, without deadlock, and without starvation |
Model:
- 3 authority levels: Regional, National, International (RCP jurisdictional hierarchy)
- 4-component priority key: (authority_rank, inverted_timestamp, action_severity, inverted_node_id)
- BFT threshold: n ≥ 3f + 1 (standard Byzantine fault tolerance)
- Timeout-based locking (models VRF-randomized leader election abstractly)
- Fair leader assumption: within any
fairness_boundepochs, at least one honest leader is elected
Design pattern. The liveness proof uses assume-guarantee reasoning: the fairness assumption abstracts VRF randomness as a deterministic condition, and Property 2 discharges the honest-node assumption that Property 1 implicitly required. Together they establish unconditional safety + liveness under the Byzantine model.
Status: Not started. Planned after Property 1 AFP acceptance.
Property 3 will compose the Cross-Domain State Preservation Functor with Lochbihler's Merkle Functor (AFP entry ADS_Functor) to establish end-to-end assurance from Canton off-chain ledgers through OSS synchronization to on-chain EVM state.
.
├── Cross_Domain_State_Preservation/ # AFP entry
│ ├── State_Preservation.thy # Property 1 generic theory (383 lines)
│ │ # 4 locales: state_machine,
│ │ # state_preservation,
│ │ # symmetric_state_preservation,
│ │ # multi_domain_preservation
│ ├── Regulatory_Instance.thy # Property 1 regulatory instance (1053 lines)
│ │ # State machine interpretation,
│ │ # synchronization protocol,
│ │ # regulatory homomorphism,
│ │ # valid state preservation,
│ │ # multi-domain instantiation
│ ├── Priority_Resolution.thy # Property 2 generic theory (422 lines)
│ │ # 3 locales: priority_system,
│ │ # deadlock_free_locking,
│ │ # fair_leader_system
│ ├── DQuencer_Instance.thy # Property 2 D-quencer instance (491 lines)
│ │ # Authority levels, priority keys,
│ │ # BFT system locale,
│ │ # liveness instantiation,
│ │ # combined safety + liveness theorem
│ ├── ROOT # Isabelle session configuration
│ └── document/
│ └── root.tex # LaTeX document for AFP
├── FORMAL_MODEL_MAPPING.md # Model-to-implementation correspondence
├── docs/
│ └── document.pdf # Generated theory document (from AFP build)
├── LICENSE
├── CONTRIBUTING.md
└── README.md
- Isabelle 2025-2 (or later)
# Clone the repository
git clone https://github.com/oraclizer/formal-verification.git
cd formal-verification
# Build and check all proofs
isabelle build -d . Cross_Domain_State_PreservationExpected output: Finished Cross_Domain_State_Preservation with no errors.
isabelle build -d . -o document=pdf Cross_Domain_State_PreservationThe generated PDF will be in the session output directory.
This work is submitted to the Archive of Formal Proofs under the entry name Cross_Domain_State_Preservation.
- Initial submission date: 2026-03-25 (Property 1)
- Status: Under editor review
- Submission URL: AFP Submission
Property 2 is complete and will be submitted as an entry update after Property 1 acceptance.
- Kim, Jinwook (2026). Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL. arXiv:2604.03844 [cs.CR]. https://arxiv.org/abs/2604.03844
- Kim, Jinwook and Hong, Jonghun (2026). A Regulatory Compliance Protocol for Asset Interoperability Between Traditional and Decentralized Finance in Tokenized Capital Markets. arXiv:2603.29278 [cs.CY]. https://arxiv.org/abs/2603.29278
- Lochbihler, A. (2020). Formalization of Authenticated Data Structures as Functors in Isabelle/HOL. FMBC 2020. AFP Entry: ADS_Functor
- Oraclizer Research: Proofs — Research publications on formal verification
- Oraclizer Documentation — Technical documentation
BSD License. See LICENSE for details.
- Author: Jinwook Kim (Jay) — jay@oraclizer.io
- Twitter/X: @Oraclizer