Dev

.bestpractices.json

@@ -1,24 +1,24 @@
 {
   "name": "Reproducible Agentic Environments System",
   "description": "RAES describes and validates authored agentic-environment scenarios, with published contracts, examples, conformance checks, and a Python reference implementation.",
-  "homepage_url": "https://raesystem.github.io/rae/",
-  "repo_url": "https://github.com/RAESystem/rae",
+  "homepage_url": "https://openrae.github.io/rae/",
+  "repo_url": "https://github.com/OpenRAE/rae",
   "license": "MIT",
   "implementation_languages": "Python",
   "description_good_status": "Met",
-  "description_good_justification": "The README states the purpose, scope, first successful task, and current limits: https://github.com/RAESystem/rae#readme.",
+  "description_good_justification": "The README states the purpose, scope, first successful task, and current limits: https://github.com/OpenRAE/rae#readme.",
   "interact_status": "Met",
-  "interact_justification": "Public GitHub issues and pull requests support URL-addressable discussion: https://github.com/RAESystem/rae/issues.",
+  "interact_justification": "Public GitHub issues and pull requests support URL-addressable discussion: https://github.com/OpenRAE/rae/issues.",
   "contribution_status": "Met",
-  "contribution_justification": "Contribution setup and pull-request steps are in https://github.com/RAESystem/rae/blob/main/CONTRIBUTING.md.",
+  "contribution_justification": "Contribution setup and pull-request steps are in https://github.com/OpenRAE/rae/blob/main/CONTRIBUTING.md.",
   "contribution_requirements_status": "Met",
   "contribution_requirements_justification": "CONTRIBUTING.md documents the dev branch, tests, docs rules, and Conventional Commit pull-request titles.",
   "floss_license_status": "Met",
   "floss_license_justification": "RAES uses the MIT License.",
   "floss_license_osi_status": "Met",
   "floss_license_osi_justification": "MIT is an OSI-approved open source license.",
   "license_location_status": "Met",
-  "license_location_justification": "The license is at https://github.com/RAESystem/rae/blob/main/LICENSE.",
+  "license_location_justification": "The license is at https://github.com/OpenRAE/rae/blob/main/LICENSE.",
   "documentation_basics_status": "Met",
   "documentation_basics_justification": "The README and docs/public provide installation, a tested quickstart, concepts, task guides, research context, and limits.",
   "documentation_interface_status": "Met",
@@ -32,7 +32,7 @@
   "maintained_status": "Met",
   "maintained_justification": "The public repository has current commits, releases, issues, and pull requests.",
   "repo_public_status": "Met",
-  "repo_public_justification": "The source repository is public at https://github.com/RAESystem/rae.",
+  "repo_public_justification": "The source repository is public at https://github.com/OpenRAE/rae.",
   "repo_track_status": "Met",
   "repo_track_justification": "The project uses Git and preserves public history on GitHub.",
   "repo_interim_status": "Met",
@@ -60,9 +60,9 @@
   "continuous_integration_status": "Met",
   "continuous_integration_justification": "GitHub Actions runs repository policy, tests, docs, security, and conformance checks.",
   "code_of_conduct_status": "Met",
-  "code_of_conduct_justification": "The project policy is at https://github.com/RAESystem/rae/blob/main/CODE_OF_CONDUCT.md.",
+  "code_of_conduct_justification": "The project policy is at https://github.com/OpenRAE/rae/blob/main/CODE_OF_CONDUCT.md.",
   "governance_status": "Met",
-  "governance_justification": "The maintainer-led decision and release model is at https://github.com/RAESystem/rae/blob/main/GOVERNANCE.md.",
+  "governance_justification": "The maintainer-led decision and release model is at https://github.com/OpenRAE/rae/blob/main/GOVERNANCE.md.",
   "bus_factor_status": "Unmet",
   "bus_factor_justification": "RAES currently has one maintainer, so its bus factor is below two.",
   "two_person_review_status": "Unmet",

.github/ISSUE_TEMPLATE/config.yml

@@ -1,8 +1,8 @@
 blank_issues_enabled: false
 contact_links:
   - name: Security report
-    url: https://github.com/RAESystem/rae/security/advisories/new
+    url: https://github.com/OpenRAE/rae/security/advisories/new
     about: Report a suspected vulnerability privately.
   - name: Support guide
-    url: https://github.com/RAESystem/rae/blob/main/SUPPORT.md
+    url: https://github.com/OpenRAE/rae/blob/main/SUPPORT.md
     about: Choose the right route and include a small example.

.github/workflows/ci.yml

@@ -18,7 +18,10 @@ permissions:
 
 jobs:
   verify:
-    runs-on: ubuntu-latest
+    # Ubuntu 24.04 restricts unprivileged user namespaces through AppArmor.
+    # Keep the proof-bearing job on 22.04 so Bubblewrap enforces the sandbox
+    # without disabling a host security control on the runner.
+    runs-on: ubuntu-22.04
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
         with:
@@ -28,6 +31,19 @@ jobs:
           python-version: "3.12"
       - name: Install uv
         uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v8
+      - name: Restore pinned Isabelle archive
+        uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
+        with:
+          path: .cache/raes-sdl/tooling/archives/Isabelle2025-2_linux.tar.gz
+          key: isabelle-linux-x86-64-2025-2-a20a507bc7c1270d
+      - name: Install proof sandbox
+        run: |
+          if ! command -v bwrap >/dev/null 2>&1; then
+            sudo apt-get update
+            sudo apt-get install --no-install-recommends -y bubblewrap
+          fi
+      - name: Acquire pinned Isabelle distribution
+        run: uv run --project implementations/python --frozen python -m tools.isabelle_tool acquire
       - name: Resolve policy base revision
         id: base
         run: |

.github/workflows/docs.yml

@@ -30,7 +30,9 @@ jobs:
       - name: Install uv
         uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v8
       - name: Validate and build public docs
-        run: uv tool run --from 'nox[uv]==2026.4.10' nox -f noxfile.py -s docs
+        run: uv tool run --from 'nox[uv]==2026.4.10' nox -f noxfile.py -s docs-local
+      - name: Check external documentation links
+        run: uv tool run --from 'nox[uv]==2026.4.10' nox -f noxfile.py -s docs-links
       - name: Upload Pages artifact
         if: github.ref == 'refs/heads/main'
         uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v5.0.0

.ground-control.yaml

@@ -1,13 +1,13 @@
 schema_version: 1
 project: aces-sdl
-github_repo: RAESystem/rae
+github_repo: OpenRAE/rae
 workflow:
   test_command: RAES_REQUIREMENT_UID="${RAES_REQUIREMENT_UID:-$(printenv A""CES_REQUIREMENT_UID)}" uv tool run --from 'nox[uv]==2026.4.10' nox -f noxfile.py -s verify
-  completion_command: RAES_REQUIREMENT_UID="${RAES_REQUIREMENT_UID:-$(printenv A""CES_REQUIREMENT_UID)}" uv tool run --from 'nox[uv]==2026.4.10' nox -f noxfile.py -s verify
+  completion_command: RAES_REQUIREMENT_UID="${RAES_REQUIREMENT_UID:-$(printenv A""CES_REQUIREMENT_UID)}" uv tool run --from 'nox[uv]==2026.4.10' nox -f noxfile.py -s verify-completion
   lint_command: uv tool run --from 'nox[uv]==2026.4.10' nox -f noxfile.py -s lint
   format_command: uv tool run --from 'nox[uv]==2026.4.10' nox -f noxfile.py -s hygiene
   policy_command: RAES_REQUIREMENT_UID="${RAES_REQUIREMENT_UID:-$(printenv A""CES_REQUIREMENT_UID)}" make policy
-  precommit_command: RAES_REQUIREMENT_UID="${RAES_REQUIREMENT_UID:-$(printenv A""CES_REQUIREMENT_UID)}" pre-commit run --all-files
+  precommit_command: RAES_REQUIREMENT_UID="${RAES_REQUIREMENT_UID:-$(printenv A""CES_REQUIREMENT_UID)}" pre-commit run
   codex_review:
     pre_push_cap: 1
   test_quality_review:

.mcp.json

@@ -6,7 +6,7 @@
       "args": ["/home/atomik/src/Ground-Control/mcp/ground-control/index.js"],
       "env": {
         "GC_BASE_URL": "http://red-dragon:8000",
-        "GH_REPO": "RAESystem/rae"
+        "GH_REPO": "OpenRAE/rae"
       }
     },
     "sonarqube": {

CONTRIBUTING.md

@@ -26,7 +26,7 @@ Prerequisites:
 Install the locked Python environment:
 
 ```shell
-git clone https://github.com/RAESystem/rae.git
+git clone https://github.com/OpenRAE/rae.git
 cd rae
 uv sync --project implementations/python --all-extras --frozen
 ```

README.md

@@ -1,10 +1,10 @@
 # Reproducible Agentic Environments System
 
-[![CI](https://github.com/RAESystem/rae/actions/workflows/ci.yml/badge.svg?branch=main)](https://github.com/RAESystem/rae/actions/workflows/ci.yml)
-[![Docs](https://github.com/RAESystem/rae/actions/workflows/docs.yml/badge.svg?branch=main)](https://raesystem.github.io/rae/)
+[![CI](https://github.com/OpenRAE/rae/actions/workflows/ci.yml/badge.svg?branch=main)](https://github.com/OpenRAE/rae/actions/workflows/ci.yml)
+[![Docs](https://github.com/OpenRAE/rae/actions/workflows/docs.yml/badge.svg?branch=main)](https://openrae.github.io/rae/)
 [![PyPI](https://img.shields.io/pypi/v/raes.svg)](https://pypi.org/project/raes/)
 [![Python](https://img.shields.io/pypi/pyversions/raes.svg)](https://pypi.org/project/raes/)
-[![License: MIT](https://img.shields.io/badge/License-MIT-blue.svg)](https://github.com/RAESystem/rae/blob/main/LICENSE)
+[![License: MIT](https://img.shields.io/badge/License-MIT-blue.svg)](https://github.com/OpenRAE/rae/blob/main/LICENSE)
 
 RAES, the Reproducible Agentic Environments System, helps you describe and
 check an agentic environment. RAES SDL is its YAML language for authored
@@ -74,29 +74,29 @@ Validated first-scenario with 2 nodes.
 
 RAES has checked the file shape and current semantic rules. It has not created
 infrastructure. Continue with the
-[quickstart](https://raesystem.github.io/rae/quickstart.html) to learn what
+[quickstart](https://openrae.github.io/rae/quickstart.html) to learn what
 each part means.
 
 ## Choose your route
 
 - **Scenario authors:** Start with the
-  [SDL guide](https://raesystem.github.io/rae/sdl/) and
-  [worked examples](https://github.com/RAESystem/rae/tree/main/examples/scenarios).
+  [SDL guide](https://openrae.github.io/rae/sdl/) and
+  [worked examples](https://github.com/OpenRAE/rae/tree/main/examples/scenarios).
 - **Python users:** Use the
-  [Python guide](https://raesystem.github.io/rae/guides/python.html) and
-  [API reference](https://raesystem.github.io/rae/api/).
+  [Python guide](https://openrae.github.io/rae/guides/python.html) and
+  [API reference](https://openrae.github.io/rae/api/).
 - **CLI users:** See the
-  [command-line guide](https://raesystem.github.io/rae/guides/cli.html).
+  [command-line guide](https://openrae.github.io/rae/guides/cli.html).
 - **Backend implementers:** Read the
-  [backend and conformance guide](https://raesystem.github.io/rae/backends.html).
+  [backend and conformance guide](https://openrae.github.io/rae/backends.html).
 - **Researchers:** Review the
-  [research context](https://raesystem.github.io/rae/research.html),
-  [current limits](https://raesystem.github.io/rae/limitations.html), and
-  [citation guide](https://raesystem.github.io/rae/citation.html).
+  [research context](https://openrae.github.io/rae/research.html),
+  [current limits](https://openrae.github.io/rae/limitations.html), and
+  [citation guide](https://openrae.github.io/rae/citation.html).
 - **Contributors:** Follow
-  [CONTRIBUTING.md](https://github.com/RAESystem/rae/blob/main/CONTRIBUTING.md)
+  [CONTRIBUTING.md](https://github.com/OpenRAE/rae/blob/main/CONTRIBUTING.md)
   and the
-  [developer documentation index](https://github.com/RAESystem/rae/blob/main/docs/README.md).
+  [developer documentation index](https://github.com/OpenRAE/rae/blob/main/docs/README.md).
 
 ## Understand what RAES promises
 
@@ -111,7 +111,7 @@ validity, or reproducibility.
 The repository does not include a production deployment backend or a managed
 environment service. It includes contracts, stubs, examples, conformance
 checks, and reference code. Read the
-[current limits](https://raesystem.github.io/rae/limitations.html) before
+[current limits](https://openrae.github.io/rae/limitations.html) before
 choosing it for a study or integration.
 
 ## See where RAES fits
@@ -136,7 +136,7 @@ The core model is not limited to those areas.
 Install the locked development environment:
 
 ```console
-git clone https://github.com/RAESystem/rae.git
+git clone https://github.com/OpenRAE/rae.git
 cd rae
 uv sync --project implementations/python --all-extras --frozen
 uv run --project implementations/python raes --help
@@ -165,8 +165,8 @@ reviewer for every change.
 
 Release Please owns package versions, GitHub releases, and `CHANGELOG.md`.
 Published schemas carry separate stability labels. See
-[GOVERNANCE.md](https://github.com/RAESystem/rae/blob/main/GOVERNANCE.md) and
-[MAINTAINERS.md](https://github.com/RAESystem/rae/blob/main/MAINTAINERS.md) for
+[GOVERNANCE.md](https://github.com/OpenRAE/rae/blob/main/GOVERNANCE.md) and
+[MAINTAINERS.md](https://github.com/OpenRAE/rae/blob/main/MAINTAINERS.md) for
 the current decision and maintenance model.
 
 ## Cite RAES
@@ -177,11 +177,11 @@ the current decision and maintenance model.
   title   = {RAES: Reproducible Agentic Environments System},
   year    = {2026},
   license = {MIT},
-  url     = {https://github.com/RAESystem/rae}
+  url     = {https://github.com/OpenRAE/rae}
 }
 ```
 
 RAES is released under the
-[MIT License](https://github.com/RAESystem/rae/blob/main/LICENSE). Third-party
+[MIT License](https://github.com/OpenRAE/rae/blob/main/LICENSE). Third-party
 notices are in
-[THIRD_PARTY_NOTICES.md](https://github.com/RAESystem/rae/blob/main/THIRD_PARTY_NOTICES.md).
+[THIRD_PARTY_NOTICES.md](https://github.com/OpenRAE/rae/blob/main/THIRD_PARTY_NOTICES.md).

contracts/concept-authority/behavioral-relations-v1.json

@@ -1,7 +1,7 @@
 {
   "schema_version": "behavioral-relations/v1",
   "taxonomy_id": "raes-behavioral-relations",
-  "taxonomy_revision": "rev8",
+  "taxonomy_revision": "rev9",
   "bibliography": [
     {
       "source_id": "park-1981",
@@ -2000,13 +2000,15 @@
         "implementations/python/tests/test_issue_961_participant_opacity.py covers profile and claim resolution, finite bounds, active strategies, coalition fusion, decision and omission channels, retained release knowledge, vacuity, deterministic evidence, replay, and explicit nonclaims.",
         "The participant-opacity finite-state checker derives the complete reachable fixed point from an exact transition model, checks every reachable secret evaluation point, and binds catalog, profile, model, assumptions, explored coverage, tool version, result or safe counterexample, and replay evidence.",
         "The committed model-check input and evidence fixtures retain the exact positive baseline model, result, digests, complete coverage, tool identity, and explicit nonclaims; invalid fixtures exercise count and partial-result promotion failures.",
-        "implementations/python/tests/test_issue_962_participant_opacity_model_check.py covers pair-probe incompleteness, supervisor behavior, active strategies, coalition fusion, retained memory, release changes, order and probability non-promotion, exact bounds, replay, and agreement with the bounded lane."
+        "implementations/python/tests/test_issue_962_participant_opacity_model_check.py covers pair-probe incompleteness, supervisor behavior, active strategies, coalition fusion, retained memory, release changes, order and probability non-promotion, exact bounds, replay, and agreement with the bounded lane.",
+        "The Isabelle/HOL Participant_Opacity session kernel-checks the SEM-231 one-sided opacity definition, its information-cell knowledge characterization, and the conditional implication from a matching SEM-230 noninterference instance for an eligible predicate; checked countermodels preserve the invalid-promotion boundaries."
       ],
       "explicit_non_claims": [
         "Relation definition, catalog validation, claim-profile binding, and bounded finite analysis do not establish opacity of RAES, RUN-319, or any backend outside the exact admitted artifact.",
         "No checker, finite-state model check, mathematical proof, runtime enforcement, supervisor synthesis, backend declaration, backend realization, or backend conformance is delivered by taxonomy revision rev5.",
         "Taxonomy revision rev7 adds only an in-process bounded-test checker; it does not add a model check, mathematical proof, runtime enforcement, supervisor synthesis, backend declaration, backend realization, or backend conformance.",
         "Taxonomy revision rev8 adds one exact finite-state model-check result; it does not add a mathematical proof, runtime enforcement, supervisor synthesis, backend declaration, backend realization, or backend conformance.",
+        "Taxonomy revision rev9 adds only the abstract conditional mathematical theorem bound to participant-opacity-theorem-v1; it does not prove opacity of RAES, a runtime, a deployment, a backend, or the finite fixture profile.",
         "Bounded evidence authenticates only the normalized-input digest; it does not authenticate a claimed source artifact or materializer.",
         "Opacity of one predicate does not imply SEM-230 policy noninterference, projected-history equivalence, epistemic indistinguishability of two selected worlds, trace inclusion or equivalence, simulation, refinement, or strong or weak bisimulation.",
         "The possibilistic baseline makes no posterior-risk, entropy, probabilistic, differential-privacy, timed, progress-sensitive, or universal partial-order claim."
@@ -2020,7 +2022,7 @@
         "definition_status": "defined",
         "implementation_status": "implemented",
         "test_status": "bounded",
-        "proof_status": "deliberately-unproved",
+        "proof_status": "proved",
         "checker_status": "implemented",
         "model_check_status": "model-checked",
         "runtime_enforcement_status": "not-enforced",
@@ -2030,7 +2032,8 @@
         "evidence_refs": [
           "docs/decisions/adrs/adr-099-participant-relative-predicate-opacity.md",
           "specs/formal/participant-semantics/participant-predicate-opacity.md",
-          "contracts/profiles/behavioral-relation/participant-opacity-baseline-v1.json",
+          "contracts/profiles/behavioral-relation/history/participant-opacity-baseline-v1-sem-231-rev2.json",
+          "contracts/profiles/behavioral-relation/participant-opacity-theorem-v1.json",
           "contracts/schemas/formal-analysis/participant-opacity-model-check-input-v1.json",
           "contracts/schemas/formal-analysis/participant-opacity-model-check-evidence-v1.json",
           "contracts/fixtures/formal-analysis/participant-opacity-model-check-input-v1/valid/opaque-transition-model.json",
@@ -2039,7 +2042,12 @@
           "implementations/python/packages/raes_processor/participant_opacity/_model_check.py",
           "implementations/python/tests/test_sem_231_participant_predicate_opacity.py",
           "implementations/python/tests/test_issue_961_participant_opacity.py",
-          "implementations/python/tests/test_issue_962_participant_opacity_model_check.py"
+          "implementations/python/tests/test_issue_962_participant_opacity_model_check.py",
+          "implementations/python/tests/test_issue_963_participant_opacity_proof.py",
+          "specs/formal/participant-semantics/isabelle/Participant_Opacity.thy",
+          "specs/formal/participant-semantics/participant-opacity-proof-evidence.json",
+          "tools/check_participant_opacity_proof.py",
+          "tools/isabelle_tool.py"
         ]
       },
       "source_refs": [

contracts/concept-authority/controlled-vocabularies-v1.json

@@ -774,6 +774,10 @@
         "service-content-v1": {
           "title": "Service Content v1",
           "description": "Exact reconciliation of authored content into a named service with controlled reset and participant-equivalent readback."
+        },
+        "service-search-index-schema-v1": {
+          "title": "Service Search Index Schema v1",
+          "description": "Exact reconciliation of a provider-neutral declared-field search-index schema with fresh native readback."
         }
       }
     },