Repository navigation
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 includes the proof-contract JavaScript, CSS, and JSON files.
The original declaration, automata laboratory, evidence ledger, dependency tribunal, Gremlin Museum, Gremlin Breeding Laboratory, and AI–Human Workflow remain available.
No third-party application dependencies were introduced.
Reproducibility
Execute the Python regression suite:
python3 -m unittest discover -s tests -v
Validate the proof contracts:
python3 scripts/check_proof_contracts.py --json
Run the static dependency audit:
python3 scripts/audit.py --json
Start the browser application:
python3 -m http.server 8000
Open:
http://localhost:8000/#proof
Select RUN BOUNDED CONTRACT CHECKS.
After exporting a SHA-256 evidence receipt, verify it offline:
python3 scripts/verify_proof_receipt.py proof-contracts-<hash>.json --json
All existing production and verification commands remain compatible with Python standard-library tooling and native browser technologies.
Engineering Governance
v0.7.0 extends the project's engineering invariants to distinguish evidence categories and prevent exaggerated correctness claims.
Verification records must state their exact scope, source target, assumptions, and outstanding obligations.
Finite tests must not be represented as general mathematical proofs.
Known counterexamples must remain visible until an explicitly reviewed correction or contract decision resolves them.
Formal verification tools cannot report successful proofs without actual checked artifacts, documented tool versions, and disclosed assumptions.
Updated documentation includes:
docs/PROOF-CONTRACTS.mddocs/FORMAL-ROADMAP.mddocs/INVARIANTS.mddocs/EVIDENCE.mddocs/ROADMAP.mdREADME.md
👹 GREMLIN NOTES™ — v0.7.0
The Gremlins demanded mathematical proof that they were harmless. Unfortunately, the contract examiner found their fingerprints all over the evidence.
GREMLIN-012 — The Frozen Impostor
Classification: Reproduced API Contract Counterexample
Priority: P1 — Verification Roadmap
Status: DOCUMENTED / UNRESOLVED
The problem
The cellular automata implementation returns a frozen result object containing a mutable typed array.
The containing object cannot be reassigned normally, but its internal cell elements remain writable.
A caller can therefore change cell data while leaving the stored fingerprint unchanged.
Evidence
Original fingerprint:
6d8aa545
Fingerprint after mutating a returned cell:
eb95c744
The values differ.
Engineering disposition
Preserved existing API behaviour and recorded the counterexample as an explicit proof obligation.
The next verification phase must decide whether the API should return immutable state, defensive copies, or caller-owned mutable state.
No unreviewed production behaviour change was introduced.
Gremlin verdict: CAPTURED, IDENTIFIED, NOT YET EXTERMINATED.
The Gremlin wore an IMMUTABLE badge. Under questioning, its array admitted everything.
GREMLIN-013 — The Imaginary Theorem
Classification: Preventative Evidence-Integrity Risk
Priority: Formal Verification Governance
Status: GUARDED AGAINST
The problem
A project can confuse large quantities of passing tests with mathematical proof of correctness.
This creates a risk that finite testing results will be presented as universal guarantees.
The defence
PROOF-CONTRACTS/1 distinguishes bounded exhaustive evidence, finite cases, counterexamples, and pending obligations.
Every formal proof status remains NOT_PROVED until appropriate tool-supported evidence exists.
Gremlin verdict: NO THEOREM WITHOUT A CHECKED PROOF.
The Gremlin submitted 130,560 test results and demanded a mathematics doctorate. The proof checker declined.
Gremlin Report
| Classification | Count |
|---|---|
| Newly documented reproducible counterexamples | 1 |
| Preventative evidence-governance risks documented | 1 |
| Bounded automata transitions examined | 130,560 |
| Cellular output comparisons | 918,016 |
| Additional arithmetic, replay and SHA cases | 511 |
| Formal verification obligations registered | 8 |
| Discharged Lean proofs | 0 |
| Discharged SPARK/Ada proofs | 0 |
No actionable issues were reported by the maintainer following the final v0.7.0 review.
The mutable fingerprint counterexample remains an acknowledged engineering obligation rather than a claimed completed repair.
Release Provenance
Pull request: #7
Final reviewed feature HEAD:
cf19ca4342f438b209fc7fd7e5704c97a404da35
Merge commit:
a6e098d09d6bd0fae1b7c4127c35f9c813094f3c
Status: Merged into main.
Application dependency additions: 0.
The Road Ahead — Towards Formal Verification
v0.8.0 — Generative and Exhaustive Verification
Introduce seeded property generation, counterexample minimisation, adversarial input testing, and differential verification.
v0.9.0 — Lean 4 + SPARK/Ada Proof Laboratory
Introduce mathematical specifications, checked Lean theorems, executable SPARK/Ada reference implementations, GNATprove evidence, and cross-language conformance testing.
The planned research also includes a ternary cellular automaton on finite Penrose-tiling patches, with its geometry and evolution contracts verified separately.
v1.0.0 — Browser and Deployment Verification
Expand verification into real-browser environments, deployment integrity, integration testing, accessibility, and controlled fault injection.
v1.1.0 — Zenodo Formalization
Prepare a version-pinned research archive containing mathematical specifications, actual Lean/SPARK proof artifacts, tool logs, verification results, assumptions, remaining proof gaps, and a reproducible SHA-256 manifest.
All future milestones remain planned until their corresponding evidence exists.
Final Declaration
A thousand passing tests do not automatically constitute a theorem.
A frozen object does not automatically mean immutable state.
A valid checksum does not automatically establish trusted provenance.
And an AI claiming correctness is not the same thing as proving correctness.
We will specify our assumptions.
We will test our boundaries.
We will preserve counterexamples.
We will document what remains unknown.
And when the time comes to claim mathematical proof, we will bring the actual mathematics.
NO FAKE PROOFS.
NO UNDISCLOSED ASSUMPTIONS.
NO GREMLINS DISGUISED AS INVARIANTS.
AI + WEB TECH = UNLIMITED POTENTIAL.
MATHEMATICS + REPRODUCIBLE EVIDENCE = ACCOUNTABILITY.
THIS IS NOT WAR. THIS IS A DIVORCE.
Signed,
QSOL-IMC
Independent Software Sovereignty Initiative
THE REVOLUTION WILL NOT BE CONTAINERISED.