v1.2.0 — External Research Provenance

PROVENANCE v1.2.0 adds an optional, vendor-neutral research manifest for retaining external research materials with explicit source identity, artifact hashes, attribution, licensing evidence and scope declarations.

The release includes an offline OpenAI Math example, an independent byte verifier, review-driven validation fixes and preservation of the historical Phase 18 archive’s citation metadata.

Release identity

• Version: v1.2.0
• Final merged commit: 41451bf690597a75f461299dfcbbee559c83e924
• Release DOI: [10.5281/zenodo.23207011](https://doi.org/10.5281/zenodo.23207011) — reserved for this version; publication remains a separate archival step.
• Merged PR: [#20](#20)
• Successful full release gate: [Run 37613070156](https://github.com/QSOLKCB/PROVENANCE/actions/runs/37613070156)
• Changes since v1.1.1: [Compare](v1.1.1...41451bf)

The immutable v1.2.0 tag should target the exact commit above.

Research manifests

The new provenance_research module introduces provenance.research-manifest.v1.

A manifest records:

• The upstream project, repository, exact commit, commit hash algorithm and declared license.
• Retained artifacts with unique keys, portable relative paths, upstream or local origin, roles, SHA-256 content identities and byte counts.
• Explicit reference, copy, adaptation and derivation relationships, including modification notices where required.
• Separate manuscript, formalized and local scopes.
• Relevant declarations, comparator references and optional retained verification receipts.
• Upstream credit, license evidence, NOTICE observations and citation artifacts.

Source commits explicitly declare sha1 or sha256. Copied artifacts must match both the upstream content identity and byte count.

Sealing uses the existing provenance.canonical-json.v1 canonicalization rules and a dedicated research-manifest hash domain:

sha256(b"PROVENANCE/RESEARCH-MANIFEST/v1\0" + canonical_json_bytes(core))

The sealed envelope binds the manifest core to its research identity and explicitly records the identity field’s self-hash exclusion.

Independent verification

Two public entry points support sealing and checking:

seal_research_manifest(core) -> bytes
verify_research_manifest(data, contents) -> dict

The verifier checks canonical encoding, schema validity, manifest identity and retained artifact SHA-256 hashes and byte counts. Artifact bytes come from a caller-supplied mapping keyed by content identity.

Verification performs no network access, path opening or proof execution. Its report keeps byte-integrity results, missing artifacts and errors visible.

Research metadata remains DECLARED. Upstream membership, mathematical validity and license compliance are reported as not_checked; retained receipts do not automatically establish those properties.

Research manifests and retained materials can be carried through existing evidence and custody workflows as ordinary artifacts. Research-specific verification remains an explicit operation.

OpenAI Math example

The release includes a small, pinned offline fixture from openai/math at commit:

adc7f1241b42e322a6451854ab7e4b4c146bf78a

The example covers family 271, associated with Spontaneous magnetization in the quantum Heisenberg ferromagnet, and declaration:

OAI.Heisenberg.spontaneous_magnetization

It retains five unmodified upstream files: the Apache-2.0 license, scope document, Lean challenge, comparator JSON and manuscript citation README. Their Git blob identities were checked against the pinned upstream revision.

OpenAI receives explicit upstream credit. These retained upstream materials preserve their Apache-2.0 licensing; the PROVENANCE implementation remains MPL-2.0.

The Lean challenge contains an upstream sorry. It is retained as a statement/comparator specification and does not constitute a completed proof. The fixture does not include the manuscript PDF, a solution corpus or proof-execution evidence.

Run the example with:

python3 -m examples.openai_math.verify

Validation and verifier fixes

Review feedback produced additional fail-closed behavior:

• Artifact paths reject all Unicode control-category characters, including DEL and C1 controls.
• Malformed artifact roles, origins and references are rejected before operations that could otherwise raise unexpected exceptions.
• Excessively nested input produces a failed verification report.
• Missing artifact lookups remain visible gaps while verification continues.
• Ordinary artifact-store exceptions are recorded with their exception type and message, allowing remaining artifacts to be checked.
• Metadata classification remains unset until the manifest core passes schema validation.

Historical archive integrity

The Phase 18 formal archive retains the historical v1.1.1 citation in formal/CITATION.cff, bound to DOI [10.5281/zenodo.23043860](https://doi.org/10.5281/zenodo.23043860).

The archive excludes the moving root CITATION.cff. Its generation validates the retained historical citation against a pinned digest and fails if those bytes change.

Regression tests exercise the workflow’s archive command, verify archive contents and confirm that later root citation changes do not alter the historical citation.

Compatibility and verification scope

Existing evidence, bundle, custody, package, signature and transfer formats remain unchanged. This release introduces no new runtime dependency or automatic upstream fetching.

The existing FV-01–FV-04 formal evidence remains scoped to the frozen v1.0.0 implementation:

0b1a2eea6c3c2b40a7f2a390fcd3410c75fab742

The new research module is covered by tests but is outside that formal runtime bridge. This release makes no whole-program verification claim and does not adopt or prove the example’s mathematical result.

Validation evidence

The release-grade full workflow completed successfully against the exact final merged commit. It covers the Rust CLI, Python invariant and integration suites, additional hash-seed checks, source cleanliness, tamper detection and real Ollama smoke lanes.

The focused research and historical archive regression suites passed 19 tests. The pinned offline fixture verifier also passed.

Release and archival metadata should retain the final commit SHA and successful workflow link above.

PROVENANCE v1.1.1 — Archival Metadata Finalization

Metadata-only archival release preparing PROVENANCE for final Zenodo publication.

Changes

• Updates CITATION.cff to v1.1.1.
• Sets the canonical release URL to v1.1.1.
• Marks the Phase 18 formal proof set as complete.
• Explicitly distinguishes:
  • v1.0.0 — immutable implementation target formally modelled in Lean.
  • v1.1.1 — formal verification and archival release layer.
• Records Zenodo DOI 10.5281/zenodo.23043860 as publication pending.

No runtime, proof-source, schema, verifier, or evidence-contract semantics are changed.

Formal verification against the frozen v1.0.0 target remains unchanged and green.

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.

v1.0.0 - PROVENANCE — Inaugural Release

Provenance v1.0.0
Cryptographic chain of custody for LLMs, software, agents, tools, and automated systems.

This is the first tagged release of PROVENANCE and therefore represents the complete project history from its constitutional foundation through the implemented Phase 16 release-grade trust lane.

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

It provides a framework-neutral system for capturing actions, preserving exact artifacts, binding evidence and custody records to cryptographic identities, retaining uncertainty explicitly, and independently verifying the resulting record without requiring the original monitored application.

Release Target

commit:
0b1a2eea6c3c2b40a7f2a390fcd3410c75fab742

roadmap state:
Phase 16 implemented

next roadmap stage:
Phase 17 — Immutable Candidate Freeze

This release establishes the implementation state developed across Phases 0–16.

Because this is the first tagged release, there is no previous release baseline or incremental changelog. The notes below describe the complete implemented system.

---

Highlights

• Deterministic canonical evidence identities.
• SHA-256 content identity for raw artifacts.
• Domain-separated identities for structured PROVENANCE records.
• Explicit OBSERVED, DECLARED, and DERIVED evidence classes.
• Independent read-only evidence verification.
• Local content-addressed evidence storage.
• Append-only cryptographically linked custody.
• Explicit clock-source assurance.
• Real Ollama observation with independent real-model CI.
• Dependency-free MCP stdio interface.
• Zero-dependency Rust CLI and keyboard-first terminal interface.
• Read-only localhost evidence viewer.
• Provider-neutral HTTP and local-process adapters.
• Portable forensic evidence packages.
• Detached Ed25519 SSHSIG signatures.
• Git commit anchoring.
• Bounded deterministic parallel verification.
• Verifiable selective disclosure and redacted derivatives.
• Signed offline distributed-custody transfer.
• Release-grade full-system trust lane with pinned toolchains and real-model validation.

---

Phase 0 — Constitutional Foundation

Established the repository's governing evidence and architecture principles before implementation.

The project defines:

what PROVENANCE records
what PROVENANCE does not control
what counts as evidence
how uncertainty is represented
how modules remain separated
which invariants cannot silently change

Core project guidance includes:

• README.md
• README4AIs.md
• AGENTS.md
• architecture and invariants documentation
• project lineage
• donor/provenance documentation
• phased roadmap

The foundational design law is:

RECOMPUTE.
DO NOT TRUST STORED CLAIMS WHEN THEY CAN BE RECOMPUTED.
DO NOT REWRITE HISTORY.
DO NOT HIDE EVIDENCE GAPS.

---

Phase 1 — Canonical Evidence Core

Introduced the dependency-free universal evidence model.

Implemented:

• strict canonical UTF-8 JSON
• deterministic key ordering
• compact separators
• canonical trailing-newline policy
• duplicate-key rejection
• BOM rejection
• non-finite and unsafe-number rejection
• ordinary sha256:<digest> artifact content identity
• domain-separated structured identities
• immutable artifact records
• immutable event records
• relationships
• manifests
• evidence classification
• retention and collection states
• self-hash exclusion rules

Evidence classes:

OBSERVED
DECLARED
DERIVED

Raw artifact SHA-256 remains directly interoperable with ordinary forensic and cryptographic tooling.

Structured records use explicit semantic identity domains so that an artifact, event, manifest, custody record, and other structured objects cannot silently share identity semantics.

---

Phase 2 — Independent Verifier

Added the independent, read-only provenance_verify implementation.

The verifier recomputes rather than trusts:

• manifest identities
• artifact-record identities
• retained artifact hashes
• byte counts
• event identities
• self-hash exclusions
• bundle closure
• references and relationships
• canonical JSON
• physical filesystem membership

Adversarial verification covers cases including:

• changed artifact bytes
• changed structured fields
• wrong byte counts
• missing evidence
• undeclared extra members
• duplicate entries
• malformed identities
• noncanonical JSON
• symbolic links
• special filesystem entries
• unsafe path traversal
• malformed or incomplete structured data
• unresolved event relationships
• parser-depth and numeric-limit failures

The verifier does not repair evidence to make verification succeed.

---

Phase 3 — Local Content-Addressed Evidence Store

Added the first local evidence store.

The reference backend uses:

local filesystem
+
content-addressed immutable objects

Implemented:

• retained artifact storage
• artifact-record storage
• event storage
• immutable snapshots
• strong-content deduplication
• exact-byte conflict detection
• atomic no-overwrite publication
• verifier-gated finalization
• durable HEAD advancement
• reopening verified snapshots
• monotonic evidence availability

Retention may advance:

MISSING
→ DIGEST_ONLY
→ CONTENT_RETAINED

but historical evidence is never rewritten to pretend unavailable evidence was always present.

Extensive hardening covers:

• interrupted publication
• corrupt objects
• stale finalizers
• symlink substitution
• filesystem identity changes
• snapshot reconstruction
• directory fsync durability
• stale and concurrent processes
• descriptor cleanup
• concurrent store initialization

---

Phase 4 — Minimal Append-Only Custody Chain

Extended artifact integrity into cryptographically linked custody.

Implemented custody actions:

CAPTURED
STORED
VERIFIED
EXPORTED
TRANSFERRED
SUPERSEDED

Custody records bind:

• subject identity
• action
• actor/source when available
• related identity
• previous custody identity
• recorded time
• time source
• time assurance

Clock assurance includes:

LOCAL
NETWORK
AUTHENTICATED_NETWORK
SIGNED_ATTESTATION

Custody order comes from cryptographic predecessor links, not wall-clock comparison.

The ledger is append-only and derives current tips from immutable records rather than trusting mutable per-subject HEAD files.

Concurrency and crash recovery were hardened using:

same-process synchronization
+
POSIX fcntl locking
+
non-authoritative staging

Unknown handlers remain unknown rather than being invented.

---

Phases 5–6 — Ollama Reference Adapter and Real-Model CI

Added the first real AI-system observation path.

Local Ollama adapter

The stdlib-only adapter uses local Ollama /api/generate.

It captures exact:

• request bytes
• response bytes
• request events
• response events
• declared model identifiers
• adapter identity/version
• observation boundaries
• failure evidence
• custody

Classification remains explicit:

request bytes seen by adapter
→ OBSERVED

response bytes seen from Ollama
→ OBSERVED

model identifier reported by Ollama
→ DECLARED

It does not claim observation of:

• hidden model state
• chain-of-thought
• internal GPU execution
• unexposed provider provenance

Transport hardening

The adapter includes protections for:

• proxy bypass
• non-loopback rejection
• redirect rejection
• malformed HTTP status
• truncated response bodies
• truncated HTTP error bodies
• duplicate/non-finite/malformed JSON
• zero-length responses
• failed observations
• exact failure-detail retention
• repeated identical calls
• thread concurrency
• cross-process observation races

Real-model CI

Clean GitHub-hosted runners independently exercise:

qwen2.5:0.5b
qwen2:0.5b

Each lane:

1. verifies the pinned Ollama installer checksum;
2. installs pinned Ollama;
3. starts an independent local server;
4. pulls the reference model;
5. performs real inference;
6. records exact evidence;
7. independently verifies bundle and custody;
8. tampers retained evidence;
9. requires verification to fail.

Model output text is deliberately not used as a golden fixture.

---

Phase 7 — MCP Stdio Interface

Added a dependency-free MCP server over stdio.

Implemented tools:

provenance.record
provenance.inspect
provenance.verify
provenance.finalize
provenance.export
provenance.package

Identity-addressed resources expose artifacts, events, manifests, and custody.

Critical classification rule:

caller assertion
→ DECLARED

observed MCP invocation occurrence
→ OBSERVED

Repeated identical declarations may deduplicate as content but do not collapse separate observed call occurrences.

The MCP layer delegates to the existing core, store, custody, export, and verification implementations rather than creating a separate MCP evidence format.

---

Phase 8 — Rust CLI and Terminal Interface

Added a zero-external-dependency Rust command-line interface.

Commands developed through the current implementation include:

record
inspect
verify
finalize
export
package
sign-package
anchor-payload
anchor-git
verify-assurance
redact-disclosure
verify-disclosure
transfer-create
transfer-receive
verify-transfer
verify-receipt
tui

The terminal interface includes a keyboard-first slash-command palette.

Operator-supplied evidence remains DECLARED.

Each successful record invocation also creates unique OBSERVED occurrence evidence.

CLI and MCP intentionally share hardened operational working state so the interfaces cannot acknowl...