aquaursa/parallax-5
GitHub: aquaursa/parallax-5
Stars: 0 | Forks: 0
# PARALLAX-5
**A five-obligation substrate for smart contracts and AI agents.**
[](https://github.com/aquaursa/parallax-5/actions/workflows/ci.yml)
[](LICENSE)
[](https://doi.org/10.5281/zenodo.20402755)
[](parallax/formal/lean/Parallax5.lean)
[](parallax/formal/lean/Parallax5.lean)
[](paper/supplement/catalog.csv)
PARALLAX-5 decomposes smart-contract safety into five primitive obligations:
| | Obligation |
|---|---|
| **A₁** | Value Conservation |
| **A₂** | Authorization Closure |
| **A₃** | Signature Integrity |
| **A₄** | Temporal Distinctness |
| **A₅** | External-Attestation Trust Boundary |
Under an explicit security-interface adequacy condition, every trust-base-respecting loss-inducing transition has a non-empty violation signature. The substrate is mechanized in Lean 4 (95 theorems, zero `sorry`), validated against a 53-incident empirical catalog ($5.97 B aggregate losses), and refined to a production EVM semantics via EvmYulLean. See [the paper](paper/parallax-5.pdf) for the full development.
## Repository structure
parallax-5/
├── paper/ Paper (parallax-5.pdf, 47 pages) and supplements
├── docs/ Standalone specifications:
│ CHARTER, FORK_PROTOCOL, CERTIFICATE_SCHEMA,
│ MAPPING_PROTOCOL, REGISTRY, DEPLOY, CROPS_VECTOR,
│ WALKAWAY_THEOREM, ARTIFACT_MAP, TOOL_COMPARISON,
│ plus the eight persona-driven docs added in v1.1.0
├── schemas/ JSON Schema for the certificate (v1.0)
├── parallax/ The substrate (research code):
│ formal/ Lean 4 module + Z3 + halmos + 53-incident catalog
│ obligations/ Five-obligation vocabulary (A₁–A₅)
│ obligationsol/ Obligation-typed Solidity static checker
│ economics/ Insurance pricing
│ product/ Trust-surface server + reports + badges
│ chronos/, hse/, standard/
├── src/ Installable Python packages:
│ parallax5_coordinator/ Coordinator + CLI + theorem framework
│ parallax5_cli/ Practical CLI (doctor, quote, audit-import, …)
├── registry/ ParallaxRegistry.sol + 24 Foundry tests + Lean state-machine proof
├── lean/ Lake project for substrate-level theorems
│ (Compositional, Walkaway, Registry)
├── demos/ Three worked examples with Lean proofs:
│ vault (A₁, D4) · bridge (A₃ + A₅) · agent_gate (A₁ + A₂ + D5)
├── case_studies/ Additional case studies
├── examples/ Worked certificate examples
├── notebooks/ EVMYulLean integration verification notebook
├── integrations/ Downstream integrations (GitHub Action)
├── scripts/ CI helpers and tooling
└── tests/ Test fixtures and Python test suites
## Quickstart
git clone --recursive https://github.com/aquaursa/parallax-5.git
cd parallax-5
pip install -e .
./RUN_VERIFICATION.sh
The full verification recipe runs all gates locally. Continuous integration runs the same gates on every push via `.github/workflows/ci.yml`.
## Navigation
- **Read the paper.** [`paper/parallax-5.pdf`](paper/parallax-5.pdf) — the canonical 47-page artifact.
- **The AI-Agent Containment Theorem worked example.** [`demos/agent_gate/`](demos/agent_gate/) — Demo 3 deploys an explicit adversarial agent behind a PARALLAX-5 gate; Lean proof in [`demos/agent_gate/proof/Containment.lean`](demos/agent_gate/proof/Containment.lean). The most concrete demonstration of the substrate's central AI-safety claim.
- **Challenge a specific claim.** [`paper/FALSIFICATION_CHALLENGE.md`](paper/FALSIFICATION_CHALLENGE.md) — the formal falsification surface for the substrate's main claims; the basis-counterexample bounty.
- **Use the substrate.**
- [`docs/CHARTER.md`](docs/CHARTER.md) — the structurally irrevocable non-capturability commitments.
- [`docs/FORK_PROTOCOL.md`](docs/FORK_PROTOCOL.md) — how to fork the standard cleanly.
- [`docs/CERTIFICATE_SCHEMA.md`](docs/CERTIFICATE_SCHEMA.md) — the certificate format specification.
- [`docs/MAPPING_PROTOCOL.md`](docs/MAPPING_PROTOCOL.md) — protocol for authoring tool-mapping documents in the `tool-mapping/{author}-v{major}` namespace.
- [`docs/REGISTRY.md`](docs/REGISTRY.md) — the onchain registry contract reference.
- **For partners and integrators.**
- [`docs/FOR_INTEGRATORS.md`](docs/FOR_INTEGRATORS.md) — how audit firms, runtime monitors, and AI safety platforms integrate the substrate (three patterns: tool-mapping, certificate-issuing, runtime-gate).
- [`docs/COMPLIANCE_MAPPING.md`](docs/COMPLIANCE_MAPPING.md) — EU AI Act / DORA / NIST AI RMF / ISO 42001 article-by-article mapping for Big 4 and regulatory consultants.
- [`docs/RELATED_WORK.md`](docs/RELATED_WORK.md) — positioning vs Certora, K-framework, MIRAI, Move Prover, CertiK, and the operational security tool ecosystem.
- [`docs/TOOL_COMPARISON.md`](docs/TOOL_COMPARISON.md) — coverage matrix and engagement cost comparison across Slither, Mythril, halmos, Foundry, Certora, and the substrate's own checkers.
- [`docs/IP_PROVENANCE.md`](docs/IP_PROVENANCE.md) — IP situation, license layering, contributor model, patent and trademark posture for M&A counsel and Big 4 third-party risk teams.
- **For researchers.**
- [`docs/THEOREM_INDEX.md`](docs/THEOREM_INDEX.md) — annotated index of the 95-theorem Lean core; identifies load-bearing theorems with intuitions.
- [`docs/OPEN_PROBLEMS.md`](docs/OPEN_PROBLEMS.md) — research roadmap; substantive contributions earn co-authorship on v1.1+ revisions.
- [`docs/EVMYUL_COMPOSITION.md`](docs/EVMYUL_COMPOSITION.md) — methodology for substrate × VM-semantics composition, with the EVMYulLean instance as the reference.
- [`docs/AI_SAFETY_INTERPRETATION.md`](docs/AI_SAFETY_INTERPRETATION.md) — substrate translated into AI-safety vocabulary (Tegmark, Anthropic RSP, Constitutional AI, mechanistic interpretability).
- [`docs/CATALOG_METHODOLOGY.md`](docs/CATALOG_METHODOLOGY.md) — how the 53-incident catalog was constructed; inter-rater reliability; falsification surface.
- **Run the demos.** `make demo-all` exercises the three end-to-end worked examples.
- **Validate a certificate.** `parallax5 validate path/to/cert.json` after install.
- **Compose a P-level certificate.** `parallax5-coordinator analyze tests/VulnerableLending.sol --output /tmp/cert.json` produces a defensible certificate from Slither, Mythril, halmos, and ObligationSol output.
- **Contribute.** See [`CONTRIBUTING.md`](CONTRIBUTING.md).
- **Report a vulnerability.** See [`SECURITY.md`](SECURITY.md).
## Citation
@software{parallax5_2026,
author = {{AquaUrsa Research}},
title = {{PARALLAX-5: A Five-Obligation Substrate for Smart Contracts
and AI Agents}},
year = {2026},
version = {1.0.1},
doi = {10.5281/zenodo.20402755},
url = {https://github.com/aquaursa/parallax-5},
note = {Companion verification artifact:
doi:10.5281/zenodo.20386868}
}
The repository also includes a [`CITATION.cff`](CITATION.cff) which the GitHub web UI renders as a "Cite this repository" widget.
## License
PARALLAX-5 is layered by component type per the [Non-Capturability Charter](docs/CHARTER.md):
| Component | License |
|---|---|
| Paper (`paper/parallax-5.{tex,pdf}`) | CC-BY 4.0 — see [`LICENSE-PAPER`](LICENSE-PAPER) |
| Standard text (specification documents, schemas, vocabulary) | CC0 1.0 Universal — see [`LICENSE-CC0`](LICENSE-CC0) |
| Code (Python, Solidity, Lean, scripts) | Apache License 2.0 — see [`LICENSE`](LICENSE) |
The standard vocabulary is structurally unencumbered; the reference implementation preserves attribution. See `docs/CHARTER.md` Article 2 for the full irrevocability commitment, and `docs/FORK_PROTOCOL.md` for the fork procedure.
## Acknowledgments
This substrate builds on EvmYulLean (Nethermind's Lean 4 EVM semantics, Cancun fork), forge-std (Foundry Standard Library, foundry-rs), Mathlib (Lean 4), and the open-source security tool ecosystem (Slither, Mythril, halmos). The certificate registry contract is anchored on Sepolia testnet.
| Paper | paper/parallax-5.pdf · doi:10.5281/zenodo.20402755 |
| Verification artifact | doi:10.5281/zenodo.20386868 |
| Onchain reference (Sepolia) | 0x8015A98dF9037Cd79a03B291a6fF3C2841992D5b |
| Version | 1.0.1 |
| Status | All gates green: 2,152 compositional · 129 Python fire tests · 24 Foundry · 47-page paper compiles cleanly |
| Verify all claims | CANONICAL_FACTS.md — single source of truth, reproducible in 3 min via ./RUN_VERIFICATION.sh |
| Licenses | Paper: CC-BY 4.0 · Standard text: CC0 1.0 · Code: Apache-2.0 |