PARALLAX-5: A Five-Obligation Substrate for Smart Contracts and AI Agents
Abstract
PARALLAX-5 is a transition-level obligation interface for value-bearing decentralized systems. The interface consists of five primitive obligations: value conservation, authorization closure, signature integrity, temporal distinctness, and external-attestation trust. Under an explicit security-interface adequacy condition, every trust-base-respecting loss-inducing transition has a non-empty violation signature; the claim is falsifiable by basis counterexamples that are precisely defined. The substrate composes with a production EVM semantics via a typeclass-based refinement: nineteen abstract theorems lift to compiled Lean 4 proof terms over EvmYulLean's EvmYul.EVM.State (Cancun fork). The Lean 4 module compiles to 95 theorems with zero sorry; 129 Python fire tests pass across three suites; a 53-incident empirical catalog (2016–2026, $5.97 billion aggregate losses) classifies each entry by minimum observability set. The package also defines a step-secure execution-time shield, an AI-Agent Containment Theorem, a five-component PARALLAX-CROPS trust-surface vector, a 19-field machine-checkable certificate schema with seven-state lifecycle, an onchain certificate registry (Solidity 0.8.24, live on Sepolia at 0x8015A98dF9037Cd79a03B291a6fF3C2841992D5b), and three worked examples covering value conservation, bridge attestation, and AI-agent runtime gating. The standard text is dedicated under CC0 with structurally irrevocable non-capturability commitments; code artifacts are released under Apache-2.0; this paper is licensed under CC-BY 4.0. v1.0.1 changes (vs v1.0.0, doi:10.5281/zenodo.20400525): repository-hygiene release. Removed four non-substrate subsystems (hse, product, economics, chronos) that were not paper-aligned. Standardized fire-test count from 134 to 129 to reflect the cleaned codebase. Restructured standalone specifications under docs/ directory with canonical names (CHARTER.md, FORK_PROTOCOL.md, CERTIFICATE_SCHEMA.md, etc.). Converted forge-std to a proper git submodule. Added CITATION.cff, CHANGELOG.md, CONTRIBUTING.md, SECURITY.md. The substrate's mathematical content, theorems, and verification gates are unchanged from v1.0.0.
Community
0 commentsNo discussion yet
Be the first to share a question or observation.