INDEPENDENCE v1.1.0 — The Most Rigorous Rant in the World.

INDEPENDENCE v1.1.0 — The Most Rigorous Rant in the World

Formal Models, Bounded Conformance, and Evidentiary Trust Boundaries

INDEPENDENCE v1.1.0 marks the formalisation and research-preservation milestone of the project.

What began as a declaration of software independence has evolved into a reproducible investigation of mathematical correctness, first-party software engineering, evidence integrity, and the limits of verification.

This release consolidates genuine mathematical proof results, executable conformance evidence, browser testing, and immutable research archives into a single, auditable body of work.

The central principle: A checksum is not a theorem. A theorem is not an integration test. And a passing test is not independent execution attestation.

Highlights

1. Cross-tool formal verification evidence

The preserved execution receipts report:

Verification system	Evidence
Lean 4.35.0	6 kernel-checked mathematical theorem statements
SPARK Ada / GNATprove	10 discharged verification conditions
Ada reference implementation	4,096 valid conformance vectors and 10 invalid-input cases
Production JavaScript	4,096 finite conformance vectors
Rocq 9.2	15 kernel-checked theorem/example obligations
Chromium and Firefox	92 historical recorded passing assertions

These are distinct evidence classes and are never represented as a single universal correctness proof.

2. Rocq arbitrary-width mathematical formalisation

The Rocq model extends beyond the original four-cell AUTOMATA4/1 specification.

Its mathematical obligations cover:

• Arbitrary finite Boolean-row lengths.
• Arithmetic rule-bit evaluation and explicit eight-pattern lookup.
• Equivalence of independently defined mathematical row evaluators.
• Output-length preservation.
• Fixed-zero boundary conditions.
• Rule 0 and Rule 255 identities.
• Rule 90 XOR semantics.
• Empty-row and singleton-row behaviour.
• Specialisation to the original four-cell model.

The preserved local Rocq execution records all 15 assumption audits closed and successful compilation.

This proves properties of the specified mathematical model, not formal refinement of production JavaScript.

3. Original proof evidence preserved

Two original, byte-identical research archives are now included in the repository.

AUTOMATA4 proof archive

• Lean 4 and GNATprove execution receipts.
• Ada and JavaScript differential evidence.
• Toolchain version records.
• Source commit and worktree provenance.
• Individual SHA-256 checksums.

SHA-256:
05990c6b614d463e973bdee55b20159b59a37844fe03d81f75927f729de99457

Rocq proof archive

• Original Rocq mathematical proof source.
• Kernel execution receipt.
• Recorded compiled .vo fingerprint.
• opam toolchain inventory.
• Source commit and SHA-256 checksums.

SHA-256:
c7a28f450c0cb50df51f16cec6190cbcfef850dcf88042e88911bb6167796d6f

Both original compressed archives are preserved without recompression or reserialization.

4. Fail-closed research evidence verification

Added scripts/verify_formalisation_archive.py, an offline Python standard-library verifier.

The verifier checks:

• Exact original archive fingerprints.
• Original archive member inventories.
• All 13 internal file checksums.
• Lean theorem and axiom-audit receipts.
• GNATprove contract-discharge records.
• Ada and JavaScript finite conformance evidence.
• Rocq theorem inventories and assumption-audit results.
• Historical source revisions.
• Evidence limitations and provenance declarations.

Following Codex review, the verifier additionally freezes every claim-bearing field in the research manifest.

Attempts to falsely promote Zenodo publication, independent execution attestation, production correctness, or arbitrary-width implementation verification are rejected.

5. Research-grade formalisation report

Added:

formal/research/v1.1.0/FORMALISATION_REPORT.md

The report includes the mathematical specification, methodology, theorem inventories, evidence hierarchy, original research provenance, reproducibility procedures, threats to validity, falsification criteria, and outstanding verification obligations.

The report explicitly rejects unsupported claims of universal implementation correctness, independent remote execution attestation, framework performance superiority, and general security certification.

6. Regression verification and browser compatibility

The final release candidate passed:

• 377 Python regression tests.
• Original research archive and receipt-integrity checks.
• Independent finite automaton conformance checks.
• Historical browser evidence restoration.
• Chromium browser journeys.
• Firefox browser journeys.
• Controlled HTTP failure and malformed-response scenarios.
• Narrow-viewport checks.
• First-party dependency auditing.

The post-merge GitHub Actions workflow also completed successfully.

No new website runtime dependencies were introduced.

Reproducibility

From the repository root:

python3 -m unittest discover -s tests -v

python3 scripts/verify_formalisation_archive.py \
  --output formalisation-integrity.json

python3 scripts/verify_browser_archive.py

For independent local execution of the actual Rocq compiler, activate the pinned Rocq 9.2.0 opam environment and run:

eval "$(opam env --switch=independence-rocq-9.2 --set-switch)"

python3 scripts/check_rocq_semantics.py \
  --require-rocq \
  --output rocq-executed-evidence.json

The repository's CI integrity checks do not substitute for actual local proof-tool execution.

Known limitations

The release does not claim:

• Formal refinement of production JavaScript against the Lean or Rocq specifications.
• Universal correctness for arbitrary JavaScript input widths.
• Independent authentication of locally generated proof execution.
• General security certification or WCAG compliance.
• Continuous live GitHub Pages availability.
• That removing third-party dependencies automatically improves software quality.

These limitations are intentionally part of the research record.

Research identifier

Zenodo DOI: https://doi.org/10.5281/zenodo.23816739

Author-associated identifier, subject to confirmation of the final public Zenodo record and its deposited contents.

Author: Trent Slade
Affiliation: QSOL-IMC — Independent Research
Year: 2026
Version: 1.1.0

Release provenance

• Repository: https://github.com/QSOLKCB/INDEPENDENCE
• Implementation and formalisation: PR #26
• Release target: e3962f894931f58a6c1c9d62490731c3d1f5a5a8
• Research archive: formal/research/v1.1.0/
• Verification: GitHub Actions and original local toolchain receipts.

---

Final declaration

Software independence is not the absence of libraries.

It is the ability to inspect our assumptions, understand our dependencies, reproduce our results, expose our failures, and distinguish what we have proved from what we merely believe.

A checksum cannot replace a theorem. A theorem cannot replace a test. A test cannot replace provenance. And no amount of rhetorical confidence can replace evidence.

INDEPENDENCE v1.1.0 puts that principle into executable practice.

The Gremlins may disagree. Their objections must now include a reproducible counterexample.

QSOL-IMC — Prove it, mate. 👹

INDEPENDENCE v1.0.1 — Immutable Real-Browser Evidence Preservation

Overview

INDEPENDENCE v1.0.1 establishes a reproducible, immutable archive of the original real-browser verification evidence collected during the v1.0.0 development cycle.

This preservation-focused release safeguards the original GitHub Actions browser evidence without rewriting its JSON contents, regenerating its ZIP structure, or changing its provenance.

The result is a versioned research artifact suitable for future formalisation, independent examination, and inclusion in a Zenodo evidence package.

Original bytes. Reproducible verification. Explicit provenance. No fabricated claims.

What's New

1. Lossless Browser Evidence Archive

Preserved the original GitHub Actions artifact from run 41112613136, artifact ID 13003029340.

The original 6,182-byte ZIP is stored losslessly as nine individually pinned base64 fragments under:

formal/evidence/browser/v1.0.1/base64/

Each fragment has a recorded Git blob fingerprint. Reconstruction must reproduce the original ZIP's exact SHA-256 digest:

76514017982d86c95003bd4f86ccdcf4404502ede4609ba8f7767b89ee6c396a

This is a byte-preservation mechanism, not a regenerated evidence substitute.

2. Historical Dual-Browser Evidence

The archived ZIP contains four original JSON reports from real Chromium and Firefox test runs.

Evidence category	Recorded assertions
Chromium — normal operation	14 PASS
Chromium — HTTP 503 fault	9 PASS
Chromium — malformed JSON fault	9 PASS
Chromium — narrow viewport	14 PASS
Firefox — normal operation	14 PASS
Firefox — HTTP 503 fault	9 PASS
Firefox — malformed JSON fault	9 PASS
Firefox — narrow viewport	14 PASS
Total	92/92 PASS

