Skip to content

INDEPENDENCE v0.9.0 — Lean 4 + SPARK/Ada Automata Proof Laboratory

Choose a tag to compare

View all tags
@EmergentMonk EmergentMonk released this 30 Oct 18:35
Immutable release. Only release title and notes can be modified.
v0.9.0
f3e223e
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Release Notes

INDEPENDENCE v0.9.0 — Lean 4 + SPARK/Ada Automata Proof Laboratory

Release date: 31 October 2026
Project: QSOL-IMC — Software Declaration of Independence
Version: v0.9.0
License: Apache-2.0

Overview

INDEPENDENCE v0.9.0 introduces a consolidated, executable Lean 4 + SPARK/Ada Automata Proof Laboratory, extending the deterministic property testing and counterexample minimisation infrastructure established in v0.8.0.

This release introduces a versioned mathematical specification, new Lean theorem candidates, SPARK/Ada reference implementations, exhaustive finite cross-language verification, and a fully integrated interactive browser laboratory.

Two parallel development branches were consolidated into one authoritative implementation, preserving the stronger formal verification foundation while incorporating the interactive browser experiments and deployment improvements.

Correctness outranks complexity. Evidence outranks slogans.

What's New

1. AUTOMATA4/1 — Versioned Automata Specification

Introduced a human-reviewable specification for elementary cellular automata with:

  • Four binary cells per row.
  • All 256 elementary cellular automaton rules.
  • All 16 possible four-bit input configurations.
  • Simultaneous state transitions.
  • Explicit fixed-zero exterior boundaries.
  • Deterministic input ordering and reproducible outputs.

The resulting finite reference corpus contains 4,096 exhaustive rule/input combinations.

Canonical corpus SHA-256:

f1ecce4798a35f6642a065a0ffbf87e6bdfcbb30ba0afffb5fb0da69c7c40635

2. Lean 4 Mathematical Proof Laboratory

Introduced formal/lean/AutomataReference.lean containing six new theorem candidates covering:

  • Bounded neighbourhood indexing.
  • Rule 0 cell behaviour.
  • Rule 255 cell behaviour.
  • Rule 0 complete-row behaviour.
  • Rule 255 complete-row behaviour.
  • Known Rule 90 four-cell transitions.

The implementation uses the pinned Lean 4.35.0 toolchain and supports trust-zero kernel checking, theorem-by-theorem transitive axiom audits, and rejection of unapproved proof escapes.

These theorem candidates are separate from the historically recorded 13 Lean theorem checks.

Verification boundary: New theorem success is not claimed until the actual pinned Lean toolchain executes successfully.

3. SPARK/Ada Reference Implementation

Added a standalone SPARK-mode Ada reference kernel implementing the four-cell automaton semantics.

Features include:

  • Explicit preconditions and postconditions.
  • Bounded binary cell types.
  • Deterministic transition semantics.
  • GNATprove-compatible proof obligations.
  • A separate developer-only Ada command-line interface.
  • Strict ASCII-decimal input validation.
  • Explicit rejection of malformed and out-of-range inputs.

The verification pipeline supports compiling fresh Ada sources and comparing the executable against all 4,096 reference vectors and additional invalid-input cases.

The Ada CLI remains outside the SPARK proof boundary.

4. Executable Cross-Language Verification

Introduced a reproducible verification workflow connecting independent mathematical and executable models.

The development tools separately track:

  • Python finite-reference enumeration.
  • Lean mathematical proof execution.
  • GNATprove contract verification.
  • Compiled Ada runtime comparison.
  • Actual production JavaScript comparison.

The JavaScript verification executes the repository's existing lab/core.js:evolve() implementation rather than substituting a test-only implementation.

The full 4,096-case JavaScript corpus was successfully executed in GitHub Actions, producing the expected canonical digest.

5. Interactive Browser Formal Laboratory

Added a new first-party interactive laboratory to the INDEPENDENCE website.

Live page after deployment:
https://qsolkcb.github.io/INDEPENDENCE/#formal-lab

Visitors can:

  • Execute all 4,096 deterministic four-cell test cases.
  • Compare real JavaScript results against an independent arithmetic reference.
  • Detect unexpected mutation of input Uint8Array objects.
  • Inspect actual finite verification outcomes.
  • Export SHA-256 evidence receipts.

The browser laboratory uses the same authoritative AUTOMATA4/1 specification as the development verification tools.

No additional JavaScript frameworks, external services, telemetry or package manager are required.

6. Evidence Integrity and Independent Receipt Verification

Introduced stricter evidence reporting and verification.

