aquaursa/parallax-5
GitHub: aquaursa/parallax-5
该项目是一个用 Lean 4 形式化验证的五义务安全底层基座，旨在为智能合约和价值承载 AI agent 提供可机械化证明的安全性保证。
Stars: 0 | Forks: 0
# PARALLAX-5
**用于智能合约和 AI agent 的五义务底层基座。**
[](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 将智能合约安全性分解为五个基本义务：
| | 义务 |
|---|---|
| **A₁** | 价值守恒 |
| **A₂** | 授权闭包 |
| **A₃** | 签名完整性 |
| **A₄** | 时间唯一性 |
| **A₅** | 外部认证信任边界 |
在显式的安全接口充分性条件下，每个遵守信任基底的致损状态转换都具有非空的违规签名。该底层基座在 Lean 4 中实现了机械化（包含 95 个定理，零 `sorry`），通过一个包含 53 起事件的经验目录（总损失达 59.7 亿美元）进行了验证，并通过 EvmYulLean 细化为生产级的 EVM 语义。有关完整的理论发展，请参阅[论文](paper/parallax-5.pdf)。
## 仓库结构
```
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
```
## 快速开始
```
git clone --recursive https://github.com/aquaursa/parallax-5.git
cd parallax-5
pip install -e .
./RUN_VERIFICATION.sh
```
完整的验证方案将在本地运行所有门禁。持续集成会在每次推送时通过 `.github/workflows/ci.yml` 运行相同的门禁。
## 导航
- **阅读论文。** [`paper/parallax-5.pdf`](paper/parallax-5.pdf) — 标准的 47 页文档。
- **AI Agent 遏制定理实操示例。** [`demos/agent_gate/`](demos/agent_gate/) — 演示 3 在 PARALLAX-5 门禁后方部署了一个显式的对抗性 agent；Lean 证明位于 [`demos/agent_gate/proof/Containment.lean`](demos/agent_gate/proof/Containment.lean) 中。这是对该底层基座核心 AI 安全声明最具体的演示。
- **挑战特定声明。** [`paper/FALSIFICATION_CHALLENGE.md`](paper/FALSIFICATION_CHALLENGE.md) — 底层基座主要声明的正式证伪界面；基础反例赏金。
- **使用该底层基座。**
- [`docs/CHARTER.md`](docs/CHARTER.md) — 结构上不可撤销的不可捕获性承诺。
- [`docs/FORK_PROTOCOL.md`](docs/FORK_PROTOCOL.md) — 如何干净地 fork 该标准。
- [`docs/CERTIFICATE_SCHEMA.md`](docs/CERTIFICATE_SCHEMA.md) — 证书格式规范。
- [`docs/MAPPING_PROTOCOL.md`](docs/MAPPING_PROTOCOL.md) — 在 `tool-mapping/{author}-v{major}` 命名空间中编写工具映射文档的协议。
- [`docs/REGISTRY.md`](docs/REGISTRY.md) — 链上注册表合约参考。
- **面向合作伙伴和集成商。**
- [`docs/FOR_INTEGRATORS.md`](docs/FOR_INTEGRATORS.md) — 审计公司、运行时监控器和 AI 安全平台如何集成该底层基座（三种模式：工具映射、证书签发、运行时门禁）。
- [`docs/COMPLIANCE_MAPPING.md`](docs/COMPLIANCE_MAPPING.md) — 面向四大审计和监管咨询公司的欧盟《AI 法案》/ DORA / NIST AI RMF / ISO 42001 逐条映射。
- [`docs/RELATED_WORK.md`](docs/RELATED_WORK.md) — 与 Certora、K-framework、MIRAI、Move Prover、CertiK 以及运营安全工具生态的定位对比。
- [`docs/TOOL_COMPARISON.md`](docs/TOOL_COMPARISON.md) — Slither、Mythril、halmos、Foundry、Certora 以及该底层基座自带检查器之间的覆盖率矩阵和参与成本比较。
- [`docs/IP_PROVENANCE.md`](docs/IP_PROVENANCE.md) — 面向并购法务顾问和四大第三方风险团队的知识产权现状、许可分层、贡献者模型、专利和商标态势。
- **面向研究人员。**
- [`docs/THEOREM_INDEX.md`](docs/THEOREM_INDEX.md) — 包含 95 个定理的 Lean 核心的注释索引；通过直觉说明识别承重定理。
- [`docs/OPEN_PROBLEMS.md`](docs/OPEN_PROBLEMS.md) — 研究路线图；实质性贡献可在 v1.1+ 修订版中获得共同署名。
- [`docs/EVMYUL_COMPOSITION.md`](docs/EVMYUL_COMPOSITION.md) — 底层基座 × 虚拟机语义的组合方法论，并以 EVMYulLean 实例作为参考。
- [`docs/AI_SAFETY_INTERPRETATION.md`](docs/AI_SAFETY_INTERPRETATION.md) — 转换为 AI 安全词汇（Tegmark、Anthropic RSP、Constitutional AI、机制可解释性）的底层基座。
- [`docs/CATALOG_METHODOLOGY.md`](docs/CATALOG_METHODOLOGY.md) — 53 起事件目录的构建方式；评分者间信度；证伪界面。
- **运行演示。** `make demo-all` 会运行三个端到端的实操示例。
- **验证证书。** 安装后执行 `parallax5 validate path/to/cert.json`。
- **组合 P 级证书。** `parallax5-coordinator analyze tests/VulnerableLending.sol --output /tmp/cert.json` 根据 Slither、Mythril、halmos 和 ObligationSol 的输出生成可靠的证书。
- **贡献。** 参见 [`CONTRIBUTING.md`](CONTRIBUTING.md)。
- **报告漏洞。** 参见 [`SECURITY.md`](SECURITY.md)。
## 引用
```
@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}
}
```
该仓库还包含一个 [`CITATION.cff`](CITATION.cff)，GitHub 网页界面会将其渲染为“引用此仓库”组件。
## 许可证
根据[不可捕获性宪章](docs/CHARTER.md)，PARALLAX-5 按组件类型进行分层：
| 组件 | 许可证 |
|---|---|
| 论文 (`paper/parallax-5.{tex,pdf}`) | CC-BY 4.0 — 参见 [`LICENSE-PAPER`](LICENSE-PAPER) |
| 标准文本（规范文档、schema、词汇表） | CC0 1.0 Universal — 参见 [`LICENSE-CC0`](LICENSE-CC0) |
| 代码 | Apache License 2.0 — 参见 [`LICENSE`](LICENSE) |
标准词汇在结构上不受限制；参考实现保留署名。有关完整的不可撤销承诺，请参阅 `docs/CHARTER.md` 第 2 条；有关 fork 程序，请参阅 `docs/FORK_PROTOCOL.md`。
## 致谢
该底层基座建立在 EvmYulLean（Nethermind 的 Lean 4 EVM 语义，Cancun fork）、forge-std（Foundry Standard Library，foundry-rs）、Mathlib（Lean 4）以及开源安全工具生态系统（Slither、Mythril、halmos）的基础之上。证书注册表合约锚定在 Sepolia 测试网上。
| 论文 | paper/parallax-5.pdf · doi:10.5281/zenodo.20402755 |
| 验证制品 | doi:10.5281/zenodo.20386868 |
| 链上参考（Sepolia） | 0x8015A98dF9037Cd79a03B291a6fF3C2841992D5b |
| 版本 | 1.0.1 |
| 状态 | 所有门禁全绿：2,152 个组合测试 · 129 个 Python fire 测试 · 24 个 Foundry 测试 · 47 页论文编译无误 |
| 验证所有声明 | CANONICAL_FACTS.md — 唯一事实来源，通过 ./RUN_VERIFICATION.sh 可在 3 分钟内复现 |
| 许可证 | 论文：CC-BY 4.0 · 标准文本：CC0 1.0 · 代码：Apache-2.0 |
标签：Lean 4, 以太坊, 区块链, 形式化验证, 智能合约, 逆向工具