diff --git a/profile/README.md b/profile/README.md
index f18a392..5e9bfac 100644
--- a/profile/README.md
+++ b/profile/README.md
@@ -16,6 +16,7 @@ regulatory boundaries.
[**Research**](https://research.oraclizer.io) ·
[**Documentation**](https://docs.oraclizer.io) ·
[**Formal artifacts**](https://github.com/Oraclizer/formal-verification) ·
+[**Prover**](https://github.com/Oraclizer/statesync-gkr) ·
[**X**](https://x.com/Oraclizer)
[System map](#system-and-research-map) ·
@@ -27,8 +28,9 @@ regulatory boundaries.
> [!IMPORTANT]
-> Oraclizer's public GitHub provides research, formal artifacts, and protocol
-> specifications. Each repository defines its exact assurance boundary.
+> Oraclizer's public GitHub provides research, formal artifacts, protocol
+> specifications, and source-available software. Each repository defines its
+> exact assurance boundary.
## Why state synchronization
@@ -53,8 +55,8 @@ 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, active
-development, and private candidates are intentionally distinguished.
+part of the architecture: public research, published specifications, and
+active development are intentionally distinguished.
## Assurance chain
@@ -79,19 +81,7 @@ statement, not a current claim.
| --- | --- | --- |
| [**formal-verification**](https://github.com/Oraclizer/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**](https://github.com/Oraclizer/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](https://arxiv.org/abs/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.
+| [**statesync-gkr**](https://github.com/Oraclizer/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](https://arxiv.org/abs/2610.05335). Research and other non-production use are free; production proving requires a commercial license. |
## Protocols and standards
@@ -146,6 +136,23 @@ 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.
+### StateSync-GKR
+
+**Jinwook Kim.** *StateSync-GKR: Machine-Checking the Trust Chain from
+Sparse-Merkle State Transitions to GKR Verification.*
+
+[arXiv:2610.05335](https://arxiv.org/abs/2610.05335) ·
+[Software DOI](https://doi.org/10.5281/zenodo.23280552) ·
+[Repository](https://github.com/Oraclizer/statesync-gkr)
+
+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](https://research.oraclizer.io).
@@ -156,6 +163,7 @@ corrections are especially useful.
- Start with the [formal artifact catalog](https://github.com/Oraclizer/formal-verification#formal-artifact-catalog) and its [assurance boundary](https://github.com/Oraclizer/formal-verification#assurance-boundary).
- Review the [ERC-TRUST candidate repository](https://github.com/Oraclizer/erc-trust) for typed regulatory-action execution, its evidence package, and its issue forms.
+- Review the [StateSync-GKR repository](https://github.com/Oraclizer/statesync-gkr) for the prover, its [formal-verification guide](https://github.com/Oraclizer/statesync-gkr/blob/main/FORMAL_VERIFICATION.md), 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](https://github.com/Oraclizer/formal-verification/security/policy), never through a public issue.
- Read the [OIP v0.5 specification](https://docs.oraclizer.io/oip-v05/oip-overview/) for protocol semantics and conformance scope.
diff --git a/profile/assets/oraclizer-social-preview.png b/profile/assets/oraclizer-social-preview.png
index 309fca7..e660e37 100644
Binary files a/profile/assets/oraclizer-social-preview.png and b/profile/assets/oraclizer-social-preview.png differ
diff --git a/profile/assets/oraclizer-social-preview.svg b/profile/assets/oraclizer-social-preview.svg
index a1b7d78..962b8f4 100644
--- a/profile/assets/oraclizer-social-preview.svg
+++ b/profile/assets/oraclizer-social-preview.svg
@@ -40,7 +40,7 @@
PROVING
- StateSync-GKR in development
+ StateSync-GKR
ORACLIZER.IO
diff --git a/profile/assets/oraclizer-system-map-mobile.svg b/profile/assets/oraclizer-system-map-mobile.svg
index 066bb91..bd5c2d8 100644
--- a/profile/assets/oraclizer-system-map-mobile.svg
+++ b/profile/assets/oraclizer-system-map-mobile.svg
@@ -66,8 +66,8 @@
PUBLIC
StateSync-GKR
- Private prover stack · public release planned
- PRIVATE
+ Source-available Rust prover · BSL 1.1
+ PUBLIC
diff --git a/profile/assets/oraclizer-system-map.svg b/profile/assets/oraclizer-system-map.svg
index 8bc01ea..e003885 100644
--- a/profile/assets/oraclizer-system-map.svg
+++ b/profile/assets/oraclizer-system-map.svg
@@ -87,7 +87,7 @@
ERC-TRUST
- Public pre-ERC candidate · unaudited, not for production
+ Pre-ERC candidate · unaudited, not for production
PUBLIC
@@ -103,9 +103,9 @@
StateSync-GKR
- Private prover stack · public release planned
-
- PRIVATE
+ Source-available Rust prover · BSL 1.1
+
+ PUBLIC
diff --git a/scripts/verify-profile.mjs b/scripts/verify-profile.mjs
index 906a536..2a9c16a 100644
--- a/scripts/verify-profile.mjs
+++ b/scripts/verify-profile.mjs
@@ -53,7 +53,7 @@ const requiredProfileText = [
"Formal, protocol, and proving foundations for cross-domain state synchronization",
"System and research map",
"Repository portfolio",
- "Preparing for public release",
+ "Public now",
"Protocols and standards",
"Published research",
"Review and contact",
@@ -70,7 +70,6 @@ const forbiddenPatterns = [
[/The first oracle/i, "unverifiable first claim"],
[/complete state/i, "overbroad complete-state claim"],
[/safety and liveness under Byzantine faults/i, "unsupported Byzantine liveness claim"],
- [/github\.com\/Oraclizer\/statesync-gkr/i, "private repository link"],
[/[A-Za-z]:\\Users\\/i, "machine-local Windows path"],
];