遇见数据集

Paper B Reproducibility Evidence Chain for Lifecycle-Aware Isolated-Environment Replay of Proof-Carrying Formal Software

收藏
Zenodo2026-07-17 更新2026-08-02 收录
官方服务:

资源简介:

Version 1.1 is a non-retroactive correction release. It aligns the derived taxonomy, canonical-verdict schema, fixture classifications, and chronology metadata with Paper B Manuscript v0.3.1. Raw replay archives, source identity, exit codes, preserved historical packages, and contract-indexed results are unchanged: Replay 1 remains FAIL and Replay 2 remains PASS under K2/v2. The external AI-mediated replay protocol remains NOT YET EXECUTED, and no independent third-party reproduction or external validation is claimed. Version 1.0 remains an immutable historical baseline. This dataset consolidates the complete evidence chain supporting the methods paper “Lifecycle-Aware Isolated-Environment Replay for Proof-Carrying Formal Software.”It preserves: (1) the first raw replay returning FAIL; (2) canonical evidence normalization without retroactive verdict rewriting; (3) the release-lifecycle temporal oracle and its fixture coverage; (4) exact Lean/Lake and Coq/OCaml environment locks; (5) the second isolated-environment replay returning PASS under contract K2/v2; (6) the versioned contract registry, normalized G00–G20 gate ledger, orthogonal test taxonomy, and threat-to-validity register; and (7) a frozen external AI-mediated replay protocol whose status is NOT YET EXECUTED.The raw G03 failure is preserved separately from the temporal-oracle gate. The first replay remains FAIL, and the second PASS does not overwrite it.Both completed replays were operated by the author in separate fresh environments. Therefore, this record does not claim independent third-party reproduction or external validation.Source software: V0 OSAP Formal Core v1.3.0, commit 13bf095688bcabd5b090f188e9bd28a16237edeb, DOI 10.5281/zenodo.21346728. After downloading the record, run python verify_zenodo_upload.py to validate the archive, evidence checksums, source identity, preserved first-run FAIL, second-run PASS, and external-replay status.

提供机构:
Zenodo
创建时间:
2026-07-17
二维码
社区交流群
二维码
科研交流群
商业服务