[ACP-HARDEN-110] Isolate scaffold output from model-check evidence by ootakazuhiko · Pull Request #3666 · itdojp/ae-framework

ootakazuhiko · 2026-07-22T08:55:42Z

Summary

keep FormalAgent, the formal MCP boundary, and the Codex adapter limited to deterministic scaffold generation with artifactStatus=draft and modelChecking.status=not-run
close Formal Summary ingestion around schema-validated formal-runner-output/v1 and formal-execution-evidence/v1 contracts
add reviewed verificationKind capability semantics and derive claim eligibility deterministically instead of trusting runner names or runner-supplied claim classes
parse SMT and SPIN semantic results fail-closed rather than treating process exit code 0 as verification success
package and validate every referenced TLC/Alloy log in model-check-results
block Codex progress when the required TLA artifact cannot be materialized while retaining optional OpenAPI failure as a non-blocking partial warning
preserve existing required-check names, report-only defaults, and the truthful scaffold/execution boundary

Five review requirements

1. Verification capability semantics

The closed evidence contract now requires verificationKind: presence | build | typecheck | conformance | model-check | proof-check.
Claim eligibility is derived from verificationKind; it is not an independently writable authority.
Producer/kind pairs are fixed in the reviewed registry.
TLC, Alloy, Apalache, semantically validated SMT, semantically validated SPIN, and reviewed CSP assertion/refinement output can enter the model lane.
Current CSP cspx:typecheck remains typecheck, current Lean lake build remains build, and Kani tool detection remains presence. None can satisfy model/proof claims.
CSP typecheck and reviewed assertion/refinement use distinct producer identities, preventing a typecheck result from self-promoting by mutating its kind.

2. SMT and SPIN semantics

SMT strictly parses one reviewed sat | unsat | unknown result token and binds solver/version/input/expected/actual/timeout/exit/log/assumptions. Success requires expected=actual; unknown, missing expectation, malformed/multiple results, timeout, nonzero exit, and mismatch are non-success.
SPIN/Pan binds errors count, trail/counterexample presence, completed search, selected LTL property, selected depth/options, timeout, and exit code. Success requires parsed completed output, zero errors, no trail/counterexample, and requested property/bounds matching actual execution.
Counterexamples remain failing execution evidence and are not rewritten as tool startup errors.

3. Referenced-log packaging

model-check-results now contains model-check.json, all *.tlc.log.txt, and all *.alloy.log.txt.
Before report publication and after artifact download, every model-check evidence log reference must be repository-relative, a regular non-symlink file, inside the expected artifact root, and present.
Missing, escaping, absolute, symlinked, or mismatched references invalidate the report contract.
Exact-head downloaded model-check artifact evidence: detected 8, executed 8, skipped 0; 5 TLC logs + 3 Alloy logs resolved and passed contract validation.
The strict Formal Verify download also resolved every actual-execution evidence log reference (7/7).

4. Required/optional materialization

TLA scaffold: required=true; OpenAPI convenience scaffold: required=false.
Required TLA write failure blocks progress with formal-primary-artifact-materialization-failed, omits nonexistent paths and checker commands, and requires materialization retry.
OpenAPI-only failure is partial, warning-only, and non-blocking.
All Codex response/UI persistence is restricted to a real repository-local directory, uses no-follow file opens, and serializes repository-relative paths only.

5. Actual label-gated Formal Verify

run-formal and enforce-formal are applied and retained on the PR.
The labeled-event run used exact head 56c36bd4dd9609bd2e3a1a81bef757a2223c2ef3.
All 9/9 runner jobs and Formal Reports Aggregate executed successfully.
Aggregate input recorded strict_formal_summary_v1: true; Enforce Formal Summary v1 JSON (strict) executed and succeeded instead of being skipped.
Formal Summary v1/v2 were generated, uploaded, and validated with --require.
Eligible model evidence was observed from TLC, Alloy, SMT, Apalache, and SPIN. CSP remained typecheck, Lean remained build, and Kani remained presence; the proof lane remained unobserved.
The exact-head model-check report recorded detected 8 / executed 8 / skipped 0 with all referenced logs resolvable.

Exact head

