"The hard problem of AetherProof is not making TLA+, Why3, Lean, and SMT-LIB exchange data; it is proving that what these languages mean remains consistent when a specification moves from one representation to another." — AetherProof, Abstract

"Trust is explicit, not implicit: it does not propagate automatically between levels." — AetherProof, Section 8.8

📑 Table of Contents

• Overview
• Installation
• Experiments (v2.0.0)
• The Central Question
• Formal Definitions
• Propositions
• Architectural Pillars
• Relation to AetherGit and AetherFlow
• Platforms & Mirrors
• Project Structure
• Version History
• Citation
• Author
• License

🔭 Overview

AetherProof is a formal architecture — now with a first reference implementation — for specification-driven proof construction, incremental differential proving, and counterexample-guided remediation in multi-agent software ecosystems. It is the verification layer of the Aether family, sitting above AetherGit (storage) and AetherFlow (integration).

By decoupling specification from proof from remediation, AetherProof makes three usually-implicit things explicit:

1. What a specification means, across heterogeneous formal languages.
2. What evidence supports a proof, and under what assumptions.
3. When a counterexample is a code defect, a specification error, or an assumption violation.

The program is specified through three functional layers, three core mechanisms, and three protocol suites:

v2.0.0 at a glance

Figure 1 — The three-layer functional specification architecture. Double-headed arrows denote semantic relations, not refinement; the layers are functional categories, not hierarchical levels.

⚙️ Installation

pip install aetherproof-arch==0.1.0a1

Requires Python 3.9+. Runtime dependency: numpy >= 1.24.0.

git clone https://github.com/gitdeeper15/aetherproof.git
cd aetherproof

# Development (pytest, pytest-cov, ruff, mypy)
pip install -e ".[dev]"
pytest --cov=aetherproof

# Experiments (scikit-learn, matplotlib)
pip install -e ".[experiments]"

🧪 Experiments (v2.0.0)

❓ The Central Question

How can heterogeneous specification languages express different levels of system behavior while preserving semantic consistency, traceability, and verifiable relationships across their respective proof obligations?

This question is structural, not accusatory or normative. It does not presuppose that any one formalism is superior. It asks how the functions are in fact distributed across TLA+, Why3, Lean, and SMT-LIB, and what structural consequences follow from different distributions.

📐 Formal Definitions

Status: Defined in the v1.0.0 manuscript; implemented in v2.0.0.

Definition 1 — CSR Record

csr = (csr_id, artifact_hash, semantic_id, layer, language, content,
       semantic_role, requirements_refs, assumptions, relations,
       version, provenance)

Three distinct identities:

Figure 2 — CSR record structure: three identities and the relationship fields.

Definition 2 — Semantic Relation

Seven typed relations between CSR records:

refines · instantiates · approximates · implies · contradicts · depends_on · supersedes

Figure 3 — A requirement-driven trace. Solid arrows: refines / instantiates. Dashed arrow: approximates, which carries a loss_description.

Definition 3 — Translation Classification

Two orthogonal axes:

Figure 4 — Compatibility of Axis A and Axis B values. yes = compatible by definition; no = incompatible by definition; depends = depends on the specific mapping.

Definition 4 — Proof Obligation

O = (id, property, assumptions, source_csr, discharged_by, verdict)

Definition 5 — Proof Dependency Graph (PDG)

PDG = (Obligations ∪ Evidence ∪ Assumptions, Edges)

Definition 6 — Counterexample

C = (id, obligation, witness, refutation_evidence, type, provenance)

📜 Propositions

🏛️ Architectural Pillars

🔐 Per-Path TCB Manifests

The principal risk of relying on heterogeneous proof tools is that the trusted computing base (TCB) is implicit. AetherProof makes it explicit.

Figure 5 — Per-path TCB manifests. Each path records tool and prover versions, transformations, axioms and assumptions used, proof artifact hash, independent checker, resource bounds, and known limitations.

🔗 Relation to AetherGit and AetherFlow

AetherProof is the third layer in the Aether family:

flowchart LR
    G["🗄️ AetherGit<br/><sub>Storage layer</sub>"] --> F["🔀 AetherFlow<br/><sub>Integration layer</sub>"] --> P["📚 AetherProof<br/><sub>Verification layer</sub>"]

The three systems are methodologically independent. AetherProof requires only that the underlying store expose an append-only changeset log with parent pointers, which AetherGit's changeset tuple provides. Integration with AetherFlow is protocol-based (Section 7), not code-based.

🌍 Platforms & Mirrors

🗂️ Project Structure