The requested narrow viewport was 390 × 844 pixels. The actual reported browser inner widths were approximately 469 pixels for Chromium and 472 pixels for Firefox.

These observations are preserved without overstating them as exact physical mobile-device tests.

3. Independent Offline Archive Verification

Introduced:

scripts/verify_browser_archive.py

The Python standard-library verifier:

• Reconstructs the original ZIP from the preserved base64 fragments.
• Validates exact original archive and member SHA-256 digests.
• Checks fragment Git blob fingerprints.
• Enforces the expected four-member archive inventory.
• Validates the historical source revision and staged-site fingerprint.
• Checks all 92 recorded browser assertions.
• Rejects malformed, substituted, duplicated, missing or tampered evidence.
• Preserves the distinction between internally consistent evidence and independently authenticated execution.

The verifier can also restore the original archive byte-for-byte.

4. Machine-Readable Provenance

Added a preservation manifest and accompanying documentation recording the original workflow, artifact, commit identifiers, checksums, browser observations and limitations.

The archive explicitly distinguishes:

• Original PR source HEAD: 63553a4118dea389547fdf5b821f9e04a50b9dd5
• Actual GitHub Actions PR test-checkout revision: 9f5616aa76d1dd18448b8e0d1300f7c6eb43d3b3
• Original staged-site SHA-256: d0350fe0b9123a3f4a21766e84122e9299de2872a3baa7a4a123226a6e473d62
• Published v1.0.0 commit: 764aec4bda8381de2aed620037d5ff992dba25ea

These identifiers are retained separately to prevent historical PR-test evidence from being misrepresented as production deployment evidence.

5. Adversarial Regression Testing

Added negative tests for archive corruption, modified fragments, replaced or missing members, forged PASS outcomes, altered source revisions, duplicate JSON keys, nonfinite numeric values, and unsafe overwrite attempts.

The repository's existing verification and browser-test infrastructure remains intact.

6. CI Preservation Integration

GitHub Actions now verifies the preserved archive, reconstructs the original ZIP, and publishes the restored bytes as a downloadable workflow artifact.

The final v1.0.1 pull-request verification reported:

• 351 passing Python regression tests
• Successful original evidence reconstruction
• Successful archive and member integrity verification
• Successful Chromium and Firefox browser journeys
• Successful narrow-layout checks in both engines
• Completed Codex review without reported findings

The post-merge verification workflow also completed successfully.

Reproducibility

Verify the archived evidence:

python3 scripts/verify_browser_archive.py

Restore the original ZIP:

python3 scripts/verify_browser_archive.py \
  --restore independence-real-browser-evidence.zip

Verify the restored ZIP directly:

python3 scripts/verify_browser_archive.py \
  --archive independence-real-browser-evidence.zip

Run the complete repository test suite:

python3 -m unittest discover -s tests -v

No third-party Python packages, npm dependencies, containers or network access are required for archive verification.

Evidence Boundaries

The preserved evidence documents a historical GitHub Actions PR test checkout.

It does not independently authenticate browser execution, establish continuous GitHub Pages availability, certify WCAG conformance, or formally prove the production JavaScript implementation.

The archive does not alter previously established Lean, SPARK/Ada or finite-differential proof boundaries.

Provenance

Implementation PR:
#23

Merged commit:
5d706e84b186ea9d353b44701a7fe8c3bd81593e

Successful original PR validation:
https://github.com/QSOLKCB/INDEPENDENCE/actions/runs/41120551351

Successful post-merge validation:
https://github.com/QSOLKCB/INDEPENDENCE/actions/runs/41122426425

Evidence preservation tracking:
#21

Full changelog:
v1.0.0...v1.0.1

---

THE SOFTWARE DECLARATION OF INDEPENDENCE

This Is Not War, This Is a Divorce.

This Isn't War, This Is Pest Control.

No fabricated proofs. No rewritten evidence. No unnecessary dependencies.

The Gremlins have been tested, documented, checksummed, and permanently archived.

The revolution will not be containerised.

QSOL-IMC — Independent Software Sovereignty Initiative

INDEPENDENCE v1.0.0 — GitHub Pages Deployment Verification Hardening

Overview

This update strengthens INDEPENDENCE's GitHub Pages deployment verification infrastructure by separating successful publication from subsequent public CDN observations.

It fixes a failure mode where GitHub Pages successfully published the website, but the overall deployment workflow was incorrectly marked failed because an immediate HTTPS verification returned HTTP 404.

The release preserves strict SHA-256 evidence validation while improving failure reporting, artifact retention, reproducibility, and historical deployment verification.

A successful deployment is not the same as a verified public observation. Both outcomes must be reported independently.

What's Changed

Deployment Success and CDN Verification Are Now Separate

• GitHub Pages publication success is reported independently of public CDN availability.
• Post-deployment verification failures no longer incorrectly invalidate a successful publication.
• Failed public-byte checks produce explicit NOT_VERIFIED evidence and workflow warnings.
• A successful publication does not automatically claim remote asset integrity.

Deterministic Deployment Manifest Preservation

• Every deployment preserves its original deployment-manifest.json.
• The manifest records the exact staged source revision and file checksums.
• Preserved evidence remains independent of subsequent repository changes.
• Freshly collected ledger data cannot silently alter historical deployment evidence.

Improved Artifact Retention and Fallback

The manual verification workflow now uses a two-stage retrieval strategy:

1. Prefer the separately preserved independence-pages-manifest artifact, which follows repository artifact-retention settings.
2. Fall back to the original github-pages/artifact.tar only when the preferred artifact is unavailable.

This addresses the short default retention period of GitHub Pages upload artifacts.

The verifier refuses missing, malformed, duplicated, substituted, or inconsistent manifest data.

New Strict Manifest Selection Tool

Introduced:

scripts/select_public_manifest.py

Capabilities include:

• Byte-exact preservation of the original deployment manifest.
• Strict schema and SHA-256 validation.
• Safe extraction of the manifest from historical Pages archives.
• Detection of duplicate or malformed archive members.
• Fail-closed handling of unavailable or corrupted evidence.
• Machine-readable NOT_VERIFIED receipts when selection fails.

A corrupt preferred manifest never silently triggers a fallback to another source.

Manual Public-Site Verification

Added the GitHub Actions workflow:

Verify Published INDEPENDENCE Bytes

This workflow accepts an original deployment run ID, retrieves its preserved evidence, and compares every publicly served asset against its original checksums.

Verification can be repeated without republishing the website.

The workflow retains the distinction between:

• REMOTE_BYTES_MATCHED_UNATTESTED — observed public bytes match the preserved manifest.
• NOT_VERIFIED — the public deployment could not be confirmed.

Improved HTTP Diagnostics

The public verifier now identifies the specific asset and HTTP status responsible for a failure, rather than producing an ambiguous HTTP 404 message.

HTTPS-only scope restrictions and fail-closed redirect handling remain enforced.

Validation

The final pull-request validation completed successfully:

Verification	Result
Python regression suite	341/341 passed
Chromium browser journeys	Passed
Firefox browser journeys	Passed
Narrow-layout browser journeys	Passed
Manifest selection and fallback tests	Passed
Missing and corrupted evidence rejection	Passed
Deployment artifact integrity checks	Passed

These results establish successful local and CI verification. They do not independently establish that the public GitHub Pages CDN is currently serving the expected bytes.

Compatibility and Dependencies

• No application feature changes.
• No changes to the existing automata or formal proof semantics.
• No additional production JavaScript dependencies.
• No npm, Docker, Kubernetes, Selenium or Playwright requirement for the deployed website.
• Python verification remains standard-library-only.

Provenance

Pull request:
#22

Merged commit:
764aec4bda8381de2aed620037d5ff992dba25ea

Successful pull-request validation:
https://github.com/QSOLKCB/INDEPENDENCE/actions/runs/41116558846

Historical deployment investigated:
https://github.com/QSOLKCB/INDEPENDENCE/actions/runs/41113714704

Verification Limitations

The fix corrects deployment status reporting, evidence preservation and verification retryability. It does not itself establish the root cause of a persistent public HTTP 404 or guarantee CDN availability.