Start reviewed head: 6f4ac772a5c6222170b864e6d9cdf7695635b949
Current PR head: 9811a0d4240ad0a2edd6866b146750cda7780c65
Fix commits:
- 9a410d3772431dc738a2d9c3eb5f928466cf3ef6
- 97dbdb2e5d679db4e14b724f79e32cf86b6e9a44
- 60b8e637a98d123af6658d9fb8343224030740a0
- 56c36bd4dd9609bd2e3a1a81bef757a2223c2ef3
- 9811a0d4240ad0a2edd6866b146750cda7780c65 — preserve deterministic scaffold identity and metadata on repeated generation
Base: main
PR state: Ready for review

Validation

focused formal/Assurance/materialization regression suite: 20 files / 221 tests passed
final workflow/UI-summary delta: 2 files / 46 tests passed
latest review follow-up: 2 files / 7 tests passed; focused ESLint, types:check, build, and git diff --check passed
actual downloaded Formal Summary v1/v2: strict schema validation passed
actual downloaded Formal Summary → Assurance:
- model lane observed from 5 reviewed model-check producers
- proof lane observed claims: 0; CSP typecheck, Lean build, and Kani presence did not promote
actual verify:model: detected 8 / executed 8 / skipped 0; TLC 5/5, Alloy 3/3, strict enforcement passed
local build, api:check, JSON/schema validation (99 schemas), doc consistency (448 docs / 0 failures / 0 warnings), verify:lite, verify:formal, actionlint v1.7.12, public type snapshot, Context Pack, Boundary Map, and git diff --check: passed
Context Pack conflict: none

Exact-head required CI

All 6/6 required check surfaces succeeded against 9811a0d4240ad0a2edd6866b146750cda7780c65.

Exact-head Formal Verify

Strict labeled Formal Verify: exact head matched; runner jobs 9/9 success; aggregate success; strict_formal_summary_v1=true; Formal Summary v1/v2 required validation success; workflow conclusion success.
Exact-head Full CI: comprehensive workflow conclusion success; formal enforcement and downloaded model-check log-reference validation succeeded.

Compatibility impact

Formal runner outputs and execution evidence now require verificationKind; unknown producer/kind pairs and omitted/mutated kinds are rejected.
SMT/SPIN successful evidence now requires semantic-result fields, not only exit code.
CSP assertion/refinement evidence uses a distinct reviewed producer from CSP typecheck.
Model-check artifact consumers must retain the referenced TLC/Alloy log files.
Codex scaffold artifact entries now expose required and truthful per-artifact materialization state. Failed artifacts no longer expose nonexistent paths.
Existing required check names and report-only default behavior are unchanged.

Remaining limitations

Content-addressed or cryptographic binding between runner binaries, inputs, logs, and summaries remains explicitly scoped to [ACP-HARDEN-220] content-addressed artifact referenceとimplementation manifestを標準化する #3660.
Current Lean lake build does not establish the sorry/admit, proof declaration scope, or untrusted axiom policies needed for proof-check; it remains build evidence only.
Reviewed skip exceptions remain unsupported for model-check report enforcement; any detected but unexecuted model input fails strict enforcement.
GitHub Actions reports Node.js 20 action-runtime deprecation warnings; these are advisory and unrelated to the evidence-contract result.

Review status

Chat-supplied human review requirements: 5/5 implemented and strict-path validated
GitHub GraphQL unresolved review threads at start: 0
Latest Copilot review: 1/1 actionable thread fixed, replied to, and resolved in 9811a0d4240ad0a2edd6866b146750cda7780c65
GitHub GraphQL review threads at latest audit: 6 total / 0 unresolved
PR is Ready for review; Issue [ACP-HARDEN-110] FormalAgentの疑似model-check結果をAssurance経路から隔離する #3656 remains Open; no merge performed; no work started on [ACP-HARDEN-120] GitHub authority snapshotとstale-context検出を追加する #3657/[ACP-HARDEN-130] execution-result/v1を導入しstatus非変換を保証する #3658.
run-formal and enforce-formal remain applied so future commits rerun the strict path.

Refs #3656
Parent: #3655

github-actions · 2026-07-22T08:55:49Z

❓ Code Generation Drift Detection

Status:
Regeneration needed: No

Automated by AE-Framework Codegen

github-actions · 2026-07-22T08:56:24Z

