Badge interpretation: The Verify badge reports live automatic CI status. Pages deployment and published-byte audit are manual operations; their neutral badges link to workflow histories, not continuous website-health status. Public-byte verification completed successfully in manual observation run 41137612537, using the preserved manifest from deployment run 41136291743 (deployed revision 0dbcf0fced7317a1117d0c3bdda1951959eb7c2b). The exact manifest was verified and 35/35 HTTP-observable assets matched their expected SHA-256 hashes on the first attempt. The recorded status is REMOTE_HTTP_ASSETS_MATCHED_MARKER_UNOBSERVED: .nojekyll remains required and checksummed in the staged manifest but was not independently fetched over HTTP. The earlier run 41113714704 404 is historical, not the latest verification result. This is a point-in-time byte observation of that deployed revision, not a guarantee of ongoing availability or proof that later main commits are live.
Project milestone: v1.1.0 formalisation complete. GitHub release · Full research report · Published Zenodo dataset. Historical evidence and proof boundaries remain explicitly preserved.
We hereby declare our independence from the Modern Software Industry.
We reject the proposition that a simple application requires a container, a container orchestrator, a package manager, a dependency resolver, seventeen YAML files, and an army of consultants to deploy.
We reject the idea that software engineering is measured by the number of frameworks one can assemble.
We reject complexity masquerading as sophistication.
Our grievances are numerous:
- Kubernetes: We aren't deploying the fucking space shuttle.
- Docker: Not every executable needs its own shipping container.
- Node.js: JavaScript does not need to run the entire civilisation.
- npm: We would prefer not to download half the internet to compile a button.
- Dependency hell: Your supply chain is not our responsibility.
- Framework churn: Yesterday's revolutionary solution is tomorrow's deprecated liability.
We welcome AI as an instrument of independent security research, exposing vulnerabilities, auditing assumptions, and demonstrating the consequences of unnecessary complexity through reproducible evidence and responsible disclosure.
We do not claim that dependency-free software is invulnerable. We claim that every dependency introduces another relationship that must be understood, trusted, maintained, and defended.
Our principles:
- Correctness outranks convenience.
- Simplicity outranks fashion.
- Auditability outranks abstraction.
- Portability outranks platform lock-in.
- Reproducibility outranks promises.
- Zero dependencies wherever technically feasible.
- No unnecessary infrastructure.
- No mandatory cloud services.
- No framework shall become our master.
We build software that can stand on its own.
99 PUBLIC REPOSITORIES. ZERO DEPENDENCIES. ZERO FUCKS GIVEN.
Signed,
QSOL-IMC
Independent Software Sovereignty Initiative
WE DID NOT LEAVE SOFTWARE ENGINEERING. SOFTWARE ENGINEERING LEFT US.
This is not War, This is a Divorce.
This Isn't War, This Is Pest Control
The delivered project comprises the first-party, dependency-free static website; interactive automaton and dependency experiments; the public evidence ledger; seeded counterexamples; versioned proof contracts; executable conformance checks; dual-engine browser verification; and a research-grade formalisation with immutable evidence archives. The v1.1.0 GitHub release and Zenodo dataset represent this completed research milestone, not a claim of universal software correctness.
Research citation: Slade, T. (2026). INDEPENDENCE v1.1.0: Formal Models, Bounded Conformance, and Evidentiary Trust Boundaries (Version v1.1.0) [Dataset]. Zenodo. doi:10.5281/zenodo.23816739.
| Verification class | Recorded result | What it establishes |
|---|---|---|
| Lean 4.35.0 | 6 kernel-checked theorem statements | Width-four mathematical model properties |
| SPARK/GNATprove | 10 discharged verification conditions | Scoped Ada reference contracts |
| Ada CLI / production JavaScript | 4,096 width-four comparisons each; 10 additional invalid Ada cases | Finite executable conformance only |
| Rocq 9.2.0 | 15 kernel-checked theorem/example obligations; 15 closed assumption audits | Arbitrary-finite-width mathematical model properties |
| Chromium / Firefox | 92 recorded passing historical PR-run assertions | Specific browser observations, not live deployment attestation |
| Original proof archives | 2 byte-preserved tarballs and 13 internal checksum entries | File integrity, not independent compiler attestation |
| v1.1.0 post-merge CI | 377 passing Python tests; integrity, browser and staged-site checks passed | A successful versioned CI run, not permanent certification |
Reproduce the archived release checks (Python 3 standard library; developer-only compiler/browser tools are optional):
git checkout v1.1.0
python3 -m unittest discover -s tests -v
python3 scripts/verify_formalisation_archive.py --output formalisation-integrity.json
python3 scripts/verify_browser_archive.py
python3 scripts/check_rocq_semantics.py --output rocq-static.json
To actually execute the Rocq proof obligations, activate a pinned Rocq 9.2.0 toolchain and run python3 scripts/check_rocq_semantics.py --require-rocq --output rocq-executed.json. CI's ordinary static Rocq stage records NOT_RUN unless a real compiler is invoked separately. Existing archived local execution receipts distinguish this from CI source inspection.
Research boundary: Neither the Lean/Rocq models nor finite runtime comparisons formally refine the production JavaScript implementation. The original receipts do not authenticate the developer machine, certify WCAG compliance or prove all frameworks unnecessary. The website remains zero-package at runtime; GitHub Pages deployment and published-byte verification are separately manual workflows.
Evidence and reading: Formalisation report · Original archives and checksum manifest · Proof limitations · Versioned GitHub release.
The historical milestone sections below retain release-time status language. An earlier NOT_RUN does not erase a later, separately archived proof execution.
The manifesto now has a working, no-build interactive demonstration on GitHub Pages:
https://qsolkcb.github.io/INDEPENDENCE/
- Deterministic, seeded elementary cellular automata (Rules 30, 90, 110 and 184), native Canvas 2D, and a replay fingerprint.
- Browser tests (including independently known vectors), executed only when requested.
- A clearly-labelled synthetic dependency-tree thought experiment.
- Zero third-party runtime packages or externally hosted executable browser assets.
- Python 3 standard-library dependency and resource audit, plus stdlib unittest tests.
No npm install, pip install, Docker pull, container orchestration, bundler, or third-party service is needed to build, test, or serve it:
python3 -m unittest discover -s tests -v
python3 scripts/audit.py --json
python3 -m http.server 8000
Open http://localhost:8000/ for local development. The browser uses relative ECMAScript module imports and therefore should be served over HTTP.
See docs/INVARIANTS.md, docs/EVIDENCE.md, and docs/ROADMAP.md. The scope and limitations are intentional: zero third-party packages is not zero platform dependencies, not an all-repositories audit, and not proof of invulnerability.
The revolution will not be containerised.
Browse the public evidence ledger. Site changes are published separately through a manual Pages deployment; successful CI does not itself deploy the website.
The public catalogue at QSOL-IMC provides curated categories. QSOL-CONTEXT informs the provenance philosophy but is a private repository and is neither queried by the collector nor imported into this public dataset. The ledger never publishes personal context records.
This is a filename-signal inventory, not a declaration that every repo is package-free. It distinguishes observed manifests, inspected trees without known manifests, truncated trees and failed scans. Counts come from the packaged JSON, not hard-coded website constants.
Regenerate using Python's standard library (GitHub REST network required):
GITHUB_TOKEN=... python3 scripts/build_ledger.py --as-of 2026-10-30 --output ledger/data.json
The existing manually triggered Pages workflow now refreshes the snapshot before testing and packaging the site. Visitors load static JSON from GitHub Pages; their browsers do not query the GitHub API. See ledger methodology for evidence scope, unknown states, failure handling, and receipt hashing.
Open the experiment. Site updates require the manual Pages deployment.
DOM-TRIBUNAL/1 compares direct DOM replacement with a tiny first-party keyed adapter, both performing identical seeded list render, update and reorder operations on detached DOM elements. The latter is illustrative, NOT an actual React/Vue/Svelte or third-party framework benchmark. No default winning figures are provided: results only exist when the visitor explicitly runs the workload.
Every trial has matching output assertions, alternating execution order and warmups. The browser reports paired medians, seeded bootstrap 95% percentile intervals and first-party adapter source byte counts. SHA-256 receipts are downloadable locally, not sent to QSOL-IMC.
Verify an exported file with Python stdlib:
python3 scripts/verify_tribunal.py /path/to/tribunal-receipt.json --json
Verification checks exact UTF-8 payload integrity and internal sample/summary consistency, not the authenticity of measured timings. Read the protocol for scope and limitations.
Enter the Gremlin Museum after merge and manual Pages deployment.
Five safe, first-party, fixed-input demonstrations of software failure modes, each with a legacy observation, bounded corrective behaviour and reproducible assertions. Three reflect historic INDEPENDENCE review findings; two are explicitly marked illustrative. Nothing malicious is executed: all code-like inputs are inert strings shown with textContent. No external host, upload, installation, framework or package manager is needed.
Run a specimen individually or all five. For a passing full run, download an exact-payload SHA-256 JSON receipt and verify it offline:
python3 scripts/verify_museum.py /path/to/gremlin-museum-xxxxxxxxxxxx.json --json
The verifier checks integrity and fixed observations, not authorship, real-world exploitability or the absence of undiscovered vulnerabilities. Read docs/MUSEUM.md.
Visit the mutation-testing laboratory after merging and manually deploying.
GREMLIN-BREEDING/1 creates 15 harmless, predeclared pure-function mutants across five fixed targets. All 26 baseline oracle cases must pass. Each mutant must have a known divergent witness. A deliberately incomplete smoke suite misses several mutants; the expanded fixture suite catches them. This is a laboratory for testing the tests, not arbitrary mutation of repository files or a repository-wide security score.
Runs are deterministic by seed and show killed/survived classifications and failing test IDs. Download a local SHA-256 evidence receipt and verify it using Python's standard library:
python3 scripts/verify_breeding.py /path/to/gremlin-breeding-xxxxxxxxxxxx.json --json
The verifier pins the catalogue, outcomes and seeded order but does not attest genuine browser execution. See docs/BREEDING.md for methodology and limits.
Explore the AI–Human GitHub Workflow after merging and manually deploying.
The previously unspoken engine behind this repository is a human-directed loop: intent → bounded scope → invariants → AI-assisted implementation → real tests → adversarial review → fresh HEAD SHA → human-authorised merge and release.
The slogan is aspirational, not a guarantee: models can be wrong, drift, miss edge cases and misreport unverified work. Practical guidance shows how to improve reliability by freezing scope, naming forbidden changes, checking provenance and tool outputs, testing failure cases, challenging patches with a hostile reviewer and reviewing the actual latest commit before merging.
The new static browser guide includes eight selectable workflow stages, eight self-reported drift safeguards, public links to five merged PR case studies, and a local copyable agent-handoff prompt generator. It does not call an AI, send prompts to a server, track activity or claim to check your repository. Only browser-standard code and Python stdlib tests are used.
Full method and copyable adversarial-review/fix prompts: docs/AI-HUMAN-WORKFLOW.md.
Run the proof-contract dashboard after merging and manually publishing.
The machine-readable proof registry declares eight obligations. Every one remains NOT_PROVED formally. The browser executes bounded checks against the real first-party source: 130,560 elementary cellular-automaton transitions (all rules across all 1..8-wide binary rows), 918,016 output-cell comparisons, BigInt geometric-sum fixtures, seeded replay and SHA validation. A fifth observation is a real COUNTEREXAMPLE: the frozen automaton wrapper holds mutable cells, so a returned fingerprint can become stale.
Reproduce the registry check and verify a downloaded receipt with Python stdlib:
python3 scripts/check_proof_contracts.py --json
python3 scripts/verify_proof_receipt.py proof-contracts-<hash>.json --json
At the v0.7.0 milestone no Lean or SPARK proof had yet been constructed or discharged. Later model proofs and SPARK reference conditions were reported and preserved separately for the v1.1.0 archive. Hash verification alone never attests execution. Proof tools remain optional developer-only components. Read docs/PROOF-CONTRACTS.md and the formal programme through v1.1.0 Zenodo.
Introduces development-only SPARK/Ada source under formal/spark/ for a narrow finite reference: rectangular addressing and decoding, GF(2) parity arithmetic, mod-3 phase addition and validated in-range, distinct endpoint transitions. Canonical semantics are versioned at formal/spec/kernel-v1.json.
The kernel specifies preconditions and postconditions. At the original v0.7.1 implementation milestone, GNATprove was unavailable and the contracts were correctly reported NOT_RUN; later scoped local proof evidence is documented below. The CLI input boundary is not formally analyzed. There is no claim that this reference verifies existing Python or JavaScript.
python3 scripts/check_spark_reference.py
python3 scripts/check_spark_reference.py --prove --output spark-evidence.json
python3 scripts/check_spark_reference.py --require-proved
The strict command fails unless actual GNATprove analysis reports discharged obligations. GNAT/GNATprove are optional development-only tools, never site runtime dependencies. See docs/SPARK-REFERENCE.md.
A separate, versioned conformance layer tests a newly written independent Python reference against the same kernel-v1 semantics used by the v0.7.1 SPARK/Ada kernel. An Ada proof does not automatically prove Python correct.
The bridge executes 8,881 valid finite-domain cases and 16 invalid inputs against an independently coded Python oracle. It can optionally compare real Ada CLI output for a deterministic, operation-covering sample, or the whole domain if Ada tools are available.
python3 scripts/run_kernel_conformance.py --receipt conformance.json
python3 scripts/verify_kernel_receipt.py conformance.json
To compare an actually built Ada CLI, supply the executable:
python3 scripts/run_kernel_conformance.py --ada-cli formal/spark/bin/reference_cli --ada-cases 128 --receipt ada-comparison.json
The receipt distinctly reports Lean mathematical proofs, Ada contract verification, tested Python conformance, Ada CLI comparisons and unresolved obligations. In the original v0.7.2 authoring environment, GNAT/GNATprove were unavailable and those stages were recorded NOT_RUN; later historical local execution evidence is preserved in the following sections. Matching a supplied executable is explicitly UNATTESTED; neither Python application-wide correctness nor production JavaScript is established. Details: docs/PROOF-CONFORMANCE.md.
The first development-only Lean 4 proof source is in formal/lean/FiniteFoundation.lean, pinned to Lean 4.35.0 in lean-toolchain. It defines 13 proposed theorem statements and accompanying proof terms for an explicit CRT (2,3) bijection, Boolean GF(2) identities, cyclic modulo-3 phase identities, and strict degree-lex order properties on natural exponent pairs.
Historical authoring status: Lean was unavailable during the first v0.7.3 implementation, so the 13 theorem candidates were recorded NOT_RUN. Subsequent user-reported Lean 4.35.0 proof execution is described in the preserved-evidence section below. Static source inspection still cannot establish kernel checking. No Lean proof implies correctness of production Ada, Python or JavaScript.
To run actual Lean checks and a fail-closed axiom audit with a trusted Lean installation:
python3 scripts/check_lean_foundation.py --require-checked --output lean-evidence.json
For source-level validation without Lean:
python3 scripts/check_lean_foundation.py
General CRT, full monomial well-foundedness/totality, graph adjacency and model-to-code conformance remain open. See docs/LEAN-FOUNDATION.md for the exact scope, assumptions and reproducibility instructions.
The user's successful local Lean 4.35.0 verification output (13/13 theorem audits; --trust=0; reported 169/169 Python tests) has been archived and retained alongside the completed v1.1.0 research record at formal/evidence/lean/v0.7.3. The archive includes lean-evidence.json, its manifest, a copy of the historical Lean source and lean-toolchain, and a provenance explanation.
Source commit: 68351489e8bbbb879efdcac19d02869124fcf724 (merged PR #11). Provenance qualification: the report was recovered intact from the user-shared terminal transcript, not independently byte-matched against an upload of the original lean-evidence.json; the local execution was not independently attested. Archive hashes establish internal consistency, not authorship or Ada/Python/JS verification.
python3 scripts/verify_lean_evidence_archive.py
This offline integrity gate does not itself run Lean. Re-run the pinned compiler separately to reproduce the proof.
The user reported an actual GNATprove FSF 16.1.0 execution against PR #13 HEAD 9900e57f2283c534815657dd6c079d0e966715f4, with all 21 kernel checks proved, exit code 0 and a passing 186/186 Python regression suite. The exact analyzed Ada source/project SHA-256 values and the copied proof-output digest are preserved in formal/evidence/spark/pr13 for the v1.1.0 research record.
This receipt was reconstructed from a user-pasted terminal report, not the unattached original spark-evidence.json bytes or an independently authenticated run. It describes GNATprove's scoped Ada-reference checks; the Ada CLI and actual Python/Ada differential execution remain separate obligations.
python3 scripts/verify_spark_evidence_archive.py
A new offline developer-only command compiles the pinned PR #13 Ada source snapshot in a fresh temporary build directory, then compares the executable against the independent Python oracle over either 150 sample/invalid inputs or the full 8,903-process finite set. It records compiler versions, source and executable SHA-256 hashes, raw build output and a fail-closed self-consistency receipt. No Ada runtime success is claimed until the command really runs on a GNAT-equipped machine.
export PATH="$HOME/opt/edgewalk-spark-toolchain/bin:$PATH"
python3 scripts/build_and_compare_ada.py --output ada-runtime-evidence.json
python3 scripts/verify_ada_runtime_evidence.py ada-runtime-evidence.jsonSee docs/ADA-RUNTIME-EXECUTION.md. The archive verifier does not independently authenticate build execution, and Ada/Lean proofs do not establish production Python/JavaScript correctness.
The user uploaded the original ZIP and checksum following the actual Ada/Python runs. Both original JSON runtime receipts are now preserved byte-identically under formal/evidence/ada-runtime/v0.7.4, with 150-case and full 8,903-case results, their exact file SHA-256, Git blob IDs, reported Ada binary digest, historical Git revisions and a reproducibility/provenance manifest. The uploaded ZIP checksum is 429b946d083c2b0562450704f924eb3370e5c9a9c62eb81ef5ac90d41a5e2256; the ZIP itself is not stored in this Git repository. The separately uploaded GNATprove JSON matches the already archived SPARK report byte-for-byte; the Lean ZIP member remains the previously transcript-reconstructed archive file.
python3 scripts/verify_original_ada_evidence.py
File-byte identity and internal consistency are now established; independent authentication of local compiler execution is not asserted. The full set is finite, not a general formal proof of CLI or application behaviour.
The deployed first-party Property Lab generates up to 512 replayable seeded automaton cases, compares the real transition implementation against an independent oracle, exposes a deliberately injected boundary-condition mutant, and shrinks a failing 8-cell witness to its canonical 1-cell reproducer. It also reproduces the existing real mutable Uint8Array/fingerprint counterexample and provides an opt-in defensive-copy snapshot API without changing the legacy automaton interface. The browser exports exact SHA-256 property receipts, independently checked for consistency with Python stdlib:
python3 -m unittest discover -s tests -v
python3 scripts/audit.py --json
python3 scripts/verify_property_receipt.py /path/to/property-lab-<hash>.jsonThe injected mutant is intentionally faulty, not a discovered production defect. Finite tests, self-hashed receipts and opt-in ownership guards establish no universal proof or independent browser execution attestation. See docs/PROPERTY-LAB.md.
v0.9 introduces a distinct AUTOMATA4/1 four-cell elementary automaton reference, specifying fixed-zero boundaries and all 256 rule masks over 16 possible input rows (4,096 deterministic vectors). It adds six new Lean 4 theorem candidates, an exact standalone SPARK-mode Ada reference and developer CLI, independent Python finite oracle, and a developer-only JavaScript check against the actual first-party evolve function. Unlike the earlier 13 Lean and 21 SPARK results, at the original v0.9 authoring milestone, the new formal proof stages remained NOT_RUN; the subsequent v1.1.0 archives preserve the separately executed local proof receipts.
Run without any additional dependencies:
python3 -m unittest discover -s tests -v
python3 scripts/check_automata_formal.py --output automata4-static.jsonOn a machine with the pinned Lean 4.35.0, GNATprove, GPRbuild and optional Node, the strict executable gate is:
export PATH="$HOME/opt/edgewalk-spark-toolchain/bin:$PATH"
python3 scripts/check_automata_formal.py --require-all --output automata4-evidence.jsonThis checks formal proof outcomes, compiled Ada execution and all 4,096 real JavaScript transitions as separate evidence classes.
Check saved evidence integrity (not execution attestation):
python3 scripts/verify_automata_evidence.py automata4-evidence.jsonNo build tool or external dependency is added to the deployed website. See AUTOMATA-FORMAL.md.
Open the four-cell formal lab. Updated site assets are deployed through a separate manual Pages workflow. It runs the actual first-party automaton on 4,096 inputs (256 rules × 16 width-four rows), checks all outputs and source ownership against an independent reference, and exports a locally hashed JSON receipt. There is only one authoritative four-cell formal specification, not competing Lean/Ada reference implementations.
Verify a browser receipt with standard-library Python:
python3 scripts/verify_automata_browser_receipt.py /path/to/automata4-browser-xxxxxxxxxxxx.json
The receipt verifies consistency with the canonical corpus but does not independently attest that the browser executed. Formal theorem checks and Ada differential execution remain optional developer-only tools.
The project now builds an exact, dependency-free Pages artifact from one allowlist of first-party files. PAGES-ARTIFACT/1 generates a deterministic SHA-256 manifest for every byte, rejects stale/missing/extra assets and malformed HTML/CSP, and retains the Git commit revision. The manual Pages workflow verifies that staged artifact before uploading it.
Two actual development-only browser engines exercise the staged website: headless Chromium and headless Firefox via Geckodriver. Real DOM journeys cover the deterministic automaton, first-party browser tests, property/formal labs, ledger search, local workflow handoff, CSP restrictions, basic labels and controlled ledger HTTP 503/malformed-JSON failure paths. Browser/tool absence is NOT_RUN, never fabricated success. The workflow also compares the official public GitHub Pages HTTPS asset bytes with the manifest after deployment; local checks are not misrepresented as public-deployment evidence.
python3 scripts/site_bundle.py stage --source . --site /tmp/independence-v1 --revision "$(git rev-parse HEAD)"
python3 scripts/site_bundle.py verify --source . --site /tmp/independence-v1 --revision "$(git rev-parse HEAD)"
python3 scripts/run_browser_journeys.py --site /tmp/independence-v1 --require-browser --output chromium.json
python3 scripts/firefox_journeys.py --site /tmp/independence-v1 --require-browser --output firefox.json
python3 scripts/verify_deployed_site.py --manifest /tmp/independence-v1/deployment-manifest.json
All Python utilities use the standard library. Firefox/Chromium binaries are optional developer testing tools, not site requirements. See the complete v1.0 verification scope.
The original 6,182-byte ZIP from GitHub Actions run 41112613136,
artifact 13003029340, is preserved as nine individually pinned lossless
base64 fragments. Python stdlib reconstructs and verifies the exact original
ZIP SHA-256 76514017982d86c95003bd4f86ccdcf4404502ede4609ba8f7767b89ee6c396a,
all four original member hashes, immutable PR checkout/source references and
92 recorded PASS assertions. No reserialisation or reconstructed ZIP substitutes
for original bytes.
python3 scripts/verify_browser_archive.py
python3 scripts/verify_browser_archive.py --restore independence-real-browser-evidence.zip
python3 -m unittest discover -s tests -p 'test_browser_archive.py' -vThe preserved evidence belongs to a PR test checkout, not the v1.0.0 tagged production deployment. SHA-256 and internally consistent receipts do not independently attest browser execution. See the preservation manifest and method.
The new mathematical model under
formal/rocq/Automata.v uses two structurally
independent transition functions: weighted arithmetic neighbourhood bit lookup
and an explicit eight-pattern rule table. It states fifteen theorem/example
obligations covering equivalence for all finite rows, equal output length,
Rule 0 and 255 identities, Rule 90 XOR, boundary handling, and the
width-four AUTOMATA4/1 specialisation.
Rocq 9.2.0 is an optional developer tool, not a website dependency.
CI performs strict source fingerprint inspection and a separate 4,096-vector
finite Python bridge, but explicitly records NOT_RUN for the Rocq compiler
unless the actual pinned toolchain is executed. No Rocq theorem is claimed
checked merely by merging this PR.
python3 scripts/check_rocq_semantics.py --output rocq-static.json
rocq --version # requires exactly Rocq 9.2.0
python3 scripts/check_rocq_semantics.py --require-rocq --output rocq-executed.jsonThe second command exits nonzero on missing, wrong-version or failed Rocq;
a successful run must produce a compiled .vo and report all fifteen
theorem assumption audits closed. The .vo and logs are generated in a
fresh temporary directory; the evidence JSON is written only on request.
The finite bridge is not a formal refinement proof of JavaScript or SPARK.
See Rocq developer verification.
The v1.1.0 formalisation report consolidates original byte-preserved Lean/SPARK/Ada/JavaScript and Rocq local evidence archives, the historical Chromium/Firefox PR evidence and a reproducible, explicit boundary between mathematical model proofs, contract discharge, finite executable conformance, and operational observations.
The uploaded original proof archives (3,473 and 3,658 bytes) are included losslessly, with pinned SHA-256 digests, a complete 15-member manifest, and a Python-stdlib verifier that checks the 13 original internal checksum entries, proof statuses and provenance:
python3 scripts/verify_formalisation_archive.py --output formalisation-integrity.json
python3 -m unittest discover -s tests -p 'test_formalisation_archive.py' -v
python3 scripts/verify_browser_archive.pyThe evidence records six Lean width-four model theorem checks, ten SPARK verification conditions, 4,096 Ada + 4,096 JavaScript finite comparisons, fifteen Rocq arbitrary-finite-width model theorem/example obligations and 92 historical recorded passing browser assertions. No proof of production JavaScript refinement or independently authenticated execution is claimed. The author-deposited Zenodo dataset is cited as Slade (2026), DOI 10.5281/zenodo.23816739. The original archives and evidence manifest retain the historical source identities and formal trust limits. The tagged metadata proposal is a pre-deposit planning document, not a replacement for the published citation.