Changelog

Unreleased

Declare original project material proprietary and publicly source-visible, not open source; add license headers and the root LICENSE notice.
Update public repository and commercial permission documentation; preserve third-party archives and published v1.0.0 assets.

v1.0.0 — Verification scaffold

Converted supplied heap/state sketches into ATS/Postiats-checked interfaces.
Added handwritten I/K/S lambda derivations and explicit Idris beta witnesses.
Added capture-avoidance examples, corrected fuel proofs, and explicit exhaustion status.
Compiled the Idris control-model program and checked its output in CI.
Strengthened Ada allocation contracts and tested capacity, exhaustion, and reset.
Discharged all six SPARK checks for the allocation-counter model.
Added pinned compiler/prover workflows and combined verify.sh validation.
Recorded source-pinned verification reports and original sketch provenance.
Added workflow diagrams, conceptual photographs, contribution/security policies, licensing-inquiry and support pages, repository description, topics, and badges.

The ATS evaluator, generation-checked slot-map heap, FFI adapter, full effectful semantics, differential tests, and cross-language correspondence remain open. Commercial license terms and a payment destination remain owner decisions.