🔍 Verification Summary

Traceability: 0 scenarios
- Tests: 0 (0%)
- Impl: 0 (0%)
- Formal: 0 (0%)

Unlinked (top 5)

Linked examples (up to 3)

Hit basis (tests/formal)

- Test hits: title=0 id=0 tag=0 - Formal hits: title=0 id=0 tag=0

- Model Check execution report: contract=model-check-report/v1 status=executed ok=true - Model Check (TLC): 5/5 (100%) completed modules ok

Non-OK completed modules (top 5)

- Alloy: 3/3 (100%) completed specs ok

Alloy non-OK completed executions (top 5)

- Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

github-actions · 2026-07-22T08:56:34Z

Generate Artifacts Preview

Generated at: 2026-07-22T18:03:08.529Z

tests/api/generated: clean
artifacts/codex: clean
artifacts/spec: clean

github-actions · 2026-07-22T08:56:47Z

CodeX Artifacts Summary

• Contract/E2E templates: 1 files (dir: tests/api/generated)
• Tests: PBT files=123, BDD features=0
• Formal specs: TLA=1, Alloy=1

github-actions · 2026-07-22T08:57:23Z

AE-Spec Validation Report

Status: ✅ Passed
Timestamp: 2026-07-22 18:04:01 UTC
Branch: refs/pull/3666/merge
Commit: 4d932c5

Validation Results

✅ Compilation: AE-Spec → AE-IR successful
✅ Linting: No critical issues found
✅ Structure: All required fields present

AE-IR Summary

Version: 1.0.0
Entities: 1
API Endpoints: 2
Use Cases: 1
Invariants: 0

BDD Step Lint (non-blocking)

Usecases: 1

Issues: 1

Register User: no-validation — Usecase has no validation step

github-actions · 2026-07-22T08:57:53Z

KvOnce Trace Validation

OTLP: ✅ Success (Issues: 0)
NDJSON: ✅ Success (Issues: 0)

Copilot

Pull request overview

This PR hardens the formal-evidence boundary by separating FormalAgent/Codex scaffold generation from actual model-check execution evidence, introducing a new execution-report contract for model checking, and ensuring Assurance/policy/PR summaries only count runner-reported executions.

Changes:

Remove pseudo model-check surfaces (FormalAgent/MCP/Codex/quickstart) and make scaffold output explicitly artifactStatus=draft (non-evidence).
Introduce and enforce model-check-report/v1 execution-report semantics (executed/failed/tool-error/not-run) with per-attempt provenance (tool/version/input/result/scope/assumptions).
Fail-closed / reject untrusted formal artifacts in Assurance aggregation and CI enforcement, with regression tests and updated docs.

Reviewed changes