AetherProof/
├── src/
│   └── aetherproof/                # Reference implementation (v2.0.0)
│       ├── __init__.py
│       ├── __version__.py
│       ├── models.py               # CSRecord, Obligation, Counterexample, Verdict, Layer
│       ├── cli.py
│       ├── csr/
│       │   ├── record.py           # Definition 1
│       │   └── relations.py        # Definition 2 (7 relations)
│       ├── obligations/
│       │   ├── generator.py        # Obligation Generator
│       │   └── odg.py              # ODG
│       ├── proof/
│       │   ├── pdg.py              # Definition 5
│       │   ├── invalidation.py
│       │   └── engine.py           # Differential Proof Engine
│       ├── remediation/
│       │   ├── diagnosis.py
│       │   ├── guardrails.py
│       │   └── cycle.py
│       ├── protocol/
│       │   └── messages.py         # M1–M10
│       └── review/
│           └── roles.py            # 5 roles + authority matrix
├── tests/                          # 40 tests, 79% coverage
│   ├── test_models.py
│   ├── test_csr.py
│   ├── test_obligations.py
│   ├── test_proof.py
│   ├── test_remediation.py
│   ├── test_protocol.py
│   └── test_review.py
├── experiments/                    # 5 experiments (run.py + results.json each)
│   ├── specification_synthesis/
│   ├── proof_obligation_generation/
│   ├── differential_proving/
│   ├── counterexample_diagnosis/
│   └── guardrail_effectiveness/
├── docs/
│   ├── 01_specification_language.md
│   ├── 02_proof_obligations.md
│   ├── 03_incremental_proof_engine.md
│   ├── 04_counterexample_remediation.md
│   ├── 05_integration_protocol.md
│   ├── 06_human_review_protocol.md
│   ├── 07_threats_and_limitations.md
│   ├── 08_research_status_statement.md
│   ├── system_architecture.md
│   └── figures/
│       ├── Fig1_Three_Layer_Architecture.png
│       ├── Fig2_CSR_Record_Structure.png
│       ├── Fig3_Semantic_Relations_Graph.png
│       ├── Fig4_Two_Axis_Classification.png
│       └── Fig5_TCB_Manifest.png
├── PUBLICATION/
│   └── AetherProof_Research_Paper.pdf
├── REPORTS/
│   └── v2.0.0/
│       └── report.md
├── DATA/                           # (empty — future)
├── ANALYSIS/                       # (empty — future)
├── EXTERNAL_REVIEW/                # (empty — future)
├── VALIDATION/                     # (empty — future)
├── AUTHORS.md
├── CHANGELOG.md
├── CITATION.cff
├── CONTRIBUTING.md
├── INVENTORY.md
├── LICENSE
├── OSF_REGISTRATION.md
├── PROJECT_SUMMARY.txt
├── README.md
├── VERSION                         # 2.0.0
├── manifest.json
├── scientific_state.json
├── netlify.toml
├── requirements.txt
├── upload_aetherproof.py
└── pyproject.toml                  # PEP 621

🕓 Version History

See CHANGELOG.md for details.

📖 Citation

Primary Manuscript

@techreport{baladi2026aetherproof,
  author       = {Baladi, Samir},
  title        = {AetherProof: Autonomous Formal Verification and Invariant Synthesis for Multi-Agent Software Ecosystems},
  institution  = {Ronin Institute / Rite of Renaissance},
  type         = {Research Paper},
  year         = {2026},
  month        = {November},
  version      = {1.0.0},
  doi          = {10.5281/zenodo.24013124},
  url          = {https://doi.org/10.5281/zenodo.24013124},
  note         = {Formal Architecture Proposal --- Formalization Stage.}
}

Software (Reference Implementation)

@software{baladi2026aetherproof_v2,
  author       = {Baladi, Samir},
  title        = {{AetherProof} v2.0.0: Empirical Implementation of Autonomous Formal Verification and Invariant Synthesis},
  year         = {2026},
  month        = {November},
  publisher    = {PyPI},
  version      = {0.1.0a1},
  doi          = {10.5281/zenodo.24013124},
  url          = {https://pypi.org/project/aetherproof-arch/},
  note         = {Reference implementation. Available via pip install aetherproof-arch==0.1.0a1.}
}

@software{baladi2026aethergit,
  author       = {Baladi, Samir},
  title        = {{AetherGit}: Scalable Source Control for Autonomous AI Agents},
  year         = {2026},
  month        = {November},
  version      = {1.0.0},
  doi          = {10.5281/zenodo.23966896},
  url          = {https://doi.org/10.5281/zenodo.23966896}
}

@techreport{baladi2026aetherflow,
  author       = {Baladi, Samir},
  title        = {AetherFlow: Automated Post-Merge Verification and Dynamic Conflict Resolution in Multi-Agent Programming Environments},
  institution  = {Ronin Institute / Rite of Renaissance},
  type         = {Research Paper},
  year         = {2026},
  month        = {November},
  version      = {1.0.0},
  doi          = {10.5281/zenodo.23979129},
  url          = {https://doi.org/10.5281/zenodo.23979129}
}

👤 Author

Samir Baladi Interdisciplinary AI Researcher — Ronin Institute / Rite of Renaissance

⚖️ License

MIT License

Copyright (c) 2026 Samir Baladi

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.