Skip to content

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

Latest
Latest

Choose a tag to compare

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

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

Assets 2
Loading