Copilot reviewed 46 out of 49 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
tests/unit/scripts/render-codex-summary.test.ts	Asserts summary rendering ignores legacy pseudo artifacts
tests/unit/scripts/codex-quickstart-cli.test.ts	Guards quickstart stays scaffold-only (no pseudo evidence)
tests/unit/formal/run-model-checks-security.test.ts	Validates execution-report schema + status boundaries
tests/unit/formal/generate-formal-summary-v1.test.ts	Adds runner-reported executionEvidence expectations
tests/unit/ci/verify-workflow-formal-summary.test.ts	Locks workflow summary to executed-only counting
tests/unit/ci/validate-formal-summary-v2.test.ts	Enforces required fields for executionEvidence in v2
tests/unit/ci/policy-gate.test.ts	Regression: model claim blocks when evidence missing
tests/unit/agents/formal-agent.test.ts	Confirms deterministic draft scaffold + no model-check API
tests/unit/agents/codex-task-adapter.test.ts	Ensures Codex formal phase reports not-run + no model-check.json
tests/scripts/claim-evidence-manifest.test.ts	Ensures rejected formal artifacts don’t become evidence
tests/scripts/assurance-aggregate-lanes.test.ts	Rejects pseudo/draft/incomplete formal summaries from lanes
tests/agents/agent-mcp-boundary-smoke.test.ts	MCP smoke: tool list excludes model_check; draft scaffold exposed
src/self-improvement/phase3-simple.ts	Removes enableModelChecking config usage
src/self-improvement/phase3-formal-testing.ts	Removes enableModelChecking config usage
src/mcp-server/formal-server.ts	Removes model_check tool; switches listTools schemas to JSON Schema
src/agents/user-stories-task-adapter.ts	Removes enableModelChecking config usage
src/agents/ui-ux-task-adapter.ts	Removes enableModelChecking config usage
src/agents/task-types.ts	Adds structured formal scaffold vs modelChecking separation
src/agents/natural-language-task-adapter.ts	Removes enableModelChecking config usage
src/agents/formal-agent.ts	Draft-only FormalAgent; deterministic IDs; removes pseudo model checking
src/agents/domain-modeling-task-adapter.ts	Removes enableModelChecking config usage
src/agents/codex-task-adapter.ts	Stops writing pseudo model-check evidence; reports runner commands
scripts/verify/run-model-checks.mjs	Produces model-check-report/v1 execution report + per-attempt evidence
scripts/verify/render-codex-summary.mjs	Renders execution-report status; ignores legacy pseudo contracts
scripts/formal/generate-formal-summary-v1.mjs	Preserves only runner-reported executionEvidence (no backfill)
scripts/codex/quickstart.mjs	Quickstart now scaffold-only; documents checker “not run”
scripts/assurance/aggregate-lanes.mjs	Rejects untrusted formal artifacts; requires executionEvidence for promotion
schema/model-check-execution-v1.schema.json	New execution-report schema for model-check.json
schema/formal-summary-v2.schema.json	Adds executionEvidence object constraints
schema/formal-summary-v1.schema.json	Adds executionEvidence object constraints
schema/codex-task-response.schema.json	Adds formal scaffold/modelChecking structure to contract
schema/assurance-summary.schema.json	Adds warning code for untrusted-formal-summary
README.md	Documents generation vs execution boundary
package.json	Routes model-check script to the real runner
docs/verify/VERIFY-LABELS.md	Updates enforce-formal semantics (executed-only, fail-closed)
docs/verify/FORMAL-CHECKS.md	Documents ALLOY_CMD_JSON argv-safe execution + report semantics
docs/reference/CONTRACT-CATALOG.md	Adds model-check execution-report contract + evidence rules
docs/quality/formal-runbook.md	SSOT for scaffold/execution boundary + evidence eligibility
docs/phases/phase-6-uiux.md	Removes enableModelChecking mention in example config
docs/legacy/agents/formal-agent.md	Marks legacy model-check surfaces as historical/non-evidence
docs/integrations/QUICK-START-CODEX.md	Updates quickstart outputs and notes model checker not run
docs/integrations/examples/model-check.example.json	Replaces legacy pseudo example with not-run execution report
docs/integrations/CODEX-INTEGRATION.md	Updates formal phase behavior description (scaffold-only)
docs/integrations/CODEX-ARTIFACTS.md	Clarifies scaffold vs actual model-check artifacts and semantics
docs/agents/commands.md	Updates lastVerified stamp
artifacts/types/src/agents/formal-agent.d.ts	Updates public typings: draft-only, no runModelChecking
artifacts/reference/types/public-types.current.d.ts	Updates public type snapshot for FormalAgent changes
api/public-types.d.ts	Updates public-types snapshot SHA and FormalAgent types
.github/workflows/verify.yml	Summary/enforcement counts only completed executed results; adds Alloy version

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

ootakazuhiko

Independent review found four remaining blockers in the truthful formal-evidence boundary. The PR should remain Draft until the inline items are addressed and exact-head CI is rerun.

github-actions · 2026-07-22T12:39:53Z

❓ Code Generation Drift Detection

Status:
Regeneration needed: No

Automated by AE-Framework Codegen

github-actions · 2026-07-22T12:40:10Z

Cedar Policies (report-only)

Files: 1 (json=0, cedar=0)
Results: ok=0, ng=0
Tool: cedar-validator

Policy: report-only
Docs: docs/quality/cedar-quality-gates.md

github-actions · 2026-07-22T12:40:35Z

🔍 Verification Summary

Traceability: 0 scenarios
- Tests: 0 (0%)
- Impl: 0 (0%)
- Formal: 0 (0%)

Unlinked (top 5)

Linked examples (up to 3)

Hit basis (tests/formal)

