NOTICE

ECHIDNA - Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance
Copyright (c) 2024-2026 Jonathan D.A. Jewell and ECHIDNA Project Contributors

LICENSING

This project is licensed under the GNU Affero General Public License,
version 3 or later (AGPL-3.0-or-later).

  Full text:               LICENSE  (also in LICENSES/AGPL-3.0-or-later.txt)
  SPDX-License-Identifier: AGPL-3.0-or-later

Four licences apply, to four distinct parts of the tree. This is deliberate,
not drift:

  1. APPLICATION CODE          AGPL-3.0-or-later
     The Rust core, Julia ML layer, Zig FFI, Chapel parallel layer, SPARK/Ada
     units, proof corpora, build system and CI. The AGPL's network clause
     applies: if you run a modified ECHIDNA as a network service, you must
     offer your users the modified source.

  2. MACHINE-READABLE SPECIFICATION SURFACE          MPL-2.0
     Everything under .machine_readable/ (A2ML descriptiles, contractiles,
     K9 configurations, anchors, policies), 0-AI-MANIFEST.a2ml, the package
     and container manifests, and the OCI image labels emitted by the
     stapeln / svalinn build tooling.

     This part is deliberately NOT AGPL. It is specification and metadata
     intended for interoperability, some of it on a path to standards-body
     submission, where strong copyleft would obstruct adoption and
     re-publication. MPL-2.0 keeps it file-level weak copyleft: improvements
     to these files stay open, but implementing against them carries no
     obligation.

  3. DOCUMENTATION             CC-BY-SA-4.0
     Everything under docs/, plus the top-level Markdown and AsciiDoc
     documents.

  4. echidna-playground/       MPL-2.0
     The Coq-Jr playground sub-project, which carries contributions from
     Coq-Jr Contributors rather than the ECHIDNA project. It remains under
     the Mozilla Public License 2.0 and is NOT relicensed.

Files that previously offered `Palimpsest-0.6` now carry MPL-2.0. The
Palimpsest Licence is MPL-2.0 with additional ethical provisions layered on
top, so MPL-2.0 is the faithful reduction when the Palimpsest layer is not
being asserted. See "THE PALIMPSEST FRAMEWORK IS NOT A LICENCE GRANT HERE"
below.

WHY THE MPL COMPONENT IS COMPATIBLE

MPL-2.0 section 3.3 designates the GNU licences - including
AGPL-3.0-or-later - as "Secondary Licenses". MPL-covered files may therefore
be combined into this AGPL-licensed work, and the combined work distributed
under the AGPL, while those files individually remain available under the
MPL. No file in this repository carries the MPL Exhibit B
"Incompatible With Secondary Licenses" notice, which would have prevented
this.

In short: the whole distributed work is AGPL-3.0-or-later. If you extract the
MPL-2.0 parts on their own - the machine-readable specification surface, or
echidna-playground/ - you may use those under MPL-2.0.

THE PALIMPSEST FRAMEWORK IS NOT A LICENCE GRANT HERE

ECHIDNA references the Palimpsest License as an ethical / philosophical
framework - a discipline about how contributions are received, attributed and
forwarded. That reference stands, and is orthogonal to the SPDX identifiers
above.

It is not a legal grant in this repository. The Palimpsest licence proper is
the legal licence only on `palimpsest-license`, `palimpsest-plasma` and
(prospectively) `consent-aware-http`. Some files here previously carried
`... OR Palimpsest-0.6` or `... AND Palimpsest-0.6` SPDX identifiers; those
were drift rather than a deliberate grant, referenced a version superseded by
the `palimpsest-license` repository, and had no licence text distributed with
this repository. They were removed in 2026-08.

LICENCE HISTORY

  dual MIT / Palimpsest-0.6  ->  MPL-2.0  ->  AGPL-3.0-or-later for
  application code, MPL-2.0 retained for the specification surface (2026)

The AGPL decision was taken by the project owner in 2026 and the per-file SPDX
headers were reconciled to match it in 2026-08, at which point the
machine-readable specification surface was deliberately held at MPL-2.0 for
interoperability and standards-submission reasons. Documents predating that
reconciliation may describe the whole project as MPL-2.0; LICENSE and this
file are authoritative.

================================================================================

THIRD-PARTY SOFTWARE

This project includes or depends on third-party software components with their
own licences. See the respective component directories and files for details.

Rust dependencies:    Cargo.toml + `cargo license`
Julia packages:       Project.toml + Manifest.toml
Deno / AffineScript:  deno.json (run `deno info`)

Theorem provers (integrated, not redistributed):
  Agda            BSD-3-Clause
  Coq / Rocq      LGPL-2.1
  Lean 4          Apache-2.0
  Isabelle/HOL    BSD-3-Clause
  Z3              MIT
  CVC5            BSD-3-Clause
  Metamath        Public Domain
  HOL Light       BSD-2-Clause
  Mizar           GPL-3.0
  PVS             GPL-2.0
  ACL2            BSD-3-Clause
  HOL4            BSD-3-Clause
  (...and the remaining backends; see docs/SUPPORTED_PROVERS.md)

Provers are invoked as external binaries, not linked or redistributed, so
their licences do not propagate to this work.

================================================================================

REUSE COMPLIANCE

This project follows the REUSE Software Licensing specification.

  .reuse/dep5                        bulk copyright declarations
  per-file headers                   SPDX-License-Identifier, per the
                                     four-part split described above
  LICENSES/AGPL-3.0-or-later.txt     application code
  LICENSES/MPL-2.0.txt               machine-readable specification surface
                                     and echidna-playground/
  LICENSES/CC-BY-SA-4.0.txt          documentation

Verify locally: `reuse lint`

Known gaps are recorded in docs/DEBT.md rather than left silent.

================================================================================

RSR / CCCP COMPLIANCE

See RSR_COMPLIANCE.adoc at repo root.

================================================================================

CONTRIBUTIONS

Contributions are licensed under the licence governing the part of the tree
they land in: AGPL-3.0-or-later for application code, MPL-2.0 for the
machine-readable specification surface and echidna-playground/, and
CC-BY-SA-4.0 for documentation. See CONTRIBUTING.adoc.

By contributing, you certify that:
  1. You have the right to submit the contribution.
  2. You agree to license it under the licence governing that part of the
     tree, as set out above.
  3. You understand the contribution will be publicly available.

================================================================================

SECURITY

See SECURITY.md and .well-known/security.txt.
Do not disclose security issues publicly until they have been addressed.

================================================================================

CITATIONS

If you use this software in academic work, please cite:

  @software{echidna2026,
    title  = {ECHIDNA: Extensible Cognitive Hybrid Intelligence for
              Deductive Neural Assistance},
    author = {Jonathan D.A. Jewell and ECHIDNA Project Contributors},
    year   = {2026},
    url    = {https://github.com/hyperpolymath/echidna},
    license = {AGPL-3.0-or-later},
  }

See CITATION.cff for machine-readable metadata and docs/CITATIONS.adoc for
the broader bibliography.

================================================================================

CONTACT

Repository:    https://github.com/hyperpolymath/echidna
Issue tracker: https://github.com/hyperpolymath/echidna/issues
Documentation: docs/ + RSR_COMPLIANCE.adoc + CLAUDE.md

================================================================================

Version: see CHANGELOG.md