Public-byte verification remains a separate, explicit observation that must succeed before remote asset integrity is claimed.

---

THE SOFTWARE DECLARATION OF INDEPENDENCE

This Is Not War, This Is a Divorce.

No fabricated deployment failures. No fabricated verification successes. No unnecessary dependencies.

The Gremlins may interfere with deployment, but they no longer get to rewrite the evidence.

The revolution will not be containerised.

QSOL-IMC — Independent Software Sovereignty Initiative

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

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....

INDEPENDENCE v0.8.0 — Deterministic Property Generation & Counterexample Minimisation

Release Notes

INDEPENDENCE v0.8.0 — Deterministic Property Generation & Counterexample Minimisation

Release date: 31 October 2026
Project: QSOL-IMC — Software Declaration of Independence
Release: v0.8.0

Overview

INDEPENDENCE v0.8.0 introduces a fully executable, dependency-free Property Laboratory for deterministic property generation, reproducible fault injection, counterexample minimisation, and typed-array ownership testing.

Building on the v0.7 proof contracts and formally checked reference-model evidence, this release advances the project from checking predefined fixtures to systematically generating inputs, detecting behavioural violations, and reducing failing cases to smaller reproducible witnesses.

Correctness outranks speed. Evidence outranks slogans.

What's New

1. Deterministic Property Generation

• Introduced PROPERTY-LAB/1 with the existing first-party xorshift32 generator.
• Supports reproducible seeds and configurable runs of 1–512 generated cases.
• Tests the real JavaScript cellular automaton against an independently implemented transition oracle.
• Covers bounded binary rows, elementary cellular automaton rules, and fixed-zero boundary semantics.
• Detects incorrect outputs and mutation of input typed arrays.
• Produces identical generated vectors for identical configurations.

2. Counterexample Minimisation

Introduced a deterministic, bounded counterexample shrinker.

The laboratory uses a deliberately injected wraparound-boundary defect to demonstrate how a larger failing input can be reduced to a canonical minimal witness.

Original counterexample:

• Width: 8
• Rule: 110
• Mask: 255

Minimised counterexample:

• Width: 1
• Rule: 4
• Mask: 1

The shrinker uses a documented width-first, rule-then-mask ordering and rechecks the failure predicate during minimisation.

The injected defect is an educational test fixture, not a vulnerability discovered in the deployed automaton.

3. Typed-Array Ownership Protection

Reproduces the existing public-API counterexample in which Object.freeze() protects an enclosing object but does not prevent mutation of its contained Uint8Array.

Added the opt-in guardedSnapshot() interface:

• Validates automaton dimensions, cell values, and fingerprint consistency.
• Rejects stale or corrupted input snapshots.
• Creates independent private copies of cell data.
• Returns fresh typed-array copies to callers.
• Preserves fingerprint consistency against external mutations.

The original buildAutomaton() behaviour is retained for compatibility and historical reproducibility.

4. Interactive Browser Property Lab

Added a new interactive section to the INDEPENDENCE website.

Users can generate deterministic trials, inspect failure classifications, examine minimised counterexamples, and export evidence receipts.

The interface operates entirely in the browser using first-party HTML, CSS and JavaScript, without additional runtime packages, remote services, telemetry or backend infrastructure.

5. Reproducible Evidence Receipts

Introduced PROPERTY-LAB-RECEIPT/1 with SHA-256 fingerprints over exact UTF-8 JSON payloads.

Receipts contain the generator configuration, generated cases, counterexample witnesses, minimisation metadata, ownership observations, and explicit verification limitations.

The new Python standard-library verifier, scripts/verify_property_receipt.py, independently reconstructs expected data and rejects malformed, tampered or internally contradictory reports.

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

6. Expanded Regression and Security Testing

• Added 16 native JavaScript property assertions.
• Added 16 Python standard-library regression tests.
• Added tests for deterministic replay, invalid configurations, forged receipts, false formal-proof claims and counterexample manipulation.
• Addressed Codex's P2 finding concerning mutation of the actual Uint8Array supplied to evolve().
• Confirmed that correct output cannot conceal source-input corruption.
• Integrated the new Property Lab into the existing GitHub Pages deployment workflow and first-party asset audit.

Verification Results

Local verification against PR #17 HEAD:

Check	Result
Python regression suite	260/260 passed
Repository dependency audit	PASS
Files inspected	160
Dependency/remote asset findings	0
Codex review finding	Fixed and resolved
Historical Lean/SPARK/Ada evidence	Preserved unchanged

Scope and Limitations

Generated property checks are finite behavioural tests, not mathematical proofs of arbitrary JavaScript execution.

Counterexample minimisation is canonical within the explicitly defined bounded search space, not a general-purpose global minimisation guarantee.

The injected wraparound defect is separate from the genuine legacy typed-array ownership counterexample.

This release does not alter or promote the previously recorded Lean 4, SPARK/Ada or Ada/Python verification claims.

Deployment

The Property Lab is integrated into the existing first-party GitHub Pages website.

Live site: https://qsolkcb.github.io/INDEPENDENCE/#property-lab

Run the repository tests and audit:

python3 -m unittest discover -s tests -v
python3 scripts/audit.py --json

Verify an exported Property Lab receipt:

python3 scripts/verify_property_receipt.py property-lab-<hash>.json

No Node.js, npm, Docker, Kubernetes, third-party Python packages or new browser runtime dependencies are required.

Source and Provenance

Merged pull request: #17

Verified PR HEAD: 70177db2c01beb77ae2c7fe19bc11f1776600a1a

Merge commit: b8888deacd8ae72e8812848faafce82047cd9755

License: Apache-2.0

---

THE SOFTWARE DECLARATION OF INDEPENDENCE

This Is Not War, This Is a Divorce.

This Isn't War, This Is Pest Control.

Now with a deterministic shrink ray for catching Gremlins. 👹

QSOL-IMC — Independent Software Sovereignty Initiative

What's Changed

• draft: v0.7.3 Lean 4 Mathematical Foundation — kernel check required by @EmergentMonk in #10
• fix(lean): discharge CRT right-inverse without undecidable product quantifier by @EmergentMonk in #11
• archive: preserve v0.7.3 Lean kernel evidence and exact provenance for Zenodo v1.1.0 by @EmergentMonk in #12
• fix(spark): correct scalar GPR directory attributes before GNATprove by @EmergentMonk in #13
• feat: Pest Control declaration + preserve 21-check SPARK evidence by @EmergentMonk in #14
• feat(v0.7.4): build real Ada CLI and verify Python differential execution by @EmergentMonk in #15
• archive(v0.7.4): preserve original 150/8,903 Ada runtime receipts with exact byte provenance by @EmergentMonk in #16
• feat(v0.8): deterministic property generation, bounded shrinking and ownership guard by @EmergentMonk in #17

Full Changelog: v0.7.2...v0.8.0

v0.7.2 — SPARK Ada Reference Kernel & Proof-Conformance Bridge, encompassing both milestones.

INDEPENDENCE v0.7.1 + v0.7.2

SPARK ADA REFERENCE KERNEL & PROOF-CONFORMANCE BRIDGE

TWO IMPLEMENTATIONS. ONE SPECIFICATION. ZERO BORROWED PROOFS.

Release date: 30 October 2026
Organisation: QSOL-IMC
Release type: Formal Methods Infrastructure / Cross-Language Verification
Combined release version: v0.7.2
Previous release: v0.7.0
Licence: Apache-2.0

PROVING THE REFERENCE DOES NOT PROVE THE IMPLEMENTATION.

VERIFY THE MATHEMATICS. VERIFY THE CONTRACTS. TEST THE CONFORMANCE. PRESERVE THE GAPS.

---

Overview

INDEPENDENCE v0.7.1 and v0.7.2 establish the project's first cross-language formal verification infrastructure.

Building upon the Proof Contracts framework introduced in v0.7.0, these releases introduce a narrow SPARK/Ada reference implementation, a shared versioned mathematical specification, an independently implemented Python reference, and an exhaustive finite-domain conformance testing system.

