THE ORACLE STATE MACHINE
State should move as one.
An asset's token, its custody record, its contract and its regulatory status usually live in different systems. Oraclizer is built to move them in one step that either happens everywhere or nowhere.
Designed for tokenized securities, institutional ledgers, and cross-domain asset operations.
The affected domains commit together or roll back together. A partially applied result is outside the permitted state space.
WHY STATE SYNCHRONIZATION
A price can be delivered. A financial state has to be coordinated.
A data feed can tell a contract that a price changed. It cannot, by itself, keep a token, a custody record, an off-chain contract, and a regulatory action in the same causal state. Oraclizer treats the transition, its authority, its policy context, and its result as one protocol object.
Data feed
Observe a value. Publish an update. Leave each destination to determine what happens next.
Oracle state machine
Bind the affected domains. Verify the transition and its context. Commit one result, or leave every bound domain unchanged.
MODEL-LEVEL ASSURANCE
Prove the model. Refine the system.
Oraclizer uses machine-checked formal models to establish its declared properties. The assurance program targets core-wide refinement: a traceable correspondence from those formal semantics through protocol and implementation layers. As refinement obligations are discharged, model-level assurance extends to the exact mapped code and deployment boundary.
Mechanized semantics
State, authority, transition, failure, and preservation properties are stated in Isabelle/HOL so the proof kernel checks the declared model itself.
Adversarial examination
Counterexamples, mutation tests, assumption ledgers, and independent recomputation are used to expose vacuous proofs, hidden preconditions, and claims that exceed their evidence.
Core-wide refinement target
Explicit obligations map formal state and transition semantics into protocol behavior, implementation code, compiled execution, and deployment identity. A system-level claim is made only for the boundary whose correspondence has been demonstrated.
THEORY INTO SYSTEMS
From a proved model to an assured system.
The figure maps mechanized semantics, explicit refinement obligations, executable components, and deployment evidence into one assurance path. It distinguishes the model-level properties demonstrated today from the core-wide refinement target.
BUILT BY ORACLIZER
Proofs that scale.
Rules that are proven.
An oracle state machine needs two kinds of proof: proof that a ledger holds what it claims and changed correctly, and proof that a regulatory action follows rules that keep the books consistent. We built StateSync-GKR for the first and ERC-TRUST for the second. Both are public, and each can be adopted on its own.
StateSync-GKR
Lighter to prove.
Faster to check.
Built as the proof engine for Oraclizer's state synchronization, and now a product in its own right. It proves that a record is present, absent or correctly changed in its sparse Merkle tree, its GKR core extends to other layered computations, and its path from state semantics to verification is machine-checked. Research, development and testing are free; generating proofs in production requires a commercial license.
less memory to generate the same proof
faster to verify the same proof, at the deepest tree tested
lower per-request proving time when the circuit is prepared once
requests served in 15 minutes on 48 cores, every one within 500 ms
- Regulated assetsHolder registers and restricted lists
- BlockchainsRollup and app-chain state kept in its tree
- Data systemsKey-value stores and registries
- AI and custom computationLayered circuits through your own frontend, from model arithmetic to data pipelines
Controlled comparisons against StateSync-GKR's own reference implementations. The engine paper reports the full method.
ERC-TRUST
Mathematically proven rules.
Compiled code checked against them.
Mathematical assurance for regulatory actions on security tokens. All six actions, from freeze to liquidation, and their three reversals follow rules proven to keep supply, custody and case records consistent. The compiled contracts are checked against those rules execution by execution, on native tokens and on ERC-3643 tokens.
actions and reversals proven to keep the books consistent
executions of the compiled contracts checked against the rules
| Action | Native | ERC-3643 Partial | ERC-3643 Hook |
|---|---|---|---|
| FREEZE | |||
| SEIZE | |||
| CONFISCATE | |||
| RESTRICT | |||
| RECOVER | |||
| LIQUIDATE | |||
| UNFREEZE | |||
| RELEASE | |||
| UNRESTRICT | |||
| Malformed | 16 commands | 13 commands | 13 commands |
- Native9 of 9 operations · applied and not applied · 16 malformed
- ERC-3643 Partial9 of 9 operations · applied and not applied · 13 malformed
- ERC-3643 Hook9 of 9 operations · applied and not applied · 13 malformed
Partial: existing ERC-3643 tokens through an adapter. Hook: new ERC-3643 deployments with a transfer hook.
- 01Prove the rules
Isabelle/HOL theorems for six actions and three reversals.
- 02Check the executions
Every action, applied and not applied, in three token profiles.
- 03Rebuild the bytes
Two isolated clean builds produce byte-identical contracts.
Among the security-token standards we reviewed, we found none that publishes machine-checked proofs. ERC-TRUST publishes its rule proofs and re-checks them in public on every change.
Proofs cover the rules; the code checks cover 96 specific executions, not every possible transaction.
PRECONDITIONS
Six problems came before the machine.
An oracle state machine begins where a data feed stops. Before one could exist at all, six problems had to be answered, and no two of them belong to the same discipline. Each is a precondition rather than a feature, which is why answering five of them still leaves nothing that runs.
A vocabulary for regulation
A freeze, a seizure, a forced transfer. Before any of these can be synchronized, a machine has to know what they are, who is entitled to order them, and what happens when one fails. No such vocabulary existed. Two years of regulatory research came before the first line of protocol design, and the requirement set it produced became ERC-8319.
Traceable privacy
Regulated assets need two things that normally exclude each other: a history a supervisor can audit, and detail a competitor cannot read. Selective disclosure at the identity layer and transaction data held off the public chain let both hold at once, so confidentiality stops being something you buy by making the record unauditable.
Time that separate chains agree on
Chains disagree about when something is final, and a cross-domain commit that ignores the disagreement is a reorganization waiting to be discovered. The core tracks finality per chain and commits only once every bound domain has settled. That is the difference between a synchronization and a hopeful write.
Sequencing that is neither centralized nor indifferent
A freeze that waits its turn is a freeze that failed, so ordering cannot be indifferent to what it orders. Yet a sequencer that can be told what to order is the thing decentralization was supposed to prevent. Oraclizer separates the layers: operations stay fully decentralized, regulatory intervention stays transparent and bounded, and D-quencer follows a deterministic rule that nobody gets to override.
Proving that keeps a deadline
Continuous synchronization means proving the same sparse-Merkle state again and again, against a clock, and a proof that arrives late is a proof that did not matter. That repetition is the workload StateSync-GKR was built for.
A cost that survives repetition
A synchronization cycle that costs more than the asset it moves never becomes infrastructure. L3 execution, off-chain data availability, external proof verification and incremental state updates are in the design for one reason: to make continuous synchronization something an institution can afford to run continuously.
Together, these constraints define the architecture of the oracle state machine.
SYSTEM ARCHITECTURE
No layer you have to take on faith.
Protocol meaning, execution, proving, sequencing and external integration are kept apart, so each one can be specified, tested and argued with on its own.
OIP v0.5
The full protocol specification is public: messages, routing, validation, regulatory actions, cross-domain coordination and conformance. Anyone can read what Oraclizer commits to before there is a system to run it against.
Read OIP v0.5 (opens in a new tab)Oracle State Synchronization System
The execution core. It holds one synchronization cycle open across every participating domain, binds them, checks the transition against its authority and policy, then commits everywhere or nowhere. Rollback is a designed path here, so a refusal anywhere returns every bound domain to its prior state and the design admits no outcome that leaves half of them updated.
Implementation link reservedD-quencer
Sequencing built for synchronization cycles rather than for generic transactions. It orders deterministically under declared Byzantine assumptions and lets a time-critical regulatory action take priority, because a freeze that waits its turn is a freeze that failed.
Architecture in developmentStateSync-GKR
The proving layer of the stack, now available as StateSync-GKR. A reusable Rust sumcheck and GKR engine that proves a record is present, absent or correctly changed against a committed root, prepares each circuit once and runs independent proofs in parallel.
Visit StateSync-GKRIntegration layer
The RWA Registry, Canton Driver, and cross-chain message-integrity layer connect asset metadata, enterprise ledgers, and external state paths without making one external system the source of every truth.
Review the architecture (opens in a new tab)SUBSCRIPTION GAS
Metered by the session, not by the message.
Ethereum charges per transaction, but a synchronization cycle spans domains, holds state open and completes as one unit. Oraclizer meters the session an asset and its owner hold open, counting only the bound transitions that committed. Every input to a charge lands in the public event log, so anyone holding a bill can recompute it from consensus state.
USE CASES
What becomes possible when the whole asset moves.
About $60 billion of real-world assets are already tokenized, and most of that sits still, because the token can move while the interest, maturity, eligibility and regulatory status behind it do not. Oraclizer's own analysis puts 54 to 68 percent of the tokenized market on the side that needs its state moved rather than reported, bonds highest at 78 percent. On 2030 projections that is $1.1 trillion to $3.4 trillion of assets no oracle was built to serve.
Collateral that can actually be liquidated
A tokenized bond is only collateral if a liquidation can move the token, the custody record and the legal claim in one step. Where it cannot, lenders discount the asset or refuse it outright, which is why real-world collateral still sits at the edge of on-chain credit. A price feed can tell a lender what the bond is worth. It cannot move the claim behind it.
Regulatory actions that execute
A freeze, a seizure or a forced transfer arrives as an instruction with authority behind it, not as a request to somebody's back office. Each action carries its own authority, state effect, failure behavior and receipt, so a regulated asset can trade in a permissionless venue without that venue having to act as the regulator.
State synchronization with Canton's $6 trillion
Institutions put tokenized bonds, funds, repo and mortgages on Canton precisely because those assets will not settle on a public chain. They are worth considerably more the moment they can reach on-chain venues without leaving the compliance perimeter, and that takes a transition which commits on the institutional ledger and the public chain together, or on neither.
Assets that run their own lifecycle
Coupons, maturity, redemption and corporate actions move the token and the contract behind it in the same step, instead of being reconciled afterwards by two teams comparing records. The asset carries its own lifecycle.
These are the workflows the architecture is designed for. Each one is specified in the public protocol and modeled formally, ahead of production.
STANDARDS
A freeze has to mean the same thing everywhere.
Oraclizer's standards work gives regulatory actions, their authority, their outcomes and their receipts a machine-readable identity, so separate ledgers can agree on what actually happened to an asset.
ERC-8319 · Regulatory Compliance Protocol
Six regulatory actions, each with a defined authority, state effect and failure behavior, and thirty-one requirements drawn from fifteen financial regulators organized under five principles. Assigned number 8319 in the Ethereum ERCs repository. It gives a token standard a common way to state which regulatory obligations it actually enforces and which it leaves to somebody else.
ERC-TRUST · Typed Regulatory Uniformity for Security Tokens
An execution standard for regulatory actions on security tokens. Actions, authority, outcomes, failures and receipts get machine-readable identities, while policy stays specific to each environment. Its rules are mathematically proven, and its compiled code is checked against them on 96 registered executions across three token profiles. The draft and reference implementation are public and unaudited, and the ERC has not yet been submitted.
Typed Regulatory Actions and Execution Receipts for Canton Tokens
A Canton Improvement Proposal for interoperable regulatory actions and typed execution receipts in Canton token implementations, leaving policy and authority models to each implementation. Canton is one of the few institutional ledgers built on a formal ledger model, which is what makes a cross-domain claim about it provable.
Not submittedPUBLISHED RESEARCH
Read the argument before you trust the system.
Most protocols publish a paper after the product. Oraclizer published the argument first. The regulatory model the protocol was derived from, a machine-checked theory of cross-domain state preservation, a machine-checked semantics for the regulatory actions a security token can be made to execute, and the long-form work behind every major design decision are all public, and the formal development can be rerun by anyone who would rather check it than take it on trust.
Regulatory Compliance Protocol
A framework for measuring how completely a token standard represents regulatory requirements and enforcement state, applied to the standards already in use. Its requirement set is what ERC-8319 was built from.
View on arXiv (opens in a new tab)The Cross-Domain State Preservation Functor
A machine-checked Isabelle/HOL theory of what it takes to preserve state across systems that do not share a model of it, organized as a functor. When both sides are formally specified, as a public chain and Canton's ledger model are, the connection between them can be proved.
View on arXiv (opens in a new tab)Mechanizing Typed Regulatory Actions for Security Tokens
A machine-checked Isabelle/HOL semantics for the regulatory actions a security token can be made to execute, keeping what was applied, what was refused and what merely failed apart from one another. It also proves a limit on itself: two worlds that disagree about title and settlement look identical from inside the contract, so those facts have to arrive as evidence. For one implementation candidate the evidence is reported tool by tool, with the reach of each result stated separately.
View on arXiv (opens in a new tab)Formal Verification
Public machine-checked artifacts cover cross-domain state preservation, synchronization-degree monotonicity, and regulatory-action semantics. The degree result is proved in both directions: a higher degree safely carries a lower-degree asset, and a lower one provably cannot. The repository is run as a maintained public research surface, with reviewed changes, reproducible sessions, released artifacts and a security reporting path.
Explore formal verification (opens in a new tab)StateSync-GKR: Machine-Checking the Trust Chain from Sparse-Merkle State Transitions to GKR Verification
A machine-checked Isabelle/HOL argument that the engine's circuits accept exactly the valid state operations, in both directions, and that a false claim passes the modeled verifier only within a proved probability bound, carried to the exact extension field the verifier uses. It also marks where the link to the shipped Rust code is conditional.
View on arXiv (opens in a new tab)StateSync-GKR: Design and Evaluation of a Reusable Sparse GKR Engine
How a sparse prover, derived wiring, reusable preparation and independent parallel proofs turn into measured gains: about 89 times less memory than the engine's dense reference and up to 23.68 times faster prepared verification. Each result is reported with the conditions it was measured under.
arXiv link to followStructural OEV Elimination through State Synchronization
OEV exists because an oracle update becomes visible before the position it moves has settled, and extraction lives in that interval. The post shows what happens when both events are bound into one all-or-nothing transition: the set of states an extractor needs is empty, so the window is not narrowed or auctioned off, it stops existing. It also draws the line between what this removes and what no update design can remove.
Read the discussion (opens in a new tab)Research Library
Long-form research across state synchronization, formal methods, protocol design, regulation, real-world assets and tokenized markets. Most of the design decisions in Oraclizer were argued here first.
Browse the library (opens in a new tab)WHO WE BUILD WITH
The strongest systems are built in concert.
A protocol for regulated assets cannot be validated from inside the project that wrote it. Oraclizer builds alongside a zero-knowledge engineering company, an external proof-verification network, a policy leader co-authoring the standard, and a consensus research group whose interest is in finding where the model breaks.
Horizen Labs
A zero-knowledge engineering company and a co-author of ERC-8319, working with Oraclizer on the standard itself and on the proving and verification path the architecture rests on. The collaboration runs from the regulatory text down to the cryptography that has to carry it.
Visit Horizen Labs (opens in a new tab)zkVerify
Every synchronization cycle ends in a proof, and what it costs to verify those proofs decides whether continuous state synchronization is economically viable at all. zkVerify is where Oraclizer sends that verification: a network built to make proof checking cheap enough to do constantly, and independent enough that the check does not happen inside the system being checked.
Visit zkVerify (opens in a new tab)Blockchain Association
Dan Spuller, Executive Vice President of Industry Affairs at the Blockchain Association, co-authors ERC-8319 in an individual capacity. The Association represents the digital-asset industry before US regulators and lawmakers, and a standard that names regulatory actions reads differently when that vantage point is present from the first draft.
Visit Blockchain Association (opens in a new tab)Floating Pragma
A consensus research group Oraclizer takes part in. The current thread is a shared state-preservation benchmark connecting Oraclizer's Isabelle work with Bernhard Müller's Observer-Patch Holography program. Müller was an original project lead and author of the OWASP Mobile Application Security Verification Standard, helping establish a common security standard for mobile applications.
Visit Floating Pragma (opens in a new tab)FREQUENTLY ASKED
Straight answers.
01What is an oracle state machine?
An ordinary oracle publishes a value and stops. The token, the custody record, the registry entry and the regulatory status are then updated by separate systems on separate schedules, and the gaps between those schedules are where reconciliation work and disputes live. An oracle state machine treats the transition, the authority behind it, the policy it ran under and its result as one coordinated state. A freeze then carries the same meaning and the same force in every domain it reaches, which is the property a regulator needs and a delivered message cannot provide.
Read the core concept (opens in a new tab)02How is S₃ different from ordinary oracle delivery?
Ordinary delivery is a report. The oracle writes a value, each dependent system reacts on its own timing, and one refusal is enough to leave the same asset in two versions that people reconcile by hand. S₃ binds them instead. A liquidation ordered against the custody record and the token burn that has to follow it become one transition: they land together or neither lands. The position cannot be closed on one book and left open on another, which is what an enforcement order has to be able to assume. By design, a partially applied result sits outside the permitted state space rather than being an error to detect and repair afterward.
Study state synchronization (opens in a new tab)03Does Oraclizer eliminate oracle extractable value?
For any action bound into a single all-or-nothing transition, yes, and by construction rather than by auction. Extraction needs a moment where the update is visible and its consequence is not yet committed, and atomic binding makes that moment unreachable. The atomicity is machine-checked. What it does not touch is what a participant already knew before the transition began, and no update design closes that one.
Read the argument (opens in a new tab)04When is the Oraclizer testnet expected?
Q1 2027. The bar is a testnet an institution can run against, and that is what sets the work in front of it. Full refinement of the Oraclizer core carries the mathematical assurance from the model down the whole product cycle. The protocol has to be structurally mature enough to build on. StateSync-GKR has to land its proofs inside the synchronization window. Sequencing has to stay decentralized without stalling, and institutional ledgers have to be driven through the interfaces they actually expose.
05Who is Oraclizer built for, and how is usage measured?
Asset issuers, tokenization platforms, custodians and regulated market infrastructure: anyone who needs one state change to hold across tokens, custody, registries, policy and connected ledgers. Blockchains have billed the same way since the first one, pay-per-gas, a toll on every transfer. That unit does not exist in state synchronization, where one change spans domains and means nothing until the whole cycle closes. Oraclizer bills pay-per-sync: you pay for synchronization that completed, metered over the session an asset holds open, with every input published so the bill can be recomputed from consensus state.
Review the architecture (opens in a new tab)06How is Oraclizer different from Chainlink CCIP on Canton?
Chainlink CCIP carries messages and tokens both ways between Canton and a public chain, which in this hierarchy is two S₁ flows, not one binding: each side reports, each side decides alone, and nothing holds those decisions to the same answer, so the two can end up in different states. Oraclizer runs the same crossing at the top of that scale, S₃ atomic binding: both states move as one transition with only two possible endings. Its CDSP Functor imports Canton's ADS Functor proof in Isabelle/HOL and carries it past Canton's boundary to every bound domain, so what holds inside Canton holds in a machine-checked cross-domain result. To our knowledge no other route does this.
Read the state-preservation research (opens in a new tab)ORACLIZER LABS
One asset should never become two.
Oraclizer Labs is a research and protocol organization building the oracle state machine, so that a regulated asset stays one asset across every system that holds it. The work started in regulation. Two years of research across fifteen financial regulators produced the Regulatory Compliance Protocol, and the protocol design followed from what that research found. The team has been designing institutional digital-asset platforms on DAML and Canton since 2019.