This repository is an academic, model-level formal verification artifact. It does not contain a production bridge, validator, relayer, smart contract, wallet, key-management system, or deployed service.
| Scope | Status |
|---|---|
| Repository operations and public release surface | Production-maintained |
| Exact tracked CDSP and RAC sessions | Proof and model reports accepted |
Protected_Behavior_Obstructions |
Independent PARTIAL / NO SAME research companion; no product-refinement target |
Oracle_Interoperability_Protocol |
Model and artifact-binding reports accepted; the OIP reference implementation is prototype-stage and unaudited |
| Earlier commits and forks | Best effort only |
| Implementations and deployments | Not covered |
Production-maintained refers to repository review, reproducibility, release identity, public-surface checks, and coordinated reporting. It is not a production-readiness claim for any implementation or deployment.
This policy creates no warranty, support agreement, audit representation, or service-level commitment.
Use GitHub Private Vulnerability Reporting:
- Open the repository's Security tab.
- Select Advisories.
- Select Report a vulnerability.
If private reporting is unavailable, email jay@oraclizer.io with the subject
FORMAL VERIFICATION SECURITY. Do not include secrets, personal data,
production credentials, or unrelated confidential information.
Do not publish exploit details in an issue, Pull Request, discussion, social post, paper review, or standards forum before coordinated disclosure.
Ordinary counterexamples, invalid lemmas, overly strong assumptions, reproduction failures, model-scope concerns, and documentation errors are valuable and may use the public proof-review issue form when they are not sensitive or exploitable.
Include the exact commit, theory, theorem or locale, Isabelle version, AFP revision, build command, minimal reproduction, expected result, and observed result.
The maintainer will assess whether a report affects a tracked session and may request more information. No response, remediation, disclosure, release, or publication deadline is guaranteed. There is no bug bounty or financial reward program.
Credit may be offered in Git history, acknowledgments, release notes, or a security advisory when requested and appropriate.
A successful Isabelle build shows that the theories satisfy the Isabelle kernel under their definitions and assumptions. It does not establish model-to-code refinement, implementation safety, deployment security, cryptographic correctness, network liveness, or legal compliance.
The BSD 3-Clause License controls and includes warranty and liability limitations. This policy does not expand the license or certify the artifact.