The objective is to create a reproducible evidence chain connecting mathematical specifications, executable reference implementations, formal proof obligations, and actual software behaviour.

The central engineering principle is:

A verified Ada reference implementation does not automatically establish that Python or JavaScript implements the same specification correctly.

Each implementation must be independently checked.

These releases establish that separation without claiming mathematical proofs or Ada contract discharges that have not yet been executed.

Repository: https://github.com/QSOLKCB/INDEPENDENCE

---

PART I — v0.7.1: SPARK Ada Reference Kernel

1. Versioned Mathematical Specification

Introduced formal/spec/kernel-v1.json, defining shared semantics for a narrow set of mathematical and graph operations.

The specification establishes exact input domains, output formats, arithmetic rules, preconditions, and behavioural limitations.

It is intended to serve as the shared authority for independently implemented reference systems.

Changing the specification requires deliberate review and version control rather than silently changing either implementation to match the other.

2. SPARK/Ada Reference Implementation

Introduced a standalone reference kernel implemented in Ada, with SPARK mode enabled.

The initial kernel implements:

Operation	Defined behaviour
Address	Rectangular row/column addressing
Decode	Recover row and column from an address
Parity addition	GF(2) addition
Parity multiplication	GF(2) multiplication
Phase addition	Cyclic addition modulo 3
Edge validation	Validate distinct, in-range endpoints
Edge transition	Apply a parity transition to validated endpoints

The implementation uses explicit bounded types and function contracts.

Addressing is restricted to finite dimensions.

The parity operations operate over GF(2), while cyclic phase addition operates over the integers modulo 3.

Edge transitions require validated endpoints before the transition operation is permitted.

Important Mathematical Boundaries

The initial rectangular addressing implementation is not a proof of the Chinese Remainder Theorem bijection.

Validating two endpoints does not establish that an edge exists in a Penrose tiling or any particular graph.

Modulo-3 phase closure does not automatically establish quantum qutrit dynamics.

These are separate mathematical obligations for future research.

3. Explicit SPARK Contracts

Introduced Ada preconditions and postconditions for the reference kernel.

The contracts document expected behaviour, permitted inputs, output relationships, and required edge validation.

Their purpose is to make the implementation suitable for subsequent GNATprove analysis.

A declared contract is a proof obligation—not a completed formal proof.

4. GNATprove Verification Infrastructure

Introduced scripts/check_spark_reference.py.

The verification tool can inspect the reference source, validate expected declarations, detect disallowed proof-escape constructs, and optionally invoke GNATprove in an appropriate development environment.

The proof runner records command details, tool output, and verification status.

Strict verification mode is designed to fail when proof evidence is missing or inconclusive.

Unreviewed assumptions and missing proof results are not permitted to become successful verification claims.

GNATprove and GNAT remain optional development-time tools.

They are not required to run or deploy the INDEPENDENCE website.

5. Hardened Ada CLI

Introduced a CLI adapter providing deterministic input/output access to the reference functions.

During adversarial review, an input-validation issue was identified.

Ada's numeric parser could accept alternative numeric literal formats, such as:

2#1#

This conflicted with the shared specification's requirement for ordinary ASCII decimal input.

The CLI now validates decimal syntax before numeric conversion.

Invalid formats, signs, unsupported syntax, and out-of-range inputs are rejected.

This prevents an implementation-language parsing convenience from silently changing the externally defined protocol.

---

PART II — v0.7.2: Proof-Conformance Bridge

6. Independent Python Reference Kernel

Introduced formal/python/kernel.py.

This is a separately implemented Python reference using the shared versioned specification.

The Python implementation is compared against independently written arithmetic oracle functions rather than simply copying the Ada algorithms.

Its purpose is to establish finite-domain behavioural agreement.

It does not claim to verify all existing Python application code.

7. Exhaustive Finite-Domain Verification

Introduced a systematic finite-domain test generator.

The conformance system evaluates every defined input within selected practical bounds.

Verified finite-domain coverage

Operation	Test cases
Rectangular addressing	2,176
Address decoding	2,176
GF(2) addition and multiplication	8
Modulo-3 phase addition	9
Edge endpoint validation	3,840
Edge transitions	672
Total valid-domain cases	8,881
Additional invalid-input cases	16

The Python reference and independent oracle agreed on the recorded finite-domain sweep.

This establishes tested agreement over the declared domain, not a theorem about arbitrary inputs or unrelated application code.

8. Optional Python/Ada Differential Execution

Introduced scripts/run_kernel_conformance.py.

The bridge supports actual invocation of a compiled Ada CLI using the same versioned input semantics as the Python reference.

The comparison machinery can:

• Generate deterministic input vectors.
• Include every operation in a seeded sample.
• Compare exact output values.
• Reject mismatches, failed processes, stderr output, and timeouts.
• Record the supplied Ada executable's SHA-256 digest.
• Preserve source/specification digests.
• Distinguish actual runtime comparison from formal verification.

The default Ada comparison sample contains 128 valid cases, with additional invalid-input and lexical-input challenges.

The complete finite domain can also be selected.

When the Ada executable is unavailable, the comparison remains explicitly NOT_RUN.

9. Specification Integrity Lock

Introduced an exact SHA-256 lock for the shared kernel-v1.json specification.

This prevents the conformance bridge from silently accepting changed semantics under the same version identity.

Unreviewed specification modifications fail validation.

The lock protects consistency between the documented reference contract and the conformance experiment.

It does not authenticate the origin of the specification.

10. Separate Verification Evidence Classes

Introduced structured reporting that deliberately separates different kinds of verification evidence.

Evidence class	Meaning
Mathematical proof	Lean theorem checked against its specification
Ada contract verification	GNATprove discharge of stated SPARK obligations
Python conformance	Observed agreement with an independent reference
Ada CLI conformance	Actual comparison against an executed Ada program
Unresolved obligations	Claims not yet proved, tested, or independently established

A passing Python test cannot promote an Ada contract to verified status.

A successful Ada reference proof cannot automatically promote Python to formally correct.

Matching an executable's outputs cannot independently establish the executable's provenance.

NO PROOF BY ASSOCIATION.

11. SHA-256 Conformance Receipts

Introduced versioned conformance receipts containing source hashes, specification identity, finite test counts, execution classifications, unresolved obligations, and limitations.

The corresponding offline verifier, scripts/verify_kernel_receipt.py, independently checks payload integrity and expected evidence structure.

Adversarial regression tests reject altered results, fabricated formal proof claims, and misleading Ada provenance assertions.

Receipts are self-consistency records.

They do not provide independent execution attestation or demonstrate that a supplied Ada binary was built from the reviewed source.

---

Verification Summary

Verification activity	Recorded outcome
Python finite-domain comparisons	8,881 cases agreed
Invalid-input comparisons	16 cases agreed
Ada CLI compilation	NOT RUN
Ada/Python runtime differential comparison	NOT RUN
GNATprove formal contract discharge	NOT RUN
Lean kernel-checked mathematical proofs	NOT RUN
Existing ...

INDEPENDENCE v0.7.0 — Proof Contracts: Evidence Before Proof

INDEPENDENCE v0.7.0 — THE GREMLINS HAVE MET THE PROOF CONTRACTS

INDEPENDENCE v0.7.0 — PROOF CONTRACTS

EVIDENCE BEFORE PROOF.

Release date: 30 October 2026
Organisation: QSOL-IMC
Release type: Verification Infrastructure / Mathematical Research Foundation
Previous version: v0.6.0
Licence: Apache-2.0

THE GREMLINS HAVE MET THE CONTRACT.

THEY HAVE NOT YET MET THE THEOREM PROVER.

Overview

INDEPENDENCE v0.7.0 introduces PROOF CONTRACTS, the first stage of a multi-release programme to strengthen software correctness through mathematical specifications, bounded exhaustive verification, independent reference implementations, and eventually formal verification using Lean 4 and SPARK/Ada.

The project's previous releases established dependency-free browser engineering, deterministic experiments, reproducible evidence receipts, mutation testing, and human-directed AI development.

This release asks a more demanding question:

What can we actually establish about the correctness of the software we've built?

