TL;DR
- OIP is Oraclizer's protocol specification: the rules by which state and regulatory orders move between domains. Version 0.6 is still in development, and OIP v0.6 development pairs each feature's rules with Isabelle/HOL proofs, tests derived from those proofs, and code.
- The first thing that work flagged was our own public wording. Implemented as written, v0.5 could have paid the same asset twice, and we have corrected it in public.
- Regulatory execution is where it matters most. A single freeze order spans an interval from issue to publication, and a proved state machine allows five transitions the legal rules forbid. Executing an order is a path, and a path can be questioned mathematically.
- The defects share a shape: a rule reads a stand-in, such as a clock, a flag or a copy, at the moment it should read the record of what happened.
- OSS does not exist yet, atomicity across external ledgers is open, and the Canton items have not moved.
Where OIP Sits, and Three Statements from v0.5
OIP (Oracle Interoperability Protocol) is the rulebook of Oraclizer. It specifies which messages cross between domains, in what order, and when a state change or a regulatory action takes effect. The system that will run those rules is OSS (Oracle State Synchronizer), and OSS does not exist yet. OIP is at the prototype stage.
What we are trying to do is easy to state: make an asset's state and its regulatory orders move together across two domains. Writing rules is only part of that, so we also check, with proofs and code, whether the rules behave that way. This article is a working record of OIP v0.6 development, written before the specification is public, about what that checking has exposed so far.
OIP v0.5 Checkpoint left us with three statements [1], and they have aged differently.
- "We have reached the point where two implementations can read the same specification and behave the same way." This survives only in a narrow sense. Two implementations could read the same wording and agree, and that wording held a path to paying twice.
- "Some slot, invisible at the previous stage, will reveal itself." This held, and the slots turned up deeper than we had guessed.
- The checkpoint named Canton Driver multi-Signatory support and key rotation, RWA Registry Solidity signatures and Authority Registry integration as "the major work items of v0.6." All of them are still major and still open. The road we took first is what changed.
We are leaving the checkpoint as it is. It records what we thought at v0.5, and the corrections live here.
OIP v0.6 Development: Rules, Proofs and Code Together
The v0.5 method was to lay two documents side by side, the specification and the verification plan. The checkpoint said that "A simple difference in working method changed the entire downstream cost structure," and we still think so. Comparing documents, though, can only tell you that the documents agree.
Going into OIP v0.6 development, we kept stacking new proofs on the public ones. Proofs accumulated while the product's requirements stayed open, so we asked whether the method itself fit. Two reviews that had not seen our earlier verdicts gave the same answer: every remaining item could pass and not one product requirement would close. That was the hardest thing we heard in this work. The public proofs were still correct. They prove what they say, and a product asks for more.
So we changed the structure. The public proofs stay as the floor, and on top of them each feature is built as one loop: rules, a proof, tests derived from the proof, code written apart from the proof using only the rules and tests, and a review that has not seen earlier verdicts. A defect goes back to whichever part of the loop it belongs to.
The order changed too. Rather than working down the public Open Issues list, we started with the paths that carry money, authority and regulatory execution, because mistakes there are the hardest to undo. The rules and the reference code are private for now, so what follows is told at the level of events.
Most of what follows came from the joins in that loop. Where rules met proofs, sentences broke. Where proofs met code, the model turned out too coarse. Two documents side by side never had that contact surface.
A Clock Cannot Say Which Outcome Happened
This is the simplest case, and the one place in this article where we would say we came close to real trouble. The public v0.5 wording read as if the expiry of a preemptive lock's TTL (time to live) released the lock and restored the earlier state. The v0.5 checkpoint also said "after expiration, recovery proceeds through new lock acquisition."
Take a source domain holding 10 units. To send 5 to a destination, it locks and burns 5, then waits for finality. The TTL passes. By the old wording the source takes its 5 back and holds 10 again. But the finality certificate was only slow, and when it lands, the destination credits 5. An asset of 10 units is now 15.
A longer TTL does not fix this, because the two futures in the figure are the same state at the moment of expiry. Our public lock proof says so directly: "Identical expired pending states do not determine different stable outcomes," closed by the theorem no_timeout_only_classifier_can_recover_both_outcome_consumers [2]. No rule that reads only elapsed time can be right in both futures. The root is old: in an asynchronous system, a slow participant and a dead one look the same [3]. A recent Isabelle/HOL proof makes a related point, that recovery from source-side records alone must either duplicate an effect or lose one [4].
Our documentation now reads: "TTL expiry no longer releases the lock or restores the earlier state: it starts retry, reconciliation and escalation, and the lock is resolved by a verifiable finality certificate or by verifiable reversal or reorg evidence. The earlier wording allowed the same asset to be paid out twice." [5] Our internal specification had already moved on, so a proof did not discover this first. The public wording had fallen behind. No deployment ever ran on it, yet it sat where an outside developer could read it, and implemented as written it produces the run above.
The v0.5 sentence on recovery after expiry, selected in the published checkpoint
This case gives us a word for the rest of the article. A stand-in is whatever a rule reads in place of the event it is really asking about: a clock in place of an outcome, a flag in place of an elapsed deadline, a copy in place of the record. Stand-ins are usually right. So rules built on them read well on paper and break only in the runs where the stand-in and the event come apart.
Why Regulatory Execution Has to Be Proved
A double payment shows up on a ledger. A failed regulatory order is quieter. A freeze order is a legal instruction. When a protocol reports an asset as frozen, an authority relies on that report and a holder loses the use of the asset because of it. If the report is wrong, the damage does not stay a software defect, because someone has already acted on it.
We have said that regulatory compliance is part of the protocol. Having said that, whether an order takes effect is the protocol's question to answer, and asking it mathematically is a responsibility we take on.
Others have walked ahead of us where law meets formal methods. Catala turned legislative text into a formal language and uncovered a bug in an official implementation of French family benefits [6], and automated reasoning has been applied to the algorithms of exchanges and dark pools with regulation in view [7]. Those efforts ask what a rule means and whether an algorithm follows it.
What we have found much less of, in the material we have read, is the next question. Does a lawful order take effect across domains? Does that effect hold through a timeout, a restart, a restored backup and a revocation? The lawfulness of the order is an input here, and the path of execution is what we try to prove.
Between Issuing a Freeze and Enforcing It
We describe S3, atomic state binding, this way: "Every bound domain commits together or rolls back together. A partially applied result is outside the permitted state space." Read quickly, that suggests an order landing on both sides in one instant, and our internal documents did say there was no intermediate state. The proof showed real runs reaching a step where the order had been issued and not yet applied. One freeze spans an interval.
The interval was hazardous. The guard in our earlier model (the check that decides whether a step may run) admitted steps inside it one at a time. In one run, a confiscation with no prior seizure committed first, and because confiscation is terminal, the waiting freeze could never become ready. Every step the guard admitted was safe for one move, and none of them was safe to continue from. The current rules keep the interval and define what everyone hears during it.
After the source emits the order, the asset is not frozen yet, and the stored mode is still Active on both sides. When the receiving side applies the order, the mode of every registered domain changes to Frozen together. From emission to publication, current reads return busy, meaning the value at this point cannot be answered yet. They neither repeat the old value nor get ahead of the new one. A request that relied on an observation from before the order fails with no effect.
We ran one signed force-inclusion FREEZE through this sequence, reopening the Rust endpoint at each stage. A separate Isabelle/HOL result starts from a valid regulatory state and rules out a frozen view and an active view of the same asset in two projections of one cut (a single point in the execution record) after a finality step.
The sentence we can honestly write got narrower. While an order is on its way, the protocol says it is on its way, and once applied, both sides give the same answer. An authority and a holder can rely on that sentence. Atomicity that includes external ledgers remains open.
The Machine Allowed What the Chain Forbids
When Regulatory Actions Do Not Commute mechanized the regulatory state machine and closed as theorems that confiscation is terminal and reachable from every non-terminal state [8]. OIP's Escalation Chain does not let confiscation happen from just anywhere. The order is FREEZE, SEIZE, CONFISCATE, and each step needs the record of the one before.
Side by side as documents, these did not look contradictory, because the proof spoke about combinations of state and the specification spoke about legal preconditions. Placed on the same execution, five transitions came apart.
Each is right about its own object. The public theorem needs no correction, and the product's behavior is a subset of the machine's. But a proved transition has not read the legal precondition. If a confiscation commits first through any of those shortcuts, it cannot be undone, so the gap matters.
The public lemma letting confiscation fire from any non-terminal state, selected
So we proved refusal anew at the product layer. Source emission and receiving commit each run the same legal check at their own current cut, and the normal, administrative, adapter and force-inclusion paths all pass through the same final check. A seizure has to point exactly at a completed freeze record, and RESTRICT cannot fill that slot. A refusal leaves state, balances, supply and the record unchanged, and it carries a distinct reason.
We built the tests in both directions. An implementation that refuses everything passes a safety test easily and blocks lawful enforcement, so we check that an ordinary spend after a freeze is refused and that lawful enforcement executes.
Reading the Deadline Instead of a Flag
In v0.5, a CONFISCATE met its precondition by carrying appealDeadlinePassed: true. The hash beside it, appealDeadlineRecord, exists for "allowing auditors to verify that the prerequisite condition was indeed satisfied at the time of execution," which is a check made afterward. The Error Reference even tells a retry scheduler to resend at the deadline with the flag set. At the moment of decision, the rule was reading a value the requester wrote.
The rule in development reads the deadline preserved in the active seizure record, along with a trusted time. A request that arrives with a shortened deadline no longer matches the record and is refused. This fits the clock section, because here the rule really is asking whether time has passed, so time is the right input. A clock becomes a stand-in when the question is about an outcome, and for this rule the stand-in was the flag.
The same work surfaced a disagreement between our documents. Regulatory Actions allowed RESTRICT on a reserved asset and the State Management transition matrix refused it. A proof cannot hold both. We chose to allow it and corrected the matrix in public [5].
When the Code Was Finer Than the Model
The usual picture has proofs correcting code. The moment we learned most from ran the other way. Refinement is the work of showing that runs of the code correspond to runs of the proved model, which carries the theorems down to the code, and seL4 is the classic of the genre [9]. We are connecting the main paths this way. Along the way, two valid installations with the same epoch, the same cut and the same request got different answers from our Rust code: one Reserved and one Rejected. The difference was a single Reserve grant.
In the model, those two installations were the same input. The model bundled permissions per caller and per transfer binding, so it could not express revoking only one of Reserve, Dispatch or Debit. One input with two outputs breaks the correspondence, and matching the session and epoch left the counterexample standing. The code was right and the model was coarse.
We widened the model to current permissions per command. The earlier theorems still hold for what that model can say. Until we set it against code, we had no way to see what it could not say.
A Revocation Has to Enter the Same Order
For a regulated asset, the moment an authority lost its power is a legal fact. If a permission is revoked while a write made under it is in flight, which came first? We asked that with a contrast test. When revocation, cancellation or a change of writer changed the authoritative value first (the current value that every write compares against), a late save relying on an old observation was refused, and the head of the record and the balances stayed as they were.
When revocation was left only as a separate external marker and the authoritative value stayed the same, the late save succeeded. We do not accept that configuration. In a mutated build with one comparison removed from the authoritative write, a debit confirmed after revocation.
We settled this by testing, and no incident lies behind it. The rule is short: revocation and the effect enter the same authoritative order, and recovery reads the exact evidence of that decision. The external marker had been a stand-in for the revocation.
What a Restore Takes Away
Connecting code raised a question documents never had: how can a record say it is the latest? Restore a signed journal from yesterday's backup and its signatures still verify. A journal can show that it is genuine and cannot show that it is the end. A review pointed out this gap and we filled it, with no reproduced incident behind it.
The repair is an independent witness on a different cluster and endpoint, with different trust and keys. Recovery reads the source journal first and the witness last, so restoring the source alone does not change what was already selected. In a real test, we restored the source to its old empty value. The opposite decision and two votes were held back, and the first payment receipt stayed, along with the balances.
The same question reaches regulatory events. In a Rust sequence that applied FREEZE, UNFREEZE and another FREEZE, we changed only the retained freeze pointer so it named the first event. The earlier implementation then emitted and applied a SEIZE on a freeze that had already been lifted. The current one replays applied events to rebuild regulatory modes and the freeze and seizure references, and it rejects the altered image at reopening and before publication. The replay checks the structure of transitions, with historical legal facts supplied separately.
Evidence moved as well. We had kept provenance evidence inside the state and written an invariant over it, and a proof broke that design sentence with a run that restored an older cache: the restore wiped the evidence along with the cache. We moved the evidence to events at positions in the execution record.
What These Cases Share
The table lines up the cases by what each rule leaned on.
| What the rule leaned on | What came out | What it reads now |
|---|---|---|
| A clock | Refund at expiry plus a late finality certificate pays twice | Finality certificate, or reversal or reorg evidence |
| A flag the requester wrote | The request itself declares the appeal deadline passed | Deadline in the seizure record, trusted time |
| An allowed state transition | Five shortcuts with no legal precondition | The exact record of the prior event |
| A revocation marker outside the authority | A late save passes after revocation | Revocation in the same order as the effect |
| Permissions bundled per caller (model) | Revoking one command cannot be expressed | Current permission per command |
| The source journal itself | Rewound, it gives no ground to refuse the opposite decision | Selection held by an independent witness |
| Evidence inside the state | An older cache restore wipes it | Events in the execution record |
| A retained freeze pointer | A seizure rests on a freeze already lifted | Replay of applied events |
Every entry in the left column is a value that is usually right. None of them stood out in review, and it took deliberately constructed runs to pull them apart from the event. What travels to another cross-chain protocol is the question behind the table: what does this rule read at the moment it decides? Who wrote that value, and is there a run where it differs from the event?
What Is Moving and What Is Still Open
Here is where OIP v0.6 development stands against our public Open Issues list. The items differ in size, so this should not be read as a completion rate.
| Status | Public open issues |
|---|---|
| Clear progress | Interoperability testing: Rust and Go implementations exchange real signed packets |
| Partial progress | Message size (negotiated limit, no fragmentation); time-skew defense (signed trusted time, no tolerance or isolation procedure); reconciliation (at the lock and settlement level); long-term storage (for recovery) |
| Still open | Canton (multi-Signatory, key rotation and bootstrap, Party–OCID invalidation); RWA Registry Solidity signatures; ERC-TRUST integration; inter-asset dependency; token standard extensions; Restricted DSL; network propagation; dynamic routing; CRITICAL authority; phase timeout governance; DLQ thresholds and automated analysis; Registry and Authority Registry integration; Driver slashing; slashing pattern detection; quantum-resistant signatures; evidence hash verification; error code extension process |
The longest row is the open one, and it holds what the checkpoint called "major work." Building the money and authority paths first meant the list did not shrink in the order we said it would. In return, those items now have a floor where rules, proofs and code already touch.
What This Does Not Establish
None of this is a result about OSS or D-quencer. The runs use a reference configuration on one host. Legal facts (jurisdiction, basis, the lawfulness of an order) are inputs, and we do not judge whether an order is lawful. We claim regulatory compliance for no deployment, and nothing here is legal advice.
The connection between code and model covers main paths. The compiler and cryptography are out of scope, and translating intermediate compiler output into the proof language was done by hand. Rolling back both stores at once, or stealing signing and witness credentials together, is outside our assumptions. Atomicity across external ledgers is open, and there has been no external review yet. Because the rules and reference code are private, readers cannot reproduce these events today, apart from the public lock proof.
Closing Thoughts
OIP v0.5 Checkpoint ended on "As explorers, the most interesting question is where to make room for the next discovery." Our answer is the joins where rules, proofs and code touch. Making that room cost more than we expected, and it moved the order of the work.
A regulatory order really does bind or move someone's asset. To hand that job to a protocol, we should be able to answer mathematically when and how far an order took effect. What we can answer today is a set of narrow sentences inside a reference configuration, and widening those sentences is what OIP v0.6 development is for.
We keep returning to a few questions. How far can the interval between issuing and enforcing shrink on real ledgers? What would a record have to look like for a regulator to accept it as evidence? And how much of a legal rule can a machine check without pretending to judge?
References
- [1] Oraclizer Research. (2026). OIP v0.5 Checkpoint: Three Discoveries and the Big Map. https://research.oraclizer.io/oip-v0-5-integration-review-notes/
- [2] Oraclizer. (2026). Preemptive Lock Correctness, Isabelle/HOL theories at a fixed commit. https://github.com/Oraclizer/formal-verification/tree/8e50307db638e8ba2ed949a54220142221796fbf/Preemptive_Lock_Correctness
- [3] Fischer, M. J., Lynch, N. A., & Paterson, M. S. (1985). Impossibility of Distributed Consensus with One Faulty Process. Journal of the ACM, 32(2). https://doi.org/10.1145/3149.214121
- [4] Andreakis, A. (2026). Machine-Checked Dual-Write Recovery from a Commit Log. arXiv:2608.00501. https://arxiv.org/abs/2608.00501
- [5] Oraclizer. (2026). OIP documentation: Changelog. https://docs.oraclizer.io/changelog/
- [6] Merigoux, D., Chataing, N., & Protzenko, J. (2021). Catala: A Programming Language for the Law. Proceedings of the ACM on Programming Languages, 5(ICFP). https://doi.org/10.1145/3473582
- [7] Passmore, G. O., & Ignatovich, D. (2017). Formal Verification of Financial Algorithms. CADE 2017, LNCS 10395. https://doi.org/10.1007/978-3-319-63046-5_3
- [8] Oraclizer Research. (2026). When Regulatory Actions Do Not Commute: Order, Outcome, and Sixty Normal Forms. https://research.oraclizer.io/regulatory-action-composition-isabelle/
- [9] Klein, G., Elphinstone, K., Heiser, G., et al. (2009). seL4: Formal Verification of an OS Kernel. SOSP 2009. https://doi.org/10.1145/1629575.1629596