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 · Prover · X
System map · Repositories · Standards · Publications · Review
Important
Oraclizer's public GitHub provides research, formal artifacts, protocol specifications, and source-available software. Each repository defines its exact assurance boundary.
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.
The diagram is a project map, not a deployment diagram. Its status labels are part of the architecture: public research, published specifications, and active development are intentionally distinguished.
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 | 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. |
| statesync-gkr | StateSync-GKR: a Rust GKR and sumcheck engine for sparse-Merkle state transitions, with its circuit compiler and its GKR and sumcheck protocol modeled and machine-checked in Isabelle/HOL, and a conditional forward theorem relating the model to the verifier's acceptance checks | Public, source-available under the Business Source License 1.1 (v1.1.1). Signed immutable release, reproducible source checks, a software DOI, and the companion paper at arXiv:2610.05335. Research and other non-production use are free; production proving requires a commercial license. |
| 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. |
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.
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.
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.
Jinwook Kim. StateSync-GKR: Machine-Checking the Trust Chain from Sparse-Merkle State Transitions to GKR Verification.
arXiv:2610.05335 · Software DOI · Repository
The paper machine-checks, in Isabelle/HOL, the sparse-Merkle semantics, a model of the circuit compiler, the GKR and sumcheck reduction, and their composition, including the exact degree-four KoalaBear extension field that the implementation uses. A conditional forward acceptance theorem and recorded proofs for selected Rust contracts relate the model to the shipped verifier. The exact statements and premises are documented in the repository's formal-verification guide.
More protocol, proof, RWA, and economic research is indexed at research.oraclizer.io.
Independent reproduction, counterexamples, assumption challenges, and scope corrections are especially useful.
- Start with the formal artifact catalog and its assurance boundary.
- Review the ERC-TRUST candidate repository for typed regulatory-action execution, its evidence package, and its issue forms.
- Review the StateSync-GKR repository for the prover, its formal-verification guide, and its reproduction steps.
- Use the repository's structured issue forms for public proof or documentation questions.
- Report sensitive vulnerabilities through the relevant repository's security policy, never through a public issue.
- Read the OIP v0.5 specification for protocol semantics and conformance scope.
- Join the public standards discussion for ERC-8319.
General and research inquiries: jay@oraclizer.io