The answer begins by distinguishing mathematical proofs, exhaustive bounded tests, finite observations, and discovered counterexamples.

Rather than assigning an unsupported universal correctness score, INDEPENDENCE now maintains a machine-readable registry of verification obligations and their actual evidence status.

Eight registered obligations. Five executable checks. One reproduced counterexample. Zero mathematical proofs falsely claimed.

Live verification laboratory: https://qsolkcb.github.io/INDEPENDENCE/#proof

Repository: https://github.com/QSOLKCB/INDEPENDENCE

---

New Features

1. PROOF-CONTRACTS/1 — Machine-Readable Verification Registry

Introduced proof/contracts.json, a versioned specification of the project's initial verification obligations.

Every obligation records its identifier, source file and function, risk priority, expected behaviour, verification domain, evidence category, and formal verification status.

The registry includes eight obligations:

Obligation	Evidence classification
AUTOMATA-TRANSITION	Bounded exhaustive verification
DEPENDENCY-SUM	Finite arithmetic verification
AUTOMATA-REPLAY	Finite deterministic replay verification
SHA-FORMAT	Finite validation verification
FINGERPRINT-IMMUTABILITY	Reproduced counterexample
RECEIPT-AUTHENTICITY	Pending
LEAN-TRANSITION	Pending
SPARK-TRANSITION	Pending

All eight obligations remain formally classified as NOT_PROVED.

This is deliberate: successful testing must never be presented as equivalent to a formally checked theorem.

2. Exhaustive Bounded Cellular Automata Verification

Introduced an independent mathematical oracle for elementary cellular automata.

The verification engine compares the actual JavaScript evolution implementation against a separately implemented transition calculation.

The experiment enumerates every binary input state of widths 1 through 8 under all 256 elementary cellular automaton rules.

Executed development results:

Measurement	Result
Cellular automaton rules	256
Input widths	1–8
Input/rule combinations	130,560
Output cells compared	918,016
Observed mismatches	0

The checks include the existing fixed-zero boundary policy.

This establishes agreement over the enumerated finite domain. It does not establish mathematical correctness for every possible lattice size or arbitrary JavaScript input.

3. Independent Dependency Arithmetic Verification

Introduced an exact-integer reference calculation for the project's synthetic dependency-tree arithmetic.

The oracle uses JavaScript BigInt to calculate finite geometric sums independently of the production implementation.

The test domain includes combinations of direct dependency counts, branching factors, and tree depths, plus the maximum allowed input triple.

Executed development result: 463 arithmetic cases passed.

The checks verify agreement with the specified synthetic model, not real-world dependency graphs or package-manager behaviour.

4. Deterministic Replay and Fingerprint Verification

Extended verification of the existing cellular automata implementation.

The new checks evaluate combinations of deterministic seeds, automaton rules, and lattice dimensions.

An independently implemented BigInt FNV-1a reference verifies the resulting cell-state fingerprints.

Executed development result: 36 replay cases passed.

The tests establish reproducible results for their specified inputs and reference calculations.

The FNV-1a fingerprint remains a noncryptographic checksum and is not presented as a security proof.

5. SHA Identifier Contract Verification

Introduced additional checks for the distinction between Git object identifiers and SHA-256 evidence receipts.

The verification fixtures cover valid identifiers, invalid lengths, uppercase values, nonhexadecimal characters, and incorrect input types.

Executed development result: 12 validation cases passed.

The intention is to preserve the identifier-format separation established during the Evidence Ledger's earlier adversarial reviews.

6. The Mutable Fingerprint Counterexample

A real behavioural weakness was reproduced and explicitly documented.

The existing buildAutomaton() function returns a frozen object containing a mutable Uint8Array.

Freezing the containing object does not make the underlying cell array immutable.

A caller can modify the returned cells without updating the stored fingerprint.

In the fixed demonstration:

State	FNV-1a fingerprint
Original stored fingerprint	6d8aa545
Recomputed after changing one cell	eb95c744

The two values differ.

This disproves any proposed invariant claiming that a returned automaton result's fingerprint will necessarily remain consistent after arbitrary caller modification.

The finding is recorded as COUNTEREXAMPLE, not PASS.

v0.7.0 deliberately preserves existing production API behaviour. A subsequent phase will need to define and review the intended state-ownership contract before making any repair.

This is a correctness and API-contract issue, not a demonstrated remote security exploit.

7. Interactive Proof Contracts Dashboard

Introduced a dedicated browser interface at #proof.

Visitors can execute the bounded verification suite, examine per-contract evidence classifications, inspect the mutable-fingerprint counterexample, view outstanding obligations, and export SHA-256 receipts.

The dashboard distinguishes completed bounded observations from unproved mathematical claims.

Lean 4 and SPARK/Ada remain explicitly marked as not executed.

No fabricated mathematical proof status or default passing result is displayed.

8. SHA-256 Verification Receipts

Introduced local evidence export using browser-native WebCrypto.

Each receipt records the protocol version, execution scope, observed contract classifications, fixed-case counts, counterexample fingerprints, outstanding formal verification statuses, and explicit limitations.

The exact UTF-8 JSON payload is hashed using SHA-256.

Receipts are generated locally without telemetry or external submission.

A checksum establishes consistency with the supplied bytes. It does not authenticate the person, application instance, or environment that produced them.

9. Offline Proof Registry Validation

Introduced scripts/check_proof_contracts.py.

The Python standard-library verifier validates the registry's format, expected obligation identities, referenced source targets, risk classifications, baseline revision, and formal verification statuses.

It rejects malformed or incomplete obligations, missing source references, and unjustified claims of completed formal proofs.

The tool provides deterministic evidence-registry validation without additional Python packages.

10. Independent Receipt Verification

Introduced scripts/verify_proof_receipt.py.

The verifier checks strict JSON structure, duplicate properties, non-finite numeric values, exact SHA-256 integrity, expected bounded observations, counterexample data, and formal verification status.

It also rejects resealed receipts containing fabricated results or claims of mathematical proof.

Verification scope: The tool validates receipt integrity and known fixed-fixture consistency.

It does not independently execute JavaScript or certify real-browser execution.

11. Expanded Adversarial Regression Testing

Added 18 Python regression-test methods covering:

• Proof registry consistency.
• Duplicate JSON properties.
• False formal verification status.
• Incorrect source targets.
• Missing referenced source files.
• Altered receipt payloads.
• Fabricated bounded test counts.
• Falsified counterexample classifications.
• Fake Lean proof claims.
• Boolean/integer confusion.
• Non-finite numeric input.
• Invalid evidence envelopes.
• GitHub Pages deployment integration.
• Safe browser presentation.

Four additional JavaScript self-checks cover the bounded verification results, counterexample preservation, proof-status boundaries, and contract ordering.

Development verification: 46/46 JavaScript self-checks passed in an isolated JavaScript environment with a minimal DOM implementation.

The complete Python test suite and graphical browser QA were not independently executed during that development verification. Their results are not asserted here.

12. GitHub Pages Verification Integration

Extended the existing manually triggered GitHub Pages workflow to include the proof-contract registry validation gate.

The deployment package now includ...

INDEPENDENCE v0.6.0 — The Secret Source: AI + Web Tech = Unlimited Potential

RELEASE NOTES

INDEPENDENCE v0.6.0 — THE SECRET SOURCE

AI + WEB TECH = UNLIMITED POTENTIAL.

The Human Has the Vision. The AI Helps Build It. The Tests Keep Everyone Honest.

Release date: 30 October 2026
Organisation: QSOL-IMC
Release type: Feature Release / Human–AI Engineering Methodology
Previous version: v0.5.0
Licence: Apache-2.0

THE REVOLUTION WAS NEVER JUST ABOUT REMOVING DEPENDENCIES.

IT WAS ABOUT WHAT BECOMES POSSIBLE WHEN HUMAN IMAGINATION, AI ASSISTANCE, AND OPEN WEB TECHNOLOGIES WORK TOGETHER.

---

Overview

INDEPENDENCE v0.6.0 reveals THE SECRET SOURCE: the human-directed, AI-assisted GitHub development workflow behind the project's first five releases.

