Oraclizer’s cross-domain state preservation proofs are now public, and anyone can verify them. We have proved the Cross-Domain State Preservation Functor: in plain terms, that when a regulated asset’s state changes in one place, it stays consistent everywhere the asset lives, across public blockchains, enterprise ledgers such as Canton/DAML, and off-chain systems. We released the entire proof, so it is not something to take on trust; it is something anyone can check.
This addresses one of the hardest blockers to bringing real-world assets fully on-chain. Institutions hesitate because they cannot be certain that a regulatory action, a freeze or a seizure, will hold consistently across every system an asset touches. We have now closed that question with a proof rather than a promise: a machine has checked, step by step, that the guarantee cannot break within the model’s stated assumptions. In a field where “trust us, it works” is the norm, an openly verifiable mathematical proof is a different order of assurance.
The work is substantial: a body of four interlocking theorems, about 6,720 lines, machine-checked in Isabelle/HOL with no gaps and no shortcuts. It is also a genuine contribution to the formal-verification field, carrying a Canton/DAML verification result into the on-chain world, and it is headed for peer-reviewed academic publication. The full corpus is open source under the BSD-3-Clause license.
Anyone can build the repository in Isabelle and confirm the cross-domain state preservation proofs hold. GitHub: github.com/Oraclizer/formal-verification (commit f56ec12). To put the status precisely: the proofs are complete, public, and machine-checkable; their formal archive registration is still pending.
For Oraclizer this is foundational. The same proof is the safety specification our core is built against, which means the system we ship can be held to a standard that is mathematically defined rather than merely asserted. A fuller account of what this guarantees, for the product, for institutions, and for the field, will follow in our research series. Just as we shared the journey of building these proofs openly, we will keep doing so. More at the next milestone.