- Test hits: title=0 id=0 tag=0 - Formal hits: title=0 id=0 tag=0

- Model Check execution report: contract=model-check-report/v1 status=executed ok=true - Model Check (TLC): 5/5 (100%) completed modules ok

Non-OK completed modules (top 5)

- Alloy: 3/3 (100%) completed specs ok

Alloy non-OK completed executions (top 5)

- Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

github-actions · 2026-07-22T12:40:43Z

CodeX Artifacts Summary

• Contract/E2E templates: 1 files (dir: tests/api/generated)
• Tests: PBT files=123, BDD features=0
• Formal specs: TLA=1, Alloy=1

github-actions · 2026-07-22T14:37:52Z

❓ Code Generation Drift Detection

Status:
Regeneration needed: No

Automated by AE-Framework Codegen

github-actions · 2026-07-22T14:38:01Z

❓ Code Generation Drift Detection

Status:
Regeneration needed: No

Automated by AE-Framework Codegen

github-actions · 2026-07-22T14:38:33Z

🔍 Verification Summary

Traceability: 0 scenarios
- Tests: 0 (0%)
- Impl: 0 (0%)
- Formal: 0 (0%)

Unlinked (top 5)

Linked examples (up to 3)

Hit basis (tests/formal)

- Test hits: title=0 id=0 tag=0 - Formal hits: title=0 id=0 tag=0

- Model Check execution report: contract=model-check-report/v1 status=executed ok=true - Model Check (TLC): 5/5 (100%) completed modules ok

Non-OK completed modules (top 5)

- Alloy: 3/3 (100%) completed specs ok

Alloy non-OK completed executions (top 5)

- Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

github-actions · 2026-07-22T14:38:42Z

🔍 Verification Summary

Traceability: 0 scenarios
- Tests: 0 (0%)
- Impl: 0 (0%)
- Formal: 0 (0%)

Unlinked (top 5)

Linked examples (up to 3)

Hit basis (tests/formal)

- Test hits: title=0 id=0 tag=0 - Formal hits: title=0 id=0 tag=0

- Model Check execution report: contract=model-check-report/v1 status=executed ok=true - Model Check (TLC): 5/5 (100%) completed modules ok

Non-OK completed modules (top 5)

- Alloy: 3/3 (100%) completed specs ok

Alloy non-OK completed executions (top 5)

- Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

github-actions · 2026-07-22T14:38:48Z

CodeX Artifacts Summary

• Contract/E2E templates: 1 files (dir: tests/api/generated)
• Tests: PBT files=123, BDD features=0
• Formal specs: TLA=1, Alloy=1

github-actions · 2026-07-22T14:40:21Z

❓ Code Generation Drift Detection

Status:
Regeneration needed: No

Automated by AE-Framework Codegen

github-actions · 2026-07-22T14:41:55Z

🔍 Verification Summary

Traceability: 0 scenarios
- Tests: 0 (0%)
- Impl: 0 (0%)
- Formal: 0 (0%)

Unlinked (top 5)

Linked examples (up to 3)

Hit basis (tests/formal)

- Test hits: title=0 id=0 tag=0 - Formal hits: title=0 id=0 tag=0

- Model Check execution report: contract=model-check-report/v1 status=executed ok=true - Model Check (TLC): 5/5 (100%) completed modules ok

Non-OK completed modules (top 5)

- Alloy: 3/3 (100%) completed specs ok

Alloy non-OK completed executions (top 5)

- Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

github-actions · 2026-07-22T14:42:09Z

CodeX Artifacts Summary

• Contract/E2E templates: 1 files (dir: tests/api/generated)
• Tests: PBT files=123, BDD features=0
• Formal specs: TLA=1, Alloy=1

github-actions · 2026-07-22T14:46:26Z

❓ Code Generation Drift Detection

Status:
Regeneration needed: No

Automated by AE-Framework Codegen

github-actions · 2026-07-22T14:48:08Z

🔍 Verification Summary

Traceability: 0 scenarios
- Tests: 0 (0%)
- Impl: 0 (0%)
- Formal: 0 (0%)

Unlinked (top 5)

Linked examples (up to 3)

Hit basis (tests/formal)

- Test hits: title=0 id=0 tag=0 - Formal hits: title=0 id=0 tag=0