The previous releases demonstrated dependency-free browser engineering, reproducible evidence collection, controlled experimentation, adversarial bug analysis, and deterministic mutation testing.

This release explains how those capabilities were developed through an iterative collaboration between a human maintainer, AI engineering assistants, GitHub, and independently inspectable tests.

The central principle is straightforward:

AI + WEB TECH = UNLIMITED POTENTIAL.

This is an aspirational statement about creative possibilities, not a literal claim that AI has infinite capabilities or guarantees correct software.

The engineering method remains grounded in evidence, explicit constraints, reproducibility, adversarial review, and human decision-making.

Live website: https://qsolkcb.github.io/INDEPENDENCE/

The Secret Source: https://qsolkcb.github.io/INDEPENDENCE/#workflow

Repository: https://github.com/QSOLKCB/INDEPENDENCE

---

New Features

1. The AI–Human GitHub Workflow — AI-HUMAN-WORKFLOW/1

Introduced a new interactive section documenting the project's human–AI engineering methodology.

The workflow assigns distinct responsibilities to human contributors, AI assistants, testing tools, reviewers, and source-control systems.

It demonstrates how AI-assisted development can be structured around clearly defined objectives rather than unconstrained code generation.

2. The Eight-Stage Engineering Loop

The interface introduces eight connected development stages:

1. Human Intent — Define the desired outcome and observable acceptance criteria.
2. Scope Control — Establish what may and may not change.
3. Engineering Invariants — Preserve non-negotiable system properties.
4. Bounded AI Implementation — Produce focused, reviewable code changes.
5. Executable Verification — Run tests and distinguish observations from claims.
6. Adversarial Review — Challenge assumptions, edge cases, and trust boundaries.
7. Fresh HEAD Verification — Review the exact latest Git commit before merging.
8. Human-Controlled Release — Retain human authority over merges, deployments, and publication.

Each interactive stage explains the intended responsibility, a common failure mode, the evidence required, and an example.

3. AI Drift Prevention Framework

Introduced eight practical safeguards designed to reduce common failures in AI-assisted development.

The framework emphasises:

• Explicit, testable objectives.
• Positive and negative scope boundaries.
• Immutable engineering constraints.
• Meaningful positive and adversarial tests.
• Actual execution evidence.
• Independent critical review.
• Fresh commit verification.
• Human-controlled release decisions.

The interactive checklist helps visitors understand the verification responsibilities involved in effective AI collaboration.

Important: Checklist selections are self-reported acknowledgements, not automated security checks or evidence that a repository has passed verification.

4. Bounded Agent Handoff Generator

Introduced a local, interactive prompt builder for preparing engineering tasks for AI coding assistants.

Users define five essential elements:

• Observable goal.
• Permitted implementation scope.
• Explicitly excluded changes.
• Non-negotiable invariants.
• Acceptance and adversarial test requirements.

The generator combines these inputs into a structured implementation contract.

Generated instructions cover repository documentation, minimal changes, regression testing, accurate reporting of tool results, adversarial reviews, Git commit freshness, and human approval gates.

The system rejects missing required goals and oversized inputs.

Generated prompts can be copied directly into an AI coding workflow.

No LLM API call is made. No prompt is submitted, stored remotely, or automatically executed.

5. The Hostile Auditor Protocol

Formalised the project's approach to adversarial review.

Reviewers are encouraged to identify actual defects, reproduce failures, and classify actionable findings by severity:

• P0: Critical.
• P1: High.
• P2: Moderate.
• P3: Minor.

Repairs should be minimal, supported by regression tests, and evaluated against the latest source revision.

A clean review of an earlier commit does not automatically apply to a newer commit.

THE FRESHEST HEAD IS THE SOURCE OF TRUTH.

6. Evidence Versus Assertion

The release explicitly distinguishes an AI assistant's statements from independently inspectable engineering evidence.

Examples include:

• A proposed test is not an executed test.
• A generated patch is not a merged pull request.
• A successful local test is not proof of a successful deployment.
• A valid checksum is not proof of authentic execution.
• An issue-free review is not proof of defect-free software.

This distinction is central to the project's methodology.

7. Five Real GitHub Case Studies

Introduced links to the five original INDEPENDENCE development pull requests.

Version	Case study	Engineering lesson
v0.1.0	The Declaration	Define constraints before implementing
v0.2.0	The Evidence Ledger	Distinguish observations from unknown data
v0.3.0	The Dependency Tribunal	Compare equivalent workloads fairly
v0.4.0	The Gremlin Museum	Validate exact evidence provenance
v0.5.0	The Breeding Laboratory	Test whether tests actually detect defects

These records illustrate the project's development history.

They are not presented as controlled evidence of AI productivity gains, comparative model superiority, or measured reductions in development time.

8. Comprehensive Engineering Guide

Introduced docs/AI-HUMAN-WORKFLOW.md.

The document contains the complete eight-stage workflow, anti-drift engineering practices, bounded task examples, reusable adversarial review prompts, minimal repair instructions, and explicit release authority constraints.

It also explains the limitations of AI-generated code, AI-assisted review, and unverified performance or correctness claims.

9. Expanded Verification

Introduced 16 Python regression-test methods covering the new workflow interface, content constraints, safe prompt generation, deployment integration, and source safety.

Added nine browser self-checks for the workflow catalogue, prompt validation, reproducibility of template content, and checklist semantics.

Development verification: 42/42 JavaScript self-checks passed in an isolated environment using minimal DOM shims.

The interface was also exercised through a simulated browser interaction sequence covering stage navigation, example loading, missing-goal rejection, prompt generation, clipboard copying, and stale-prompt invalidation.

Full Python-suite execution and graphical browser testing were not independently established by these development checks.

10. Zero Additional Application Dependencies

The new interface is implemented using first-party HTML, CSS, and JavaScript.

The existing manually triggered GitHub Pages workflow packages the new assets and retains the Python standard-library regression tests and static audit.

No npm dependencies, third-party frontend frameworks, external AI APIs, tracking services, or application build pipeline were introduced.

---

Reproducibility

Run the complete Python regression suite:

python3 -m unittest discover -s tests -v

Run the repository audit:

python3 scripts/audit.py --json

Start the website locally:

python3 -m http.server 8000

Open:

http://localhost:8000/#workflow

Inspect the interactive workflow, generate a bounded implementation prompt, and run the website's browser self-tests.

All new interface functionality operates locally without external application packages.

---

Engineering Governance

v0.6.0 extends the repository's documented invariants to cover responsible AI-assisted engineering.

Key requirements include:

• AI-generated claims must not substitute for actual tool evidence.
• Generated prompts must preserve explicit human authority.
• User-entered prompts must never be silently transmitted to external services.
• Scope expansion requires human approval.
• Tests must be reported accurately, including skipped or unavailable checks.
• Adversarial findings must be addressed without unnecessary architectural changes.
• Review conclusions must be tied to the latest applicable commit.
• The project's aspirational claims must remain distinguishable from verified measurements.

Updated documentation:

• docs/AI-HUMAN-WORKFLOW.md
• docs/INVARIANTS.md
• docs/EVIDENCE.md
• docs/ROADMAP.md
• README.md

---

👹 GREMLIN NOTES™ — v0.6.0

The Gremlins have discovered AI-assisted software development. Naturally, they've started submitting pull requests.

GREMLIN-009 — The Scope Creep Goblin

Classification: Engineering Process Failure Mode
Severity: Preventative / Educational
Status: GUARDRAI...

INDEPENDENCE v0.5.0 — The Gremlin Breeding Laboratory 👹

#RELEASE NOTES#

INDEPENDENCE v0.5.0 — THE GREMLIN BREEDING LABORATORY 👹

Breed the Bugs. Test the Tests.

Release date: 30 October 2026
Organisation: QSOL-IMC
Release type: Feature Release / Mutation Testing Research
Previous version: v0.4.0
Licence: Apache-2.0

THE GREMLINS HAVE ESCAPED THE MUSEUM.

THIS TIME, WE BRED THEM ON PURPOSE.

Overview

INDEPENDENCE v0.5.0 introduces THE GREMLIN BREEDING LABORATORY, a deterministic mutation-testing environment designed to investigate a fundamental question in software engineering:

