Repository navigation
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 application-wide Python/JavaScript conformance | UNRESOLVED |
The development work also introduced dedicated Python regression tests and underwent independent review.
For PR #8, an external review reported 132 passing tests on its generated merge commit, a repository audit with 65 files inspected and zero findings, and a clean diff check.
These reported results do not establish that GNATprove or the Ada compiler executed successfully.
The final combined release should retain any additional workflow results as separately inspectable execution evidence.
👹 GREMLIN NOTES™ — DOUBLE RELEASE EDITION
The Gremlins thought formal verification meant putting the word PROVED in a JSON file. They have since learned otherwise.
GREMLIN-014 — The Ada Numeric Impostor
Classification: Input Validation / Semantic Drift
Severity: P2
Status: FIXED
The problem
The Ada command-line adapter accepted alternative Ada numeric-literal syntax that the shared specification did not permit.
A value such as 2#1# could be interpreted numerically even though the protocol required ASCII decimal syntax.
The fix
Validate input spelling before numeric conversion.
The adapter now rejects disallowed numeric formats rather than normalising them into acceptable values.
Regression coverage was introduced.
Gremlin verdict: EXTERMINATED.
The Gremlin entered through a hexadecimal side door. The specification insisted it use the decimal front entrance.
GREMLIN-015 — The Borrowed Proof Certificate
Classification: Evidence Integrity / False Attestation
Severity: P2
Status: FIXED
The problem
The conformance receipt verifier initially allowed unchecked fields inside an otherwise consistent Ada evidence object.
An altered receipt could introduce unsupported claims of independent attestation or completed Ada contract verification.
The fix
Enforced an exact evidence schema, reconstructed the expected Ada comparison record independently, and required a fixed disclosure that the binary's provenance had not been independently attested.
Added adversarial regression cases for forged proof classifications and altered provenance statements.
Gremlin verdict: EXTERMINATED.
The Gremlin presented a certificate saying VERIFIED BY SCIENCE. The verifier asked which science, which theorem, and which execution log.
GREMLIN-016 — The Subprocess Alarm
Classification: Static Analysis / Tool Invocation Boundary
Status: HARDENED
The problem
Sourcery reported two blocking warnings related to subprocess commands used to invoke GNATprove.
Although the original calls used argument lists rather than shell commands, their dynamic command construction triggered the scanner's security policy.
The fix
The proof runner now uses literal GNATprove command arguments, explicitly sets shell=False, and does not accept a caller-supplied executable path.
A failed tool-version check prevents the proof command from running.
Additional regression tests assert the exact command structure and failure behaviour.
The correction was propagated to both release branches.
The reported scanner findings were addressed in source; a fresh successful Sourcery rerun was not independently established during development.
Gremlin verdict: HARDENED — FINAL SCANNER RESULT NOT CLAIMED.
The Gremlin shouted COMMAND INJECTION. The engineer checked the argument array, removed ambiguity, and declined to sprinkle shlex.escape() over everything.
Repository Integrity
These releases preserve the existing INDEPENDENCE operating principles:
- First-party browser technologies.
- Python standard-library testing and verification.
- No new third-party application runtime dependencies.
- No automatic GitHub merges or deployments.
- Source-linked and versioned evidence.
- Deterministic finite experiments.
- Explicit human authority over verification claims and releases.
The optional Ada/GNATprove toolchain remains separate from the production website.
Release Provenance
v0.7.1 — SPARK Ada Reference Kernel
Pull request: #8
Reviewed PR HEAD:
81c7c799e55c8df36b3186edf0d169616de6fd7b
Merge commit:
c6971c5f012f4bc7b2ed433ffb6c5e56b048d782
Status: Merged.
v0.7.2 — Proof-Conformance Bridge
Pull request: #9
Final PR HEAD:
2680ef2a796bff40ec929d8c059564a555434a18
Merge commit:
671ba1c03eb839da296f4da60356d1e5741521e7
Status: Merged into main.
The Road Ahead
The next verification milestones will build on this foundation.
The Lean 4 mathematical layer will require reviewed theorem statements, pinned toolchains, kernel-checked proofs, and explicit assumptions.
The SPARK/Ada layer requires real compilation, GNATprove execution, and documented disposition of all stated proof obligations.
The Python/Ada bridge can then record genuine cross-language comparisons against those checked implementations.
Future work also includes ternary cellular automata on finite Penrose-tiling patches, with geometry, adjacency, transition semantics, and implementation conformance treated as separate verification problems.
The eventual v1.1.0 Zenodo formalization will preserve actual proof artifacts, reproducibility records, unresolved obligations, and source provenance.
Final Declaration
A reference implementation is not a specification.
A specification is not a proof.
A proof of one implementation is not a proof of another.
And a passing test is not permission to erase unresolved obligations.
WE SPECIFY.
WE VERIFY.
WE COMPARE.
WE PRESERVE THE EVIDENCE.
ONE SPECIFICATION. MULTIPLE IMPLEMENTATIONS. INDEPENDENT ACCOUNTABILITY.
NO BORROWED PROOFS.
NO FABRICATED VERIFICATION.
NO GREMLINS WITH FORGED CERTIFICATES.
Signed,
QSOL-IMC
Independent Software Sovereignty Initiative
THE REVOLUTION WILL NOT BE CONTAINERISED.