The new tools:

  • Record exact source SHA-256 fingerprints.
  • Bind JavaScript evidence to both the production implementation and its comparator.
  • Verify canonical finite-vector digests.
  • Reject malformed or contradictory evidence.
  • Detect rehashed receipts containing inflated proof claims.
  • Validate complete Lean axiom declarations against recorded compiler output.
  • Preserve explicit NOT_RUN statuses for unavailable toolchains.

Added a separate standard-library Python verifier for browser-generated receipts:

scripts/verify_automata_browser_receipt.py

Receipt integrity establishes internal consistency, not independent authentication of execution.

7. Codex Review Findings Resolved

Four findings across the two original development pull requests were addressed during consolidation.

Three P2 findings in PR #18:

  • Corrected Lean evidence verification to compare complete recorded axiom lists against the raw compiler output.
  • Bound JavaScript evidence to exact production and comparator source hashes.
  • Removed the obsolete experimental Node.js invocation flag for compatibility with newer runtimes.

One P1 finding in PR #19:

  • Corrected an unterminated stylesheet link that would have prevented the application's JavaScript entry point from loading.
  • Added a regression test for the HTML integration.

The three original PR #18 review threads were answered and resolved.

8. Repository and Deployment Integration

  • Consolidated the formal verification architecture into one authoritative specification.
  • Added the browser Formal Lab to the site navigation.
  • Updated README, engineering invariants and formal verification roadmap.
  • Integrated new first-party assets into GitHub Pages deployment.
  • Extended the repository dependency audit.
  • Added an automated pull-request verification workflow.
  • Preserved historical Lean, SPARK/Ada and runtime evidence unchanged.

No mandatory Node.js, npm, Docker, Kubernetes, PyPI or third-party browser dependencies were introduced.

Verification Results

GitHub Actions validation of the final PR HEAD:

Verification Result
Python standard-library regression suite 299/299 PASSED
Four-cell finite reference corpus 4,096 cases checked
Production JavaScript comparison 4,096 cases PASSED
Browser laboratory native self-tests 5/5 PASSED
AUTOMATA4 evidence integrity PASS
Proof contract registry checks PASS
First-party dependency audit PASS
GitHub Actions workflow SUCCESS
New Lean kernel execution NOT_RUN in CI
New GNATprove contract execution NOT_RUN in CI
Compiled Ada differential execution NOT_RUN in CI

The CI results establish finite executable verification and regression coverage. They do not establish that the newly introduced Lean or Ada proof obligations have been formally discharged.

Reproducibility

Run the complete Python regression suite:

python3 -m unittest discover -s tests -v

Generate the finite reference evidence:

python3 scripts/check_automata_formal.py \
  --output automata4-static.json

Verify the evidence:

python3 scripts/verify_automata_evidence.py \
  automata4-static.json

Execute the developer-side JavaScript comparison:

python3 scripts/check_automata_formal.py \
  --run-js \
  --output automata4-js.json

With separately installed, compatible Lean and GNAT/Ada toolchains, require all proof and runtime stages:

python3 scripts/check_automata_formal.py \
  --require-all \
  --output automata4-evidence.json

Verify a browser-exported receipt:

python3 scripts/verify_automata_browser_receipt.py \
  automata4-browser-xxxxxxxxxxxx.json

The Python test suite and static verification tools require only Python's standard library.

Scope and Limitations

  • The 4,096-case corpus is exhaustive for the explicitly specified four-cell domain, not arbitrary automata dimensions.
  • Lean theorem candidates concern the mathematical model, not automatic correctness of JavaScript or Ada.
  • SPARK contracts require actual GNATprove discharge before being reported as verified.
  • Cross-language finite agreement is not a universal formal refinement theorem.
  • SHA-256 receipts do not independently authenticate who executed a tool or browser.
  • Historical proof artefacts are preserved without retroactively promoting their conclusions to the new model.

Source and Provenance

Merged pull request:
#18

Superseded development pull request (closed without merging):
#19

Verified final PR HEAD:
ac1245ad3747ddcd6b9d26cc693cf3270ef5de9c

Merge commit:
f3e223eb21792450323367b020b840e92b5154db

Successful GitHub Actions verification:
https://github.com/QSOLKCB/INDEPENDENCE/actions/runs/41106033252

Full changelog:
v0.8.0...v0.9.0

THE SOFTWARE DECLARATION OF INDEPENDENCE

This Is Not War, This Is a Divorce.

This Isn't War, This Is Pest Control.

No masters. No unnecessary dependencies. No fabricated proofs.

We have now given the Gremlins a formally specified laboratory, an executable test corpus, and a paper trail.

The revolution will not be containerised.

QSOL-IMC — Independent Software Sovereignty Initiative

Assets 3
Loading