Do our tests actually detect defects, or do they merely pass?

Following the Declaration of Independence, Evidence Ledger, Dependency Tribunal, and Gremlin Museum, this release advances the project's evidence-first engineering philosophy by deliberately introducing harmless behavioural defects into isolated functions and measuring whether regression tests identify them.

The laboratory includes 15 predefined software mutants, five independently testable function families, deterministic execution ordering, two test-suite configurations, and reproducible evidence receipts.

Everything operates locally using vanilla HTML, CSS, JavaScript, and the Python standard library.

No npm. No Node.js build pipeline. No Docker. No Kubernetes. No third-party application packages.

Live laboratory: https://qsolkcb.github.io/INDEPENDENCE/#breeding

Repository: https://github.com/QSOLKCB/INDEPENDENCE

---

New Features

1. The Gremlin Breeding Laboratory — GREMLIN-BREEDING/1

Introduced a dedicated interactive mutation-testing laboratory within the INDEPENDENCE website.

Unlike the Gremlin Museum, which preserves previously identified defects, the Breeding Laboratory deliberately introduces controlled behavioural changes to evaluate test effectiveness.

Users can select a deterministic seed, choose a test-suite strength, execute the mutation experiments, inspect individual results, and export verification receipts.

Every mutation is predefined and operates exclusively on isolated, first-party functions and inert test data.

No application source files are modified or dynamically executed.

2. Fifteen Deliberately Bred Gremlins

Introduced five mutation-testing targets, each containing three intentionally defective implementations.

Target	Mutants	Research focus
SHA-256 Receipt Validation	3	Identifier and boundary validation
HTML Output Encoding	3	Missing character escaping
Finite JSON Validation	3	Numeric and recursive validation
Repository Path Scoping	3	Dependency-directory detection
Remote Module Import Detection	3	Incomplete static import recognition
Total	15	Five independent target families

The mutations include relaxed validation boundaries, missing escaping rules, incomplete recursive checks, incorrect filesystem scope, and omitted JavaScript import forms.

Every mutant has at least one known divergence from its corresponding reference implementation.

3. Two Test-Suite Configurations

Introduced two selectable testing configurations to demonstrate how test coverage influences defect detection.

Smoke Suite — Deliberately Incomplete

A minimal set of test cases intended to demonstrate how software defects can escape insufficient regression coverage.

Full Fixture Suite — Expanded Verification

An expanded test collection designed to detect the known behavioural differences introduced by all 15 predefined mutants.

The laboratory produces actual results from executing the fixed functions against the selected tests.

4. Mutation Detection Results

The frozen v0.5.0 fixture catalogue produced the following deterministic outcomes:

Metric	Smoke Suite	Full Fixture Suite
Mutants evaluated	15	15
Mutants killed	2	15
Mutants survived	13	0
Mutation score	13.3%	100%

A mutant is classified as KILLED when at least one selected test detects a difference from the expected behaviour.

A mutant SURVIVES when the selected test suite does not detect its known behavioural defect.

These results describe only the curated mutation catalogue.

A 100% score does not demonstrate complete application correctness, repository-wide test coverage, or the absence of vulnerabilities.

5. Baseline Oracle Verification

Introduced mandatory reference-behaviour verification before mutation testing begins.

The engine validates all 26 baseline oracle cases, regardless of the selected test suite.

Mutation testing cannot proceed successfully if a baseline produces an unexpected result.

Every mutant must also demonstrate at least one known difference from its reference implementation.

Equivalent or unproven mutants cause the experiment to fail rather than inflate or distort the mutation score.

CORRECTNESS BEFORE CLASSIFICATION.

6. Deterministic Mutation Ordering

Implemented reproducible mutation ordering using seeded xorshift32 and Fisher–Yates shuffling.

Features include:

• Configurable nonzero 32-bit seed.
• Stable mutation identifiers.
• Reproducible execution order.
• Fixed input fixtures.
• Explicit divergence witnesses.
• Deterministic kill/survival classifications.
• Reproducible mutation scores.

Changing the seed changes the evaluation order without changing the predefined behavioural differences or expected total scores.

7. Interactive Mutation Results

Introduced a responsive browser dashboard displaying:

• Mutation target and identifier.
• Mutation operator description.
• KILLED or SURVIVED classification.
• Selected tests that detected the mutation.
• Known divergence witnesses.
• Total mutants evaluated.
• Total killed and surviving mutants.
• Mutation detection score.

The interface distinguishes actual detected failures from known defects the selected tests missed.

All output is presented using native DOM text rendering.

No external visualisation library or application framework is required.

8. SHA-256 Mutation Evidence Receipts

Introduced downloadable evidence receipts using native browser WebCrypto.

Each receipt includes the experimental protocol, seed, suite selection, baseline verification count, deterministic mutation order, mutant identifiers, selected-suite failures, known divergence witnesses, classification results, aggregate mutation score, and explicit limitations.

The report's exact UTF-8 JSON payload is hashed using SHA-256.

Receipts are generated locally and are not uploaded to an external service.

The hash supports payload-integrity verification but does not authenticate the person or environment that produced the report.

9. Independent Python Receipt Verification

Introduced scripts/verify_breeding.py, a Python standard-library-only verifier.

The verifier independently encodes the expected mutation catalogue and validates:

• Exact SHA-256 payload integrity.
• Protocol and schema identities.
• Valid experimental parameters.
• Recognised mutation operators.
• Deterministic seeded ordering.
• Expected divergence witnesses.
• Correct KILLED/SURVIVED classifications.
• Accurate aggregate mutation scores.
• Explicit evidence limitations.
• Strict JSON structure and numeric validity.

The verifier rejects altered receipts even when the manipulated JSON has been resealed with a valid SHA-256 digest.

A valid receipt demonstrates consistency with the published fixed-fixture protocol, not independently authenticated browser execution.

10. Expanded Regression Testing

Added 18 Python regression-test methods covering valid smoke/full receipts, deterministic ordering, invalid seeds, unsupported suites, receipt tampering, forged classifications, altered mutation scores, fabricated witnesses, duplicate JSON properties, non-finite numeric values, and deployment invariants.

Eight additional browser self-checks cover mutation outcomes, deterministic replay, mutation witnesses, configuration validation, and catalogue integrity.

Development verification: 33/33 JavaScript self-checks passed in an isolated JavaScript environment using a minimal DOM model.

The complete Python test suite was committed for independent execution through the GitHub Pages deployment workflow. No independently observed full-suite passing result is asserted here.

11. GitHub Pages Deployment Integration

Extended the existing manually triggered GitHub Pages workflow to include:

• breeding/core.js
• breeding/ui.js
• breeding/breeding.css

The source audit now includes the new web assets, and deployment retains the project's existing Python verification requirements.

No package installation, application bundling, or container build is required.

---

Reproducibility

Run the complete Python regression suite:

python3 -m unittest discover -s tests -v

Run the repository static audit:

python3 scripts/audit.py --json

Start a local development server:

python3 -m http.server 8000

Open:

http://localhost:8000/#breeding

Select the Smoke or Full Fixture Suite, execute the experiment, and download the resulting SHA-256 evidence receipt.

Verify an exported receipt:

python3 scripts/verify_breeding.py gremlin-breeding-<hash>.json --json

The commands require Python's standard library only.

---

Engineering Governance

v0.5.0 introduces additional formal engineering invariants covering mutation safety, deterministic execution, evidence integrity, and scientific scope.

The laboratory must not modify deployed source files, execute dynamically generated code, install third-party packages, interact with external systems, or interpret inert test strings as executable instructions.

Every mutant re...

INDEPENDENCE v0.4.0 — THE GREMLIN MUSEUM 👹

#RELEASE NOTES#

INDEPENDENCE v0.4.0 — THE GREMLIN MUSEUM 👹

The Bugs Are in Captivity.

Release date: 30 October 2026
Organisation: QSOL-IMC
Release type: Feature Release / Security Research Exhibits
Previous version: v0.3.0
Licence: Apache-2.0

THIS IS NOT WAR. THIS IS A DIVORCE.

AND WE'RE TAKING CUSTODY OF THE BUGS.

