Lifecycle-Aware Replay for Proof-Carrying Formal Software: Contract-Indexed Verdicts, Temporal Test Semantics, and Cross-Backend Evidence Preservation

Abstract

Formal-software releases are executable research objects whose replay depends on source identity, release history, test semantics, proof-assistant toolchains, environment state, and verdict rules. This paper develops a lifecycle-aware replay method and evaluates it through a bounded case study of an immutable release containing Python validators and Lean and Coq backends. A first author-operated replay returned FAIL because a release-candidate assertion was evaluated against a post-release repository state and Lean/Lake was unavailable. The method preserved that result and introduced a versioned contract separating the raw test outcome from a lifecycle-oracle disposition, locking Lean 4.19.0/Lake 5.0.0 and Coq 8.18.0/OCaml 4.14.1, and retaining tracked-source hygiene. A second fresh replay preserved the same raw Python failure, passed the oracle and both formal backends, and returned PASS: V(R1,K1)=FAIL and V(R2,K2)=PASS. The frozen source additionally exposes a 36-record T121-T156 structural theorem inventory. All identifiers have paired Lean and Coq symbols and declared fixture mappings; 30 upstream canonical statement hashes were revalidated, while six Phase 1 statements received a separate v0.5.4 normalization. The paper contributes a formal replay model, non-retroactive evidence governance, lifecycle-sensitive gate classification, a required-backend rule, cross-backend structural correspondence, and practical release templates. Because one investigator designed K2/v2 and operated both replays, the study demonstrates transparent self-audited replay rather than independent certification. Independent reproduction, proof-term or kernel equivalence, unrestricted cross-backend semantic equivalence, and bit-for-bit reproducibility are not claimed. A separate pre-execution audit found canonical protocol v0.7 handoff-ready; its payload remains prepared but undelivered, and unaffiliated external replay is deferred pending an available qualified evaluator.