Jay Kim, CPTO of Oraclizer (publishing under his legal name Jinwook Kim), has been listed as a co-author on three papers from the Observer Patch Holography (OPH) research program, under the affiliation Oraclizer Labs. The work behind the listing is formal verification carried out in the program’s own theorem prover. All three papers are publicly available.
- Finite Observer Consensus as a Reconstruction Principle
- Observation-Determined Normal Forms: Stability, Obstructions, and Refinement in Constraint and Rewrite Systems
- Reality as a Consensus Protocol: The Fixed-Point Computation That Implements Physics
Where Observer Patch Holography Meets a Problem We Already Had
Observer Patch Holography is an open research program built on a single premise: observers are primary, and objective reality is emergent. Rather than assuming spacetime and fields, it begins with finite systems that hold local state, read only part of what their neighbors hold, and repair the disagreements between them, then asks how much physical structure can be reconstructed from there. The program is led by Bernhard Mueller, who wrote Mythril, the symbolic-execution security analyzer for EVM bytecode, authored and formerly led the OWASP Mobile Application Security Testing Guide, and now serves as AI Research Lead at the smart contract auditing platform Sherlock.
We joined because the central question is shaped like ours. Observer Patch Holography asks whether the disagreements among participants who each observe only a fragment can be repaired into one shared state. Oraclizer asks whether two domains that move independently, on-chain and off-chain, can be held to a single consistent state. The domain differs, a physical model on one side and a regulated asset on the other, but the question is the same: how far can a divergent state be brought back, and what stands in the way. Our Cross-Domain State Preservation Functor, proved in Isabelle/HOL, answered a question from that same family.
Separating the Four Ways Repair Fails
The Observer Patch Holography repository runs on Lean 4. Our own formal verification is written in Isabelle/HOL, so this work meant designing and proving the theorems in Lean from scratch rather than porting existing proofs across.
What we proved is a separation of the four ways repair fails. When a state must be preserved, there is more than one reason it may not be reached. The state may not exist at all; it may exist but stay unreachable from any starting point; it may be reachable without being reached with certainty; or it may be reached while the endpoint remains ambiguous. Under machine checking we closed that these four layers are mutually disjoint and jointly exhaustive, that each layer is inhabited by a concrete case and a countermodel, and that the separation survives transport to another model. Alongside the proofs we contributed a deterministic checker that enumerates finite models exhaustively, so a deliberately broken variant does not pass.
The same distinction carries over to Oraclizer. A regulatory freeze that reaches one domain but not the other, and a freeze that reaches both while the final states diverge, have different causes and call for different responses.
What Carries Back to Our Own Work
The collaboration settled something we could not have settled alone. The verification discipline we built for regulated assets transfers. The same way of asking a question, what must hold, under which assumptions, and what would break it, produced a usable result in a domain with no tokens and no ledgers in it. An internal review cannot establish that. A maintainer applying their own standards on their own repository can.
So the standard carries in both directions. What held up in someone else’s repository is the standard we hold our own system to, and every result Oraclizer stands behind stays where anyone can rebuild it. Our formal verification is public at github.com/Oraclizer/formal-verification, and the Observer Patch Holography repository, where these papers and the Lean sources both live, is at github.com/FloatingPragma/observer-patch-holography.