Overview

INDEPENDENCE v0.4.0 introduces THE GREMLIN MUSEUM, an interactive, dependency-free archive of reproducible software failure modes, engineering mistakes, and their corrections.

Following the original Declaration of Independence, the Software Independence Evidence Ledger, and the Dependency Tribunal, this release establishes a permanent home for the bugs discovered during adversarial software review.

Rather than merely fixing defects and forgetting them, the Gremlin Museum preserves bounded reproductions, expected failure behaviours, corrected implementations, provenance records, and deterministic assertions.

Each exhibit demonstrates an engineering lesson through independently inspectable source code.

Five exhibits. Eighteen fixture assertions. Zero additional third-party packages.

Live Museum: https://qsolkcb.github.io/INDEPENDENCE/#museum

Repository: https://github.com/QSOLKCB/INDEPENDENCE

---

New Features

1. The Gremlin Museum — GREMLIN-MUSEUM/1

Introduced a dedicated interactive museum integrated into the existing INDEPENDENCE website.

Visitors can:

• Browse five individual software failure exhibits.
• Examine historical or illustrative provenance.
• Inspect inert reproduction inputs.
• Compare legacy behaviour with corrected behaviour.
• Execute deterministic assertions.
• Run every exhibit in a single operation.
• Generate downloadable SHA-256 evidence receipts.
• Independently verify receipts using Python.

The interface is implemented entirely using native browser technologies.

No package manager, build system, container runtime, external JavaScript library, or third-party execution service is required.

2. Five Captive Gremlins

EXHIBIT 001 — The Side-Effect Stowaway

Static Audit Bypass — Historical INDEPENDENCE Finding

Reproduces the v0.1.0 defect where a remote JavaScript side-effect import escaped a restricted static dependency scanner.

Demonstrates the original incomplete detection rule and the corrected handling of side-effect imports.

Lesson: A security or dependency rule is only as comprehensive as the syntax it recognises.

EXHIBIT 002 — The Phantom Dependency

Audit False Positive — Historical INDEPENDENCE Finding

Demonstrates how inspecting absolute filesystem ancestry can create false dependency findings.

A repository located beneath an unrelated .venv directory could incorrectly appear to contain vendored dependencies.

The corrected implementation restricts inspection to repository-relative paths.

Lesson: Evidence must remain within its declared scope.

EXHIBIT 003 — The SHA Identity Crisis

Evidence Validation — Historical INDEPENDENCE Finding

Preserves the v0.2.0 defect in which a 40-character Git object identifier validator incorrectly rejected valid 64-character SHA-256 evidence receipts.

Demonstrates separate validation rules for distinct identifier types.

Lesson: Similar-looking identifiers are not interchangeable contracts.

EXHIBIT 004 — The Infinity Smuggler

JSON Numeric Correctness — Illustrative Example

Demonstrates how a JSON numeric literal such as 1e999 can be parsed into a non-finite floating-point value.

Shows how subsequent JSON serialization can alter the representation and how explicit finite-number validation detects the problem.

Lesson: Syntactically valid input does not guarantee semantically valid data.

This is a general illustrative case, not a reported vulnerability in INDEPENDENCE.

EXHIBIT 005 — The Markup Masquerade

HTML Output Encoding — Illustrative Example

Demonstrates the distinction between unsafe HTML string construction and correctly encoded untrusted text.

All example strings are displayed as inert text. No browser injection payload is executed.

Lesson: Untrusted input must not silently become executable or interpreted markup.

This is a general illustrative case, not a reported vulnerability in INDEPENDENCE.

3. Deterministic Exhibit Execution

Introduced museum/core.js, containing the fixed exhibit definitions, reproduction logic, corrected behaviours, and assertions.

All exhibits use bounded, predefined inputs.

The museum enforces deterministic results and rejects invalid exhibit identifiers.

Verification performed during development: 18/18 exhibit assertions passed.

These checks demonstrate the specific reproduced behaviours. They are not evidence that the entire application is free of vulnerabilities.

4. Secure Browser Presentation

Introduced museum/ui.js and museum/museum.css.

The interface presents potentially dangerous-looking inputs using safe text rendering rather than HTML interpretation.

Design safeguards include:

• No execution of specimen payloads.
• No dynamic evaluation of supplied code.
• No remote module imports.
• No third-party network requests.
• No browser telemetry.
• No real filesystem or credential access.
• No arbitrary external attack targets.

The Museum is an educational and regression-testing environment, not an exploitation platform.

5. SHA-256 Museum Evidence Receipts

Introduced downloadable evidence receipts using browser-native WebCrypto.

Each passing museum-wide run records:

• Protocol and schema version.
• Exhibit identifiers and classifications.
• Fixed reproduction inputs.
• Observed legacy behaviours.
• Corrected behaviours.
• Deterministic assertion results.
• Per-exhibit provenance.
• Source references.
• Explicit experimental limitations.

The exact UTF-8 payload is hashed using SHA-256.

Failed or incomplete exhibit checks prevent evidence export.

Receipts support reproducibility and integrity checking, without claiming independent authentication of their creator or execution environment.

6. Offline Python Evidence Verification

Introduced scripts/verify_museum.py, a Python standard-library-only evidence verifier.

Capabilities include:

• Strict JSON parsing.
• Duplicate-property rejection.
• Non-finite numeric rejection.
• Exact SHA-256 payload verification.
• Fixed exhibit identity validation.
• Expected reproduction-output verification.
• Corrected-output verification.
• Assertion-count verification.
• Exact provenance and source validation.
• Explicit limitations checking.

The verifier rejects inconsistent or tampered receipts, including receipts that have been recomputed with a valid SHA-256 hash but contain incorrect fixed-fixture claims.

7. Expanded Regression Testing

Introduced tests/test_museum.py, including 15 Museum-specific test methods following adversarial review hardening.

Coverage includes:

• Valid fixed-fixture receipts.
• Deterministic receipt generation.
• Modified payload detection.
• Falsified corrected-output rejection.
• False passing-status rejection.
• Missing provenance detection.
• Malformed JSON handling.
• Invalid receipt structure.
• Offline file verification.
• Static Pages integration.
• Inert browser display requirements.
• Historical attribution forgery.
• Repository URL prefix collisions.
• Swapped legitimate review references.
• Illustrative examples falsely claiming historical origins.

The existing browser self-test suite was expanded to 25 checks.

Development verification: 25/25 browser checks passed in an isolated JavaScript environment with a minimal DOM model.

The complete Python suite was committed for execution by the deployment workflow. These release notes do not assert an independently observed full-suite result.

8. GitHub Pages Deployment Integration

Extended the existing manually triggered GitHub Pages workflow to include the Museum's first-party JavaScript and CSS files.

The deployment process retains the project's standard-library verification and static audit stages.

All previous website features remain available:

• Declaration of Independence.
• Deterministic Computing Laboratory.
• Software Independence Evidence Ledger.
• Dependency Tribunal.
• Dependency Complexity Explorer.

No external application packages were introduced.

---

Reproducibility

Run the full Python regression suite:

python3 -m unittest discover -s tests -v

Run the repository's static audit:

python3 scripts/audit.py --json

Start a local server:

python3 -m http.server 8000

Open:

http://localhost:8000/#museum

Select an exhibit, reproduce its behaviour, or run all five specimens.

After generating a SHA-256 receipt, verify it locally:

python3 scripts/verify_museum.py /path/to/gremlin-museum-<hash>.json --json

No pip installation, npm package, Docker container, or Kubernetes orchestration is required.

---

Engineering Governance

v0.4.0 extends the INDEPENDENCE engineering invariants with additional requirements for security research exhibits.

Every exhibit must distinguish historical evidence from illustrative examples, use bounded local inputs, provide meaningful regression assertions, and preserve explicit provenance.

Potentially unsafe examples must remain inert.

Failed checks must prevent evidence export.

SHA-256 receipt validity must not be misrepresented as proof of authorship, exploitability, complete application security, or the absence of undiscovered defects.

Updated documentation includes:

• docs/MUSEUM.md — Museum protocol and evidence limits.
• docs/INVARIANTS.md — Safe-executio...