- Model Check execution report: contract=model-check-report/v1 status=executed ok=true - Model Check (TLC): 5/5 (100%) completed modules ok

Non-OK completed modules (top 5)

- Alloy: 3/3 (100%) completed specs ok

Alloy non-OK completed executions (top 5)

- Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

github-actions · 2026-07-22T14:48:23Z

CodeX Artifacts Summary

• Contract/E2E templates: 1 files (dir: tests/api/generated)
• Tests: PBT files=123, BDD features=0
• Formal specs: TLA=1, Alloy=1

github-actions · 2026-07-22T14:48:37Z

❓ Code Generation Drift Detection

Status:
Regeneration needed: No

Automated by AE-Framework Codegen

github-actions · 2026-07-22T14:50:20Z

🔍 Verification Summary

Traceability: 0 scenarios
- Tests: 0 (0%)
- Impl: 0 (0%)
- Formal: 0 (0%)

Unlinked (top 5)

Linked examples (up to 3)

Hit basis (tests/formal)

- Test hits: title=0 id=0 tag=0 - Formal hits: title=0 id=0 tag=0

- Model Check execution report: contract=model-check-report/v1 status=executed ok=true - Model Check (TLC): 5/5 (100%) completed modules ok

Non-OK completed modules (top 5)

- Alloy: 3/3 (100%) completed specs ok

Alloy non-OK completed executions (top 5)

- Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

github-actions · 2026-07-22T14:50:29Z

CodeX Artifacts Summary

• Contract/E2E templates: 1 files (dir: tests/api/generated)
• Tests: PBT files=123, BDD features=0
• Formal specs: TLA=1, Alloy=1

github-actions · 2026-07-22T16:03:17Z

❓ Code Generation Drift Detection

Status:
Regeneration needed: No

Automated by AE-Framework Codegen

github-actions · 2026-07-22T16:04:03Z

🔍 Verification Summary

Traceability: 0 scenarios
- Tests: 0 (0%)
- Impl: 0 (0%)
- Formal: 0 (0%)

Unlinked (top 5)

Linked examples (up to 3)

Hit basis (tests/formal)

- Test hits: title=0 id=0 tag=0 - Formal hits: title=0 id=0 tag=0

- Model Check execution report: contract=model-check-report/v1 status=executed ok=true - Model Check (TLC): 5/5 (100%) completed modules ok

Non-OK completed modules (top 5)

- Alloy: 3/3 (100%) completed specs ok

Alloy non-OK completed executions (top 5)

- Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

ootakazuhiko · 2026-07-22T16:11:59Z

Human review response summary — five requested corrections

All five chat-supplied human review requirements have been implemented and validated on exact head 56c36bd4dd9609bd2e3a1a81bef757a2223c2ef3.

Verification capability semantics — the closed runner contract now fixes reviewed producer/verificationKind pairs and derives claim eligibility from the kind. TLC, Alloy, Apalache, semantically validated SMT, and semantically validated SPIN are model evidence; CSP typecheck, Lean build, and Kani presence are retained as execution records without model/proof promotion.
SMT semantic parsing — strict single-token sat | unsat | unknown parsing binds expected and actual results; missing expectation, unknown, malformed/multiple results, mismatch, timeout, and nonzero exit fail closed.
SPIN semantic parsing — Pan output now binds errors, trail/counterexample, completed search, property, depth/options, timeout, and exit code. Unparsed or mismatched output and counterexamples remain failing execution evidence.
Referenced-log materialization — model-check-results contains model-check.json, five TLC logs, and three Alloy logs. The downloaded exact-head artifact resolved all 8/8 model-check references; the strict Formal Verify download resolved all 7/7 actual-execution evidence references.
Primary materialization blocking — TLA is required=true and a failed write blocks progress without a nonexistent path or checker next action. OpenAPI is optional; an OpenAPI-only failure is partial and non-blocking.

Exact fix commits

9a410d3772431dc738a2d9c3eb5f928466cf3ef6 — capability/semantic-result contracts, runner adapters, log contract, Assurance mapping, and negative/E2E tests
97dbdb2e5d679db4e14b724f79e32cf86b6e9a44 — required/optional Codex materialization and path hardening
60b8e637a98d123af6658d9fb8343224030740a0 — execute aggregate for pull-request callers
56c36bd4dd9609bd2e3a1a81bef757a2223c2ef3 — install aggregate dependencies before summary generation/validation

