Repository navigation
v1.0.0 — Verification scaffold
This first version packages the checked proof/model/interface components and
their evidence. It is a development foundation for the combined Unlambda,
ATS, Idris 2, and SPARK architecture.
Included
- ATS/Postiats 0.4.2-checked heap and state interface declarations.
- Handwritten SKI derivations with Idris 2 0.8.0-checked proof terms.
- A compiled fuel/control model with an executable smoke test.
- An assertion-tested Ada allocation counter with all six SPARK checks discharged.
- Combined compiler/prover validation, documented toolchains, and source-pinned reports.
- Contributor/security policies, licensing/support information, diagrams, and artwork.
Release assets
unlambda-idris-spark-v1.0.0-source.zip: source snapshot and documentation.unlambda-idris-spark-v1.0.0-evidence.zip: release-commit CI reports, plus a
manifest identifying the source commit and workflow runs.SHA256SUMS.txt: SHA-256 hashes of those two archives.
The release record and evidence manifest identify the exact source commit.
Validate asset checksums, install the documented toolchains, and run
bash verify.sh to reproduce the component checks.
Verification scope
The runtime .sats declarations have no .dats implementation or ATS/Ada
adapter. The Ada heap counts allocations and does not store nodes or generation
handles. The Idris control model does not evaluate Unlambda programs. These
components and their proof boundaries are documented in
the verification report.
This release does not claim full interpreter correctness, cross-language
correspondence, Windows runtime support, or production certification. The
delivery backlog retains those open gates.
The repository remains private. Original-code license terms have not been
selected, commercial licensing is inquiry-only, and the donation destination
is awaiting owner confirmation.
Checked release source
Source commit: 069ac3bba84550425c3ca3562ef56638c7b2adaa.