PROVENANCE v1.1.0 — Formal Verification & Archival Release

PROVENANCE — Phase 18 Final Archival Release

This release completes the repository-side formal verification and archival release layer for PROVENANCE.

It does not redefine or replace the frozen implementation release.

The implementation formally targeted by this release remains:

PROVENANCE v1.0.0
commit: 0b1a2eea6c3c2b40a7f2a390fcd3410c75fab742

The final archival material is built around that immutable target and records the formal proofs, proof/runtime correspondence, executed verification evidence, reconstruction data, and publication metadata required for long-term independent inspection.

Phase 18

Phase 18 introduces a self-contained Lean 4 formal verification project and an archival evidence pipeline for selected stable PROVENANCE invariants.

Reference toolchain:

Lean 4.34.1

Reserved archival DOI:

10.5281/zenodo.23043860

The formal proof set consists of four deliberately bounded claims:

FV-01  Self-hash exclusion
FV-02  Append-only history extension
FV-03  Classification non-promotion
FV-04  Presentation non-interference

These proofs establish properties of an explicit Lean model corresponding to selected PROVENANCE invariants.

They do not claim whole-program formal verification of the complete Python or Rust implementation.

Formal Claims

FV-01 — Self-hash exclusion

Formalizes the rule that an object's stored self-identity is excluded from the input used to recompute that identity.

Runtime correspondence:

INV-HSH-2

The model proves that changing only the stored identity field cannot alter recomputation from the underlying core.

FV-02 — Append-only history extension

Formalizes the append-only history rule:

history
→
history ++ [new_record]

and proves that:

• the complete prior history remains a prefix; and
• previously existing records remain present after append.

Runtime correspondence:

INV-CUS-1
INV-EVD-3

This theorem concerns logical history extension. It does not claim to prove filesystem durability, locking, or operating-system behaviour.

FV-03 — Classification non-promotion

Formalizes the evidence-classification rule that caller-provided assertions remain:

DECLARED

rather than silently becoming:

OBSERVED

It also proves that transformations of unrelated fields do not alter the evidence class.

Runtime correspondence:

INV-CLS-3

FV-04 — Presentation non-interference

Formalizes the read-only presentation boundary.

A presentation operation may derive a rendered representation from evidence, but the source evidence remains unchanged.

Runtime correspondence:

INV-EVD-5
INV-ARC-3

This models the non-authoritative, read-only role of the PROVENANCE presentation layer.

Runtime Bridge

The formal model is connected to the frozen implementation through an explicit documented bridge containing:

• invariant identifiers;
• named runtime modules and functions;
• regression tests;
• frozen source identity;
• proof limitations;
• formal theorem identities.

The intended statement is:

THE ENCODED LEAN MODEL
SATISFIES
FV-01 .. FV-04

It is explicitly not:

THE ENTIRE PROVENANCE IMPLEMENTATION
IS FORMALLY VERIFIED

The formal layer does not independently prove:

operating-system correctness
filesystem durability
lock implementation correctness
cryptographic collision resistance
Python interpreter correctness
Rust compiler correctness
GitHub Actions correctness
external provider behaviour
source-data truth
human/legal identity
legal or factual truth

Independent Proof Verification

The dedicated formal CI lane performs a fresh reconstruction using the pinned Lean toolchain.

The verification sequence includes:

verify frozen v1.0.0 target
        ↓
checksum official Lean 4.34.1 bundle
        ↓
lake build
        ↓
lake env leanchecker ProvenanceFormal
        ↓
formal-source placeholder/axiom scan
        ↓
verification attestation
        ↓
formal evidence manifest
        ↓
archival source bundles
        ↓
SHA-256 checksums

The formal-source scan rejects the whole tokens:

sorry
admit
axiom

across every tracked .lean file under formal/ at the recorded proof commit.

The archive manifest inventories the proof and archival source material directly from Git rather than mutable working-tree bytes.

Executed Verification Evidence

The archival workflow retains the actual proof execution evidence:

verification-attestation.json
lean-version.txt
lake-version.txt
lake-build.log
leanchecker.log
formal-evidence.json
SHA256SUMS

The success attestation is created only after both:

lake build

and:

lake env leanchecker ProvenanceFormal

complete successfully in the same fail-closed workflow step.

The attestation records:

• frozen implementation identity;
• proof commit;
• DOI;
• Lean bundle digest;
• GitHub workflow-run identity;
• exact Lean and Lake versions;
• hashes of the retained verification logs.

Archival Source Material

The Phase 18 archive contains two distinct source identities.

Frozen implementation

PROVENANCE-v1.0.0-source.tar.gz

Generated directly from:

tag:    v1.0.0
commit: 0b1a2eea6c3c2b40a7f2a390fcd3410c75fab742

This remains the immutable implementation authority.

Formal and archival sources

PROVENANCE-phase18-formal-sources.tar.gz

Containing the formal proof project and associated archival material, including:

• formal/ProvenanceFormal.lean
• formal/TARGET.json
• pinned Lean toolchain
• Lake project configuration
• formal-verification bridge
• archival protocol
• citation metadata
• verification-attestation generator
• formal-evidence generator
• formal CI definition

Human-Facing Formal Record

The archival package additionally includes a human-facing technical record describing the complete PROVENANCE architecture and invariant system.

It documents the repository as a layered evidence system spanning:

canonical evidence
cryptographic identity
independent verification
local storage
custody
adapters
MCP
CLI
read-only presentation
forensic packaging
performance
privacy
distributed custody
release trust
formal verification
archival publication

The broader repository formalization is intentionally distinguished from the smaller subset that receives machine-checked Lean proofs.

Known Formal Boundary

A post-v1.0.0 first-construction custody-format publication race was discovered during later CI activity and fixed on main.

The immutable v1.0.0 implementation remains unchanged.

The Phase 18 Lean model does not claim to formalize filesystem concurrency or custody-format bootstrap locking, and the archival record preserves that distinction.

Final Archival Sequence

This release occupies the final repository-tag stage of the Phase 18 archival process:

immutable v1.0.0 implementation
        ↓
Lean formalization
        ↓
reconstructed formal verification
        ↓
archival bundle
        ↓
THIS FINAL ARCHIVAL TAG
        ↓
tag-triggered formal verification
        ↓
Zenodo publication

The final Zenodo record will bind:

frozen implementation target
formal proof sources
proof toolchain
executed verification evidence
final archival tag
DOI/version metadata

Repository State

Implementation authority:

v1.0.0
0b1a2eea6c3c2b40a7f2a390fcd3410c75fab742

Phase 18 merge state:

97ba96785de9799ba899d3d1f921ff265554ba4b

Formal toolchain:

Lean 4.34.1

Archival DOI:

10.5281/zenodo.23043860

Release Principle

PROVENANCE records:

who did what, when, where, why, and how — backed by evidence.

This archival release applies the same principle to PROVENANCE itself.

The implementation, proof model, verification execution, toolchain, archive contents, and publication identity are retained as separately identifiable evidence rather than collapsed into a single unsupported claim of trust.

Build the smallest trustworthy layer.
Prove it.
Then preserve the evidence.