Add PCS formalization artifacts and Lean failure gallery.

Co-authored-by: Cursor <cursoragent@cursor.com>

Author: fraware

.github/workflows/pcs.yml

@@ -75,6 +75,8 @@ jobs:
         run: python examples/pcs_qc_release/scripts/ci_validate_regeneration_report.py
       - name: Validate failure_case_manifest.json gallery metadata
         run: python examples/pcs_qc_release/scripts/ci_validate_failure_manifests.py
+      - name: Validate proof-obligation formalization artifacts
+        run: python examples/pcs_qc_release/scripts/ci_validate_formalization.py
       - name: Verify LabTrust release protocol package
         run: |
           labtrust verify-release-protocol \

docs/contracts/cli_contract.md

@@ -69,11 +69,11 @@ This document defines the contract for all LabTrust-Gym CLI commands: exit codes
 | verify-release-protocol | `--release-dir <dir>`; optional `--pcs-core <dir>` | 0 | (stderr OK labels) | examples/pcs_qc_release/RUNBOOK.md |
 | verify-release-fixtures | alias for `verify-release-protocol` | 0 | (stderr OK labels) | examples/pcs_qc_release/RUNBOOK.md |
 | check-status-policy | `--release-dir <dir>`; optional `--workflow-profile`; `--json` | 0 | Status boundary checks (no ProofChecked from LabTrust) | examples/pcs_qc_release/RUNBOOK.md |
-| regenerate-release-protocol | `--out <release-dir>`; `--certifyedge-bin`; optional `--pcs-core`; `--workflow-profile`; `--json-summary`; `--summary-out` | 0 | Full protocol package; writes `<out>/regeneration_report.json` (pcs-bench fields) | examples/pcs_qc_release/RUNBOOK.md |
+| regenerate-release-protocol | `--out <release-dir>`; `--certifyedge-bin`; optional `--pcs-core`; `--workflow-profile`; `--json-summary`; `--summary-out` | 0 | Full protocol package; writes `<out>/regeneration_report.json`, `proof_obligation_hints.json`, `proof_obligation_identifiers.json`, `formalization_readiness_report.json` (pcs-bench; Lean extraction inputs only) | examples/pcs_qc_release/RUNBOOK.md, schemas_or_docs/FormalizationReadinessReport.v0.md |
 | regenerate-release-chain | alias for `regenerate-release-protocol` | 0 | same as above | examples/pcs_qc_release/RUNBOOK.md |
 | generate-failure-gallery | `--workflow <id\|property_id>`; `--out <dir>`; optional `--release-dir`; `--workflow-profile` | 0 | Per-case `failure_case_manifest.json`, `README.md`, `artifacts/`, legacy `expected_failure.json` / `repair_hint.json` | examples/pcs_qc_release/failures/ |
 
-**PCS CI scripts (not `labtrust` subcommands):** `run_pcs_ci_local.{sh,ps1}` runs `pytest tests/pcs`, `ci_validate_workflow_profile.py`, export/release validation, `check-status-policy`, failure gallery generate/verify, and optional `verify-release-protocol` (matches `.github/workflows/pcs.yml`). `materialize_workflow_profile.py` refreshes `workflow_profile.v0.json` digest. `generate_golden.py` regenerates `expected/` in deterministic mode.
+**PCS CI scripts (not `labtrust` subcommands):** `run_pcs_ci_local.{sh,ps1}` runs `pytest tests/pcs`, `ci_validate_workflow_profile.py`, `ci_validate_formalization.py`, export/release validation, `check-status-policy`, failure gallery generate/verify, and optional `verify-release-protocol` (matches `.github/workflows/pcs.yml`). `materialize_workflow_profile.py` refreshes `workflow_profile.v0.json` digest. `materialize_formalization_artifacts.py` rebuilds formalization JSON from an existing `release/` tree. `generate_golden.py` regenerates `expected/` in deterministic mode.
 
 ## Optional / conditional commands
 

docs/pcs-reference-implementation.md

@@ -24,6 +24,7 @@ machine-readable benchmark report.
 | Reference workflow | `src/labtrust_gym/pcs/workflows/qc_release.py` |
 | Registry | `src/labtrust_gym/pcs/workflows/registry.py` |
 | Regeneration report | `src/labtrust_gym/pcs/regeneration_report.py` |
+| Proof-obligation / Lean readiness | `src/labtrust_gym/pcs/formalization.py` |
 | Failure manifests | `src/labtrust_gym/pcs/failure_case_manifest.py` |
 | JSON Schema | `policy/schemas/pcs/RegenerationReport.v0.schema.json`, `FailureCaseManifest.v0.schema.json` |
 | Committed release | `examples/pcs_qc_release/release/` |
