ci(formal): consolidate formal aggregate entry

[ootakazuhiko]

Summary\n- make formal-aggregate reusable and route PR aggregation through formal-verify\n- pass source run id + PR number for artifact download and comment upsert\n- keep manual dispatch by allowing run id input\n\n## Testing\n- not run (workflow change)

[github-actions]

❓ Code Generation Drift Detection

Status:
Regeneration needed: No

---

Automated by AE-Framework Codegen

[github-actions]

Quality Summary

• Adapters:

• Formal: n/a

• Replay: n/a

• Trace IDs:

[github-actions]

🔍 Verification Summary

• Traceability: 6 scenarios
  • Tests: 3 (50%)
  • Impl: 3 (50%)
  • Formal: 3 (50%)

Unlinked (top 5)

- Device registration publishes enough pre-keys and emits audit log (id: device-registration-publishes-enough-pre-keys-and-emits-audit-log) test:N/A impl:N/A formal:N/A - Invalid auth tag triggers audit violation for AES-GCM envelopes (id: invalid-auth-tag-triggers-audit-violation-for-aes-gcm-envelopes) test:N/A impl:N/A formal:N/A - Session rotation stays within forward secrecy thresholds (id: session-rotation-stays-within-forward-secrecy-thresholds) test:N/A impl:N/A formal:N/A

Linked examples (up to 3)

- Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/2c7a516e86a0cf5fad7efa12f27079b7449cb796/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/2c7a516e86a0cf5fad7efa12f27079b7449cb796/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/2c7a516e86a0cf5fad7efa12f27079b7449cb796/specs/formal/tla+/Inventory.tla) - Prevent negative stock (id: prevent-negative-stock) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/2c7a516e86a0cf5fad7efa12f27079b7449cb796/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/2c7a516e86a0cf5fad7efa12f27079b7449cb796/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/2c7a516e86a0cf5fad7efa12f27079b7449cb796/specs/formal/tla+/Inventory.tla) - Idempotent by order id (id: idempotent-by-order-id) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/2c7a516e86a0cf5fad7efa12f27079b7449cb796/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/2c7a516e86a0cf5fad7efa12f27079b7449cb796/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/2c7a516e86a0cf5fad7efa12f27079b7449cb796/specs/formal/tla+/Inventory.tla)

Hit basis (tests/formal)

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

- Model Check (TLC): 2/8 (25%) modules ok

Non-OK modules (top 5)

- KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt) - KvOnceImpl (log: artifacts/codex/KvOnceImpl.tlc.log.txt) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt)

- Alloy: detected 2 specs (execution skipped) - Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

[github-actions]

CodeX Artifacts Summary

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

[Copilot]

Pull request overview

This PR consolidates the “formal aggregate” workflow into a reusable workflow and routes PR aggregation through formal-verify, passing metadata needed to download artifacts and (optionally) upsert a PR comment.

Changes:

• Adds a formal-aggregate reusable workflow invocation to formal-verify after all verify jobs complete.
• Converts formal-aggregate.yml from a pull_request workflow to a workflow_call + workflow_dispatch workflow, with inputs for source_run_id and pr_number.
• Updates artifact download and PR comment upsert logic to use the provided run id / PR number.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.

File	Description
.github/workflows/formal-verify.yml	Adds a formal-aggregate job that calls the reusable aggregator after formal verification jobs.
.github/workflows/formal-aggregate.yml	Refactors the aggregator into a reusable workflow and updates artifact download/commenting to be driven by inputs.

---

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

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 2c7a516e86

ℹ️ About Codex in GitHub

Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

[github-actions]

CI Status Snapshot (2026-01-27T12:03:10.545Z)

• ci(formal): consolidate formal aggregate entry #1788 ci(formal): consolidate formal aggregate entry | ✅22 ❌2 ⏳0 ⏭️26 | review:NONE | mergeable:MERGEABLE
  • failed: gate, gate

[ootakazuhiko]

レビューコメント対応しました。

• download-artifact の token 指摘: github-token: ${{ secrets.GITHUB_TOKEN || github.token }} に変更。
• workflow_dispatch でのPRコメント: workflow_dispatch でも pr_number が指定されていれば upsert する条件に拡張。
• aggregation が skip される指摘: formal-aggregate を if: always() に変更して、verify の一部が skip/fail でも集計が走るように調整。

コンフリクトはありません（mergeable）。

[github-actions]

❓ Code Generation Drift Detection

Status:
Regeneration needed: No

---

Automated by AE-Framework Codegen

[github-actions]

🔍 Verification Summary

• Traceability: 6 scenarios
  • Tests: 3 (50%)
  • Impl: 3 (50%)
  • Formal: 3 (50%)

Unlinked (top 5)

- Device registration publishes enough pre-keys and emits audit log (id: device-registration-publishes-enough-pre-keys-and-emits-audit-log) test:N/A impl:N/A formal:N/A - Invalid auth tag triggers audit violation for AES-GCM envelopes (id: invalid-auth-tag-triggers-audit-violation-for-aes-gcm-envelopes) test:N/A impl:N/A formal:N/A - Session rotation stays within forward secrecy thresholds (id: session-rotation-stays-within-forward-secrecy-thresholds) test:N/A impl:N/A formal:N/A

Linked examples (up to 3)

- Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/02afd9e30745ebb3a42ee11f5cbdb357dfce8b07/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/02afd9e30745ebb3a42ee11f5cbdb357dfce8b07/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/02afd9e30745ebb3a42ee11f5cbdb357dfce8b07/specs/formal/tla+/Inventory.tla) - Prevent negative stock (id: prevent-negative-stock) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/02afd9e30745ebb3a42ee11f5cbdb357dfce8b07/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/02afd9e30745ebb3a42ee11f5cbdb357dfce8b07/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/02afd9e30745ebb3a42ee11f5cbdb357dfce8b07/specs/formal/tla+/Inventory.tla) - Idempotent by order id (id: idempotent-by-order-id) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/02afd9e30745ebb3a42ee11f5cbdb357dfce8b07/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/02afd9e30745ebb3a42ee11f5cbdb357dfce8b07/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/02afd9e30745ebb3a42ee11f5cbdb357dfce8b07/specs/formal/tla+/Inventory.tla)

Hit basis (tests/formal)

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

- Model Check (TLC): 2/8 (25%) modules ok

Non-OK modules (top 5)

- KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt) - KvOnceImpl (log: artifacts/codex/KvOnceImpl.tlc.log.txt) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt)

- Alloy: detected 2 specs (execution skipped) - Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

[github-actions]

CodeX Artifacts Summary

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

[ootakazuhiko]

レビュー本文（Copilot/Codex）は概要のみで追加対応不要と判断しました。インライン指摘は対応済みです。