Validation

Focused formal/Assurance/materialization suite: 20 files / 221 tests passed
Final workflow/UI-summary delta: 2 files / 46 tests passed
Full local validation: build, API snapshot, 99 schemas, doc consistency (448 docs / 0 failures / 0 warnings), verify:lite, verify:formal, actionlint, public type snapshot, Context Pack, Boundary Map, and git diff --check passed
Exact-head model-check enforcement: detected 8, executed 8, skipped 0; TLC 5/5, Alloy 3/3
Required CI: 6/6 success on the exact head
Strict exact-head Formal Verify: all 9/9 runner jobs and aggregate succeeded; strict_formal_summary_v1: true; strict Formal Summary v1/v2 required validation succeeded
Assurance audit: 5 eligible model-check producers observed; proof lane observed claims 0; CSP typecheck, Lean build, and Kani presence were not promoted

run-formal and enforce-formal remain applied. The PR remains Draft and Issue #3656 remains Open.

Remaining limitations

Content-addressed/cryptographic runner-input-log-summary binding remains scoped to [ACP-HARDEN-220] content-addressed artifact referenceとimplementation manifestを標準化する #3660.
Current Lean lake build remains build evidence; proof-check eligibility still requires reviewed sorry/admit, declaration-scope, axiom, and checker policies.
Model-check skip exceptions are unsupported; any detected but unexecuted input fails strict enforcement.
GitHub Actions Node.js 20 action-runtime deprecation warnings remain advisory.

github-actions · 2026-07-22T17:28:10Z

🔍 Verification Summary

Traceability: 0 scenarios
- Tests: 0 (0%)
- Impl: 0 (0%)
- Formal: 0 (0%)

Unlinked (top 5)

Linked examples (up to 3)

Hit basis (tests/formal)

- Test hits: title=0 id=0 tag=0 - Formal hits: title=0 id=0 tag=0

- Model Check execution report: contract=model-check-report/v1 status=executed ok=true - Model Check (TLC): 5/5 (100%) completed modules ok

Non-OK completed modules (top 5)

- Alloy: 3/3 (100%) completed specs ok

Alloy non-OK completed executions (top 5)

- Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

github-actions · 2026-07-22T17:28:15Z

CodeX Artifacts Summary

• Contract/E2E templates: 1 files (dir: tests/api/generated)
• Tests: PBT files=123, BDD features=0
• Formal specs: TLA=1, Alloy=1

Copilot

Pull request overview

Copilot reviewed 79 out of 83 changed files in this pull request and generated 1 comment.

github-actions · 2026-07-22T18:02:29Z

❓ Code Generation Drift Detection

Status:
Regeneration needed: No

Automated by AE-Framework Codegen

github-actions · 2026-07-22T18:03:11Z

🔍 Verification Summary

Traceability: 0 scenarios
- Tests: 0 (0%)
- Impl: 0 (0%)
- Formal: 0 (0%)

Unlinked (top 5)

Linked examples (up to 3)

Hit basis (tests/formal)

- Test hits: title=0 id=0 tag=0 - Formal hits: title=0 id=0 tag=0

- Model Check execution report: contract=model-check-report/v1 status=executed ok=true - Model Check (TLC): 5/5 (100%) completed modules ok

Non-OK completed modules (top 5)

- Alloy: 3/3 (100%) completed specs ok

Alloy non-OK completed executions (top 5)

- Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

github-actions · 2026-07-22T18:03:26Z

CodeX Artifacts Summary

• Contract/E2E templates: 1 files (dir: tests/api/generated)
• Tests: PBT files=123, BDD features=0
• Formal specs: TLA=1, Alloy=1

ootakazuhiko · 2026-07-25T10:09:36Z

Solo-maintainer merge decision

Exact head reviewed: 9811a0d4240ad0a2edd6866b146750cda7780c65
Independent human reviewer: unavailable; this is a one-human-maintainer project
AI/Copilot reviews: advisory Evidence only, not human approval
Required checks: successful on the exact head
Strict Formal Verify: successful on the exact head
Review threads: resolved
Repository governance change: required approving reviews changed from 1 to 0 to remove a structural solo-maintainer deadlock
Human decision: the authorized maintainer approves this exact head for regular merge
Residual limitation: no independent human review was performed