@@ -38,6 +39,7 @@ labtrust regenerate-release-protocol \
   --out examples/pcs_qc_release/release
 
 python examples/pcs_qc_release/scripts/ci_validate_regeneration_report.py
+python examples/pcs_qc_release/scripts/ci_validate_formalization.py
 python examples/pcs_qc_release/scripts/ci_validate_failure_manifests.py
 pytest tests/pcs -q
 ```

docs/pcs-workflow-implementation-guide.md

@@ -143,6 +143,13 @@ CI validators (LabTrust reference):
 - `examples/pcs_qc_release/scripts/ci_validate_failure_manifests.py`
 - `examples/pcs_qc_release/scripts/materialize_regeneration_report.py` (refresh report without CertifyEdge)
 
+Proof-obligation readiness (Lean extraction, not Lean execution):
+
+- `proof_obligation_hints.json` — artifact paths for pcs-core
+- `proof_obligation_identifiers.json` — stable IDs for ProofObligation.v0
+- `formalization_readiness_report.json` — emitted by `regenerate-release-protocol`
+- WorkflowProfile `formalization.formalization_scope` must be `trust_envelope_only`
+
 JSON Schema (validated on write and in CI):
 
 - `policy/schemas/pcs/RegenerationReport.v0.schema.json`

examples/pcs_qc_release/RUNBOOK.md

@@ -292,6 +292,12 @@ labtrust regenerate-release-protocol \
 # examples/pcs_qc_release/release/regeneration_report.json
 python examples/pcs_qc_release/scripts/ci_validate_regeneration_report.py
 
+# Lean readiness (LabTrust does not run Lean; trust_envelope_only):
+# proof_obligation_hints.json, proof_obligation_identifiers.json,
+# formalization_readiness_report.json
+python examples/pcs_qc_release/scripts/ci_validate_formalization.py
+python examples/pcs_qc_release/scripts/materialize_formalization_artifacts.py
+
 labtrust check-status-policy \
   --release-dir examples/pcs_qc_release/release
 
@@ -342,6 +348,7 @@ pytest tests/pcs/test_pcs_release_contract.py -q
 pytest tests/pcs/test_release_protocol_producer.py -q
 python examples/pcs_qc_release/scripts/ci_validate_release_fixtures.py
 python examples/pcs_qc_release/scripts/ci_validate_regeneration_report.py
+python examples/pcs_qc_release/scripts/ci_validate_formalization.py
 python examples/pcs_qc_release/scripts/ci_validate_failure_manifests.py
 python examples/pcs_qc_release/scripts/ci_validate_pcs_exports.py
 python examples/pcs_qc_release/scripts/write_failure_case_manifests.py

examples/pcs_qc_release/failures/certificate_id_tamper/artifacts/handoff_to_certifyedge.json

@@ -1,5 +1,5 @@
 {
-  "created_at": "2026-05-18T21:00:43Z",
+  "created_at": "2026-05-18T23:17:38Z",
   "expected_outputs": {
     "trace_certificate.json": {
       "artifact_type": "TraceCertificate.v0"
@@ -11,7 +11,7 @@
   "input_artifacts": {
     "runtime_receipt.json": {
       "artifact_type": "RuntimeReceipt.v0",
-      "sha256": "sha256:3ad5c55458a79ef502508f86cd215c746d42b4f0cc5c9aa4feeba9c03b4e1d60"
+      "sha256": "sha256:10576e0d581c624f7988a937ffaacb47775dceb166050cd957379a929af65ac3"
     },
     "trace.json": {
       "artifact_type": "LabTrust.Trace.v0",
@@ -23,8 +23,8 @@
     "trace_hash": "sha256:c3e8a3dc4ad86d533de1dfa4ae7fe2a338c2cff3c945404c96a75216524d58cd"
   },
   "schema_version": "v0",
-  "signature_or_digest": "sha256:352ae4a199281a1c03551e2dedd41eddb6465e659f563f17a8cdc192607a7dab",
-  "source_commit": "17ed831acfd775889ab497d11004cceb083a9c2d",
+  "signature_or_digest": "sha256:7adfc5945dda3368d8c8e833c015ce1d3116d5128dc2206b36a48efacef74bd7",
+  "source_commit": "8369892d8872bc08ef5acb6cf503f38665c36733",
   "source_repo": "https://github.com/fraware/LabTrust-Gym",
   "status": "Validated",
   "to_component": "CertifyEdge"

examples/pcs_qc_release/failures/certificate_id_tamper/artifacts/handoff_to_pf.json

@@ -1,5 +1,5 @@
 {
-  "created_at": "2026-05-18T21:00:43Z",
+  "created_at": "2026-05-18T23:17:38Z",
   "expected_outputs": {
     "signed_science_claim_bundle.json": {
       "artifact_type": "SignedScienceClaimBundle.v0"
@@ -14,17 +14,17 @@
   "input_artifacts": {
     "science_claim_bundle.certified.json": {
       "artifact_type": "ScienceClaimBundle.v0",
-      "sha256": "sha256:a8c5268390a35989cd504e34080e477229604ff13f6b4c69311a281a027eeede"
+      "sha256": "sha256:68d59a16ac4f5d1e6e5aff61a011be192fbb12f9b4476fa221079a934b1265fc"
     }
   },
   "invariants": {
-    "certificate_id": "cert-trace-1f02c608-8c7e-41fc-86dd-8808429cb371",
-    "certified_bundle_hash": "sha256:a8c5268390a35989cd504e34080e477229604ff13f6b4c69311a281a027eeede",
+    "certificate_id": "cert-trace-02b3a7c1-35f7-4d23-85c2-dfd60aff7693",
+    "certified_bundle_hash": "sha256:68d59a16ac4f5d1e6e5aff61a011be192fbb12f9b4476fa221079a934b1265fc",
     "trace_hash": "sha256:c3e8a3dc4ad86d533de1dfa4ae7fe2a338c2cff3c945404c96a75216524d58cd"
   },
   "schema_version": "v0",
-  "signature_or_digest": "sha256:1e1bed58050d790cb99bd892c0c405246e2e16be90c5ce1faff7ed3aa35f8f2f",
-  "source_commit": "17ed831acfd775889ab497d11004cceb083a9c2d",
+  "signature_or_digest": "sha256:081150b883dfd4ad70d3744803f30dc15f457e9d7234457b3f4045d486198367",
+  "source_commit": "8369892d8872bc08ef5acb6cf503f38665c36733",
   "source_repo": "https://github.com/fraware/LabTrust-Gym",
   "status": "Validated",
   "to_component": "Provability Fabric"

examples/pcs_qc_release/failures/certificate_id_tamper/artifacts/labtrust_release_fragment.json

@@ -2,23 +2,23 @@
   "artifacts": {
     "handoff_to_certifyedge.json": {
       "artifact_type": "HandoffManifest.v0",
-      "sha256": "sha256:0fc716f0506f182b454996fc8529ac52fff5a10d413166d1837f289ff38aec9a"
+      "sha256": "sha256:36a9b102c821dd7820c2074bb5e503d6ac2a8c6fcc255503549a41a61f5be4c1"
     },
     "handoff_to_pf.json": {
       "artifact_type": "HandoffManifest.v0",
-      "sha256": "sha256:594f3b1cdbc53f3fcd87ece5ad88ea5483e7c121379f414c8d47efd6830dbbe3"
+      "sha256": "sha256:2236bcf2eca9c9ad251267462720cd9276c816cb4f73f3984e8644f30fc799c5"
     },
     "runtime_receipt.json": {
       "artifact_type": "RuntimeReceipt.v0",
-      "sha256": "sha256:3ad5c55458a79ef502508f86cd215c746d42b4f0cc5c9aa4feeba9c03b4e1d60"
+      "sha256": "sha256:10576e0d581c624f7988a937ffaacb47775dceb166050cd957379a929af65ac3"
     },
     "science_claim_bundle.certified.json": {
       "artifact_type": "ScienceClaimBundle.v0",
-      "sha256": "sha256:a8c5268390a35989cd504e34080e477229604ff13f6b4c69311a281a027eeede"
+      "sha256": "sha256:68d59a16ac4f5d1e6e5aff61a011be192fbb12f9b4476fa221079a934b1265fc"
     },
     "science_claim_bundle.pending.json": {
       "artifact_type": "ScienceClaimBundle.v0",
-      "sha256": "sha256:406d376c6d26eb949c32f2b6c6f6578aa877f24c9ea0cb0a8b87bd377c72cfe0"
+      "sha256": "sha256:e89b0866cd25a9308f7ba70deb68e8e3c8f072b6885ca6f2e9fcaaa55706e6c7"
     },
     "trace.json": {
       "artifact_type": "LabTrust.Trace.v0",
@@ -27,7 +27,7 @@
   },
   "component": "LabTrust-Gym",
   "schema_version": "v0",
-  "signature_or_digest": "sha256:de29dc1c2ade982685b56455c5be342c0c6b7ab2d12e3d3e60904b42dff21e27",
-  "source_commit": "17ed831acfd775889ab497d11004cceb083a9c2d",
+  "signature_or_digest": "sha256:a2728a29078c80afc7d094b1678b8c35eeeb673a0ff087c14c82df051d98d6ac",
+  "source_commit": "8369892d8872bc08ef5acb6cf503f38665c36733",
   "source_repo": "https://github.com/fraware/LabTrust-Gym"
 }

examples/pcs_qc_release/failures/certificate_id_tamper/artifacts/manifest.json

@@ -1,25 +1,25 @@
 {
   "artifacts": {
-    "runtime_receipt.json": "sha256:3ad5c55458a79ef502508f86cd215c746d42b4f0cc5c9aa4feeba9c03b4e1d60",
-    "science_claim_bundle.certified.json": "sha256:a8c5268390a35989cd504e34080e477229604ff13f6b4c69311a281a027eeede",
-    "science_claim_bundle.pending.json": "sha256:406d376c6d26eb949c32f2b6c6f6578aa877f24c9ea0cb0a8b87bd377c72cfe0",
+    "runtime_receipt.json": "sha256:10576e0d581c624f7988a937ffaacb47775dceb166050cd957379a929af65ac3",
+    "science_claim_bundle.certified.json": "sha256:68d59a16ac4f5d1e6e5aff61a011be192fbb12f9b4476fa221079a934b1265fc",
+    "science_claim_bundle.pending.json": "sha256:e89b0866cd25a9308f7ba70deb68e8e3c8f072b6885ca6f2e9fcaaa55706e6c7",
     "trace.json": "sha256:f99eb0a90cd2b9819816a25ec4e938663d26ae8d40868cd8188665e940f7ad5c",
-    "trace_certificate.json": "sha256:c6cb984bf1639a25ae5a077a0677e1ec1b6346d8e5f7440fb414dd4b4886bed3"
+    "trace_certificate.json": "sha256:f25188838271cb394eeac93628d500e6b9ec9a7c0a8b7d6b0258d58790bd5c6c"
   },
-  "certificate_id": "cert-trace-1f02c608-8c7e-41fc-86dd-8808429cb371",
+  "certificate_id": "cert-trace-02b3a7c1-35f7-4d23-85c2-dfd60aff7693",
   "certificate_producer": "CertifyEdge",
   "certificate_source_repo": "https://github.com/fraware/CertifyEdge",
-  "certified_bundle_hash": "sha256:a8c5268390a35989cd504e34080e477229604ff13f6b4c69311a281a027eeede",
+  "certified_bundle_hash": "sha256:68d59a16ac4f5d1e6e5aff61a011be192fbb12f9b4476fa221079a934b1265fc",
   "certified_bundle_id": "scb-pcs-qc-release-v0.1",
   "certifyedge_bin": "C:\\Users\\mateo\\CertifyEdge\\target\\debug\\certifyedge.exe",
-  "certifyedge_commit": "635fca3771ad54fe3f8b49d1bb77ee35d0680ddc",
+  "certifyedge_commit": "11e079bc643b9e813c1a5516dc6d4db1d60a3f8a",
   "certifyedge_spec": "CertifyEdge/templates/hospital_lab/qc_release.stl",
-  "generated_at": "2026-05-18T21:00:42Z",
+  "generated_at": "2026-05-18T23:17:38Z",
   "generator": "regenerate_release_protocol",
   "handoff_id": "handoff-labtrust-qc_release_v0-1-to-pf",
-  "labtrust_gym_commit": "17ed831acfd775889ab497d11004cceb083a9c2d",
+  "labtrust_gym_commit": "8369892d8872bc08ef5acb6cf503f38665c36733",
   "mock_certificate": false,
-  "pcs_core_commit": "17e414501b3e1c58e8fbde1fe89a828440a945d9",
+  "pcs_core_commit": "5ed33a0f995df88392ee0fc849967e9c42038738",
   "schema_version": "v0",
   "trace_hash": "sha256:c3e8a3dc4ad86d533de1dfa4ae7fe2a338c2cff3c945404c96a75216524d58cd"
 }

examples/pcs_qc_release/failures/certificate_id_tamper/artifacts/runtime_receipt.json

@@ -21,8 +21,8 @@
   "run_id": "qc-release",
   "run_outcome": "passed",
   "schema_version": "v0",
-  "signature_or_digest": "sha256:b311c7e474ba4053a9c0265b8a9f13cf2a505f89d5205d19242246223cf148c5",
-  "source_commit": "17ed831acfd775889ab497d11004cceb083a9c2d",
+  "signature_or_digest": "sha256:ecce874ad042b848e57bfa54dc4ea9a5992ea351a06ed5da49e3a5c28da55d8b",
+  "source_commit": "8369892d8872bc08ef5acb6cf503f38665c36733",
   "source_repo": "https://github.com/fraware/LabTrust-Gym",
   "started_at": "2026-01-15T08:00:00Z",
   "status": "RuntimeObserved",