Skip to content
@Oraclizer

Oraclizer

Formal, protocol, and proving foundations for cross-domain state synchronization.
Oraclizer

Formal, protocol, and proving foundations for cross-domain state synchronization

Oraclizer is building an oracle state machine that coordinates on-chain and off-chain state transitions under explicit protocol, verification, and regulatory boundaries.

Website · Research · Documentation · Formal artifacts · X

System map · Repositories · Standards · Publications · Review

Important

Oraclizer's public GitHub provides research, formal artifacts, and protocol specifications. Each repository defines its exact assurance boundary.

Why state synchronization

Observation-oriented oracle designs move facts into a chain. Stateful assets also require coordinated changes to ownership, restrictions, contractual terms, and external records. Independent updates can leave participating domains with different views of the same asset.

Oraclizer treats this as a state-machine problem. The target architecture defines the required coupling between domains, binds related transitions, verifies the transition against explicit rules, and records a result that can be inspected and challenged. The work spans protocol specification, regulatory semantics, mechanized models, and proving infrastructure.

System and research map

Oraclizer system and research map showing on-chain and off-chain systems connected through the OIP and OSS target architecture, with regulatory semantics and assurance layers

The diagram is a project map, not a deployment diagram. Its status labels are part of the architecture: public research, published specifications, active development, and private candidates are intentionally distinguished.

Assurance chain

Mechanized Isabelle/HOL models feed bounded bridges that carry evidence today, and those bridges pin named implementations; a dashed band states the target of full core refinement from models to runtime, distinguished from the bounded evidence that exists now

The chain reads left to right: machine-checked models, the bounded bridges that carry evidence today, and the pinned implementations they are meant to land on. The dashed band is the target, full core refinement from models to runtime, closed stepwise and published with its evidence; it is a goal statement, not a current claim.

Repository portfolio

Public now

Repository Scope Current status
formal-verification Machine-checked, model-level foundations for cross-domain state preservation and regulatory action composition in Isabelle/HOL, plus an independent protected-behavior obstruction companion Public, production-maintained research. Reproducible sessions, integrity manifests, explicit assumptions, security reporting, contribution rules, governance, and citation metadata. It is not a production implementation or deployment.
erc-trust ERC-TRUST, Typed Regulatory Uniformity for Security Tokens: typed, fail-closed regulatory actions and recomputable receipts for security tokens, with the proposed ERC text, a reference implementation, an SDK, and machine-checked verification evidence Public pre-ERC candidate. Tagged candidate snapshots, reproducible verification evidence, structured issue forms, security reporting, and citation metadata, with the companion paper at arXiv:2608.29134. Unaudited and not for production.

Preparing for public release

The repositories below remain private today. These entries announce intended future publication. They do not announce availability, a delivery date, audit status, or production readiness, and no private repository link is exposed.

Repository Scope Publication boundary
StateSync-GKR A Rust prover for sparse-Merkle state transitions built on Plonky3 primitives, with GKR and sumcheck mechanized in Isabelle/HOL Private development repository. Public release is planned after internal review.

Public visibility will be evaluated independently from a version tag, release, deployment, audit, or standards-process milestone.

Protocols and standards

Work Role Public state
OIP v0.5 Oracle Interoperability Protocol: message semantics, state transitions, routing, validation, errors, and conformance rules for state-machine implementations Published specification, prototype stage. OIP is a specification; OSS is its reference implementation track.
RCP Regulatory Compliance Protocol: a regulatory benchmark derived from 31 requirements across 15 global financial regulators Published research framework. RCP organizes the requirements into five principles and defines a shared regulatory-action vocabulary.
ERC-8319 Standards Track ERC proposal for the RCP vocabulary and legal-effect semantics Open proposal under editor review. The proposal is not merged and its status is separate from Oraclizer product development.
ERC-TRUST A thin candidate extension connecting ERC-8319 semantics to typed execution, authorization, outcomes, and receipts Public pre-ERC candidate. The proposed text, reference implementation, and verification evidence are public. It has not been submitted as an ERC, and the official submission follows ERC-8319.

Published research

Regulatory Compliance Protocol

Jinwook Kim and Jonghun Hong. A Regulatory Compliance Protocol for Asset Interoperability Between Traditional and Decentralized Finance in Tokenized Capital Markets.

arXiv:2603.29278 · SSRN:6538718

The paper presents RCP as a value-neutral benchmark for identifying which regulatory requirements token standards cover, which they leave open, and where supporting off-chain infrastructure remains necessary.

Cross-Domain State Preservation

Jinwook Kim. The Cross-Domain State Preservation Functor: A Mechanized Theory of Regulatory State Synchronization in Isabelle/HOL.

arXiv:2604.03844 · SSRN:6550359 · Mechanized artifacts

The paper and repository provide mechanized, model-level results under stated definitions and assumptions. They do not establish adversarial network liveness, implementation refinement, deployed-system correctness, or audit status.

Mechanizing Typed Regulatory Actions

Jinwook Kim. Mechanizing Typed Regulatory Actions for Security Tokens: Semantics, Falsification, and Bounded EVM Evidence.

arXiv:2608.29134 · Artifact repository

The paper mechanizes execution semantics for typed regulatory actions on security tokens in Isabelle/HOL, keeps applied, refused, and failed outcomes apart, and proves an observational limit of the contract-level model. For one implementation candidate it reports bounded, tool-by-tool evidence with the reach of each result stated separately. It does not establish audit status, production readiness, or deployed-system correctness.

More protocol, proof, RWA, and economic research is indexed at research.oraclizer.io.

Review and contact

Independent reproduction, counterexamples, assumption challenges, and scope corrections are especially useful.

General and research inquiries: jay@oraclizer.io

Pinned Loading

  1. formal-verification formal-verification Public

    Three-session Isabelle/HOL artifact: cross-domain state preservation, regulatory action composition, and protected-behavior obstructions

    Isabelle

Repositories

Showing 3 of 3 repositories

People

This organization has no public members. You must be a member to see who’s a part of this organization.

Top languages

Loading…

Most used topics

Loading…