This decision does not represent AI review as human approval.

fix(formal): separate scaffolds from checker evidence

c070738

ootakazuhiko requested a review from Copilot July 22, 2026 08:56

Copilot started reviewing on behalf of ootakazuhiko July 22, 2026 08:56 View session

Copilot AI reviewed Jul 22, 2026

View reviewed changes

ootakazuhiko commented Jul 22, 2026

View reviewed changes

fix(formal): close runner evidence contract

6f4ac77

ootakazuhiko added 2 commits July 22, 2026 23:34

fix(formal): bind verification capabilities to evidence

9a410d3

fix(codex): constrain response artifact writes

97dbdb2

ootakazuhiko added the run-formal Run formal verify jobs on PR label Jul 22, 2026

ootakazuhiko added 2 commits July 22, 2026 23:43

fix(ci): run formal aggregate for PR callers

60b8e63

fix(ci): install formal aggregate dependencies

56c36bd

ootakazuhiko added the enforce-formal Enable strict formal verification enforcement label Jul 22, 2026

ootakazuhiko marked this pull request as ready for review July 22, 2026 17:27

ootakazuhiko requested a review from Copilot July 22, 2026 17:31

Copilot started reviewing on behalf of ootakazuhiko July 22, 2026 17:31 View session

Copilot AI reviewed Jul 22, 2026

View reviewed changes

Comment thread src/agents/formal-agent.ts

fix(formal): preserve deterministic scaffold metadata

9811a0d

ootakazuhiko merged commit 6f6d9b6 into main Jul 25, 2026
125 of 126 checks passed

ootakazuhiko deleted the codex/3656-formal-truthful-results branch July 25, 2026 10:09

This was referenced Jul 25, 2026

[ACP-HARDEN-110] FormalAgentの疑似model-check結果をAssurance経路から隔離する #3656

Closed

[ACP-HARDEN-100] Epic: Private Match dogfoodからのAssurance Control Plane hardening実行計画 #3655

Open

Uh oh!

Conversation

ootakazuhiko commented Jul 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Five review requirements

1. Verification capability semantics

2. SMT and SPIN semantics

3. Referenced-log packaging

4. Required/optional materialization

5. Actual label-gated Formal Verify

Exact head

Validation

Exact-head required CI

Exact-head Formal Verify

Compatibility impact

Remaining limitations

Review status

Uh oh!

github-actions Bot commented Jul 22, 2026

❓ Code Generation Drift Detection

Uh oh!

github-actions Bot commented Jul 22, 2026

🔍 Verification Summary

Uh oh!

github-actions Bot commented Jul 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Generate Artifacts Preview

Uh oh!

github-actions Bot commented Jul 22, 2026

CodeX Artifacts Summary

Uh oh!

github-actions Bot commented Jul 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

AE-Spec Validation Report

Validation Results

AE-IR Summary

BDD Step Lint (non-blocking)

Uh oh!

github-actions Bot commented Jul 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

KvOnce Trace Validation

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

ootakazuhiko left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions Bot commented Jul 22, 2026

❓ Code Generation Drift Detection

Uh oh!

github-actions Bot commented Jul 22, 2026

Cedar Policies (report-only)

Uh oh!

github-actions Bot commented Jul 22, 2026

🔍 Verification Summary

Uh oh!

github-actions Bot commented Jul 22, 2026

CodeX Artifacts Summary

Uh oh!

github-actions Bot commented Jul 22, 2026

❓ Code Generation Drift Detection

Uh oh!

github-actions Bot commented Jul 22, 2026

❓ Code Generation Drift Detection

Uh oh!

github-actions Bot commented Jul 22, 2026

🔍 Verification Summary

Uh oh!

github-actions Bot commented Jul 22, 2026

🔍 Verification Summary

Uh oh!

ootakazuhiko commented Jul 22, 2026 •

edited

Loading

github-actions Bot commented Jul 22, 2026 •

edited

Loading

github-actions Bot commented Jul 22, 2026 •

edited

Loading

github-actions Bot commented Jul 22, 2026 •

edited

Loading