Include threat-detection credits in forecast totals, expose monthly low/high/stdev, and fix formal-verifier tool denials

.github/workflows/daily-formal-spec-verifier.md

@@ -45,6 +45,7 @@ tools:
     - "cat specs/*.md"
     - "find . -name \"*_test.go\" -path \"*/pkg/*\" | head -20"
     - "cat pkg/workflow/*.go | head -200"
+    - "cat pkg/cli/*.go"
 
 safe-outputs:
   mentions: false

actions/setup/js/create_forecast_issue.cjs

@@ -70,6 +70,21 @@ function monthlyCost(workflow) {
   return Number(workflow?.monthly_monte_carlo?.p50_projected_aic ?? workflow?.monthly_projected_aic ?? 0);
 }
 
+/**
+ * @param {Record<string, any>} workflow
+ * @returns {{low:number,p50:number,high:number,stddev:number}}
+ */
+function getMonthlyForecastStats(workflow) {
+  const monthlyMonteCarlo = workflow?.monthly_monte_carlo;
+  const monthlyProjected = workflow?.monthly_projected_aic ?? 0;
+  return {
+    low: toFiniteNumber(monthlyMonteCarlo?.p10_projected_aic ?? monthlyProjected),
+    p50: toFiniteNumber(monthlyMonteCarlo?.p50_projected_aic ?? monthlyProjected),
+    high: toFiniteNumber(monthlyMonteCarlo?.p90_projected_aic ?? monthlyProjected),
+    stddev: toFiniteNumber(monthlyMonteCarlo?.std_dev_aic ?? 0),
+  };
+}
+
 /**
  * @param {Record<string, any>} workflow
  * @returns {number}
@@ -89,11 +104,11 @@ function buildForecastIssueBody(report, options) {
 
   const categorized = workflows.map(workflow => {
     const p50PerRun = toFiniteNumber(workflow?.p50_aic_per_run);
-    const monthlyP50 = toFiniteNumber(workflow?.monthly_monte_carlo?.p50_projected_aic ?? workflow?.monthly_projected_aic);
-    const hasForecastData = [p50PerRun, monthlyP50].some(hasPositiveAIC);
+    const monthly = getMonthlyForecastStats(workflow);
+    const hasForecastData = [p50PerRun, monthly.p50, monthly.high, monthly.low].some(hasPositiveAIC);
     return {
       workflow,
-      row: [renderWorkflowLink(workflow, options), toFiniteNumber(workflow.sampled_runs), p50PerRun, monthlyP50],
+      row: [renderWorkflowLink(workflow, options), toFiniteNumber(workflow.sampled_runs), p50PerRun, monthly.low, monthly.p50, monthly.high, monthly.stddev],
       hasForecastData,
     };
   });
@@ -117,7 +132,7 @@ function buildForecastIssueBody(report, options) {
         return !hasPositiveAIC(p50);
       });
 
-  const allMonthlyZero = tableRows.length > 0 && tableRows.every(([, , , monthly]) => Number(monthly) === 0);
+  const allMonthlyZero = tableRows.length > 0 && tableRows.every(([, , , , monthlyP50]) => Number(monthlyP50) === 0);
   const allProjectedZero = legacyRows ? legacyRows.length > 0 && legacyRows.every(([, , p50]) => Number(p50) === 0) : allMonthlyZero;
 
   let reportTable;
@@ -130,12 +145,15 @@ function buildForecastIssueBody(report, options) {
     if (tableRows.length === 0) {
       reportTable = "_No forecast rows were produced._";
     } else {
-      const totalMonthly = tableRows.reduce((s, [, , , m]) => s + Number(m), 0);
-      const dataRows = tableRows.map(([workflowID, sampledRuns, p50Run, monthly]) => `| ${workflowID} | ${sampledRuns} | ${formatAIC(p50Run)} | ${formatAIC(monthly)} |`);
+      const totalMonthly = tableRows.reduce((s, [, , , , monthly]) => s + Number(monthly), 0);
+      const dataRows = tableRows.map(
+        ([workflowID, sampledRuns, p50Run, monthlyLow, monthlyP50, monthlyHigh, monthlyStdDev]) =>
+          `| ${workflowID} | ${sampledRuns} | ${formatAIC(p50Run)} | ${formatAIC(monthlyLow)} | ${formatAIC(monthlyP50)} | ${formatAIC(monthlyHigh)} | ${formatAIC(monthlyStdDev)} |`
+      );
       if (tableRows.length > 1) {
-        dataRows.push(`| **TOTAL** | | | **${formatAIC(totalMonthly)}** |`);
+        dataRows.push(`| **TOTAL** | | | | **${formatAIC(totalMonthly)}** | | |`);
       }
-      reportTable = ["| Workflow | Runs | P50/Run | Monthly (P50) |", "| --- | ---: | ---: | ---: |", ...dataRows].join("\n");
+      reportTable = ["| Workflow | Runs | P50/Run | Monthly (Low) | Monthly (P50) | Monthly (High) | Monthly (Stdev) |", "| --- | ---: | ---: | ---: | ---: | ---: | ---: |", ...dataRows].join("\n");
     }
   }
   const withoutDataWorkflows = legacyRows ? legacyNoDataWorkflows : workflowsWithoutData;
@@ -166,8 +184,9 @@ function buildForecastIssueBody(report, options) {
           "### How to read this report",
           "",
           "- **P50/Run** is the median per-run AIC from sampled historical runs.",
-          "- **Monthly (P50)** is the Monte Carlo median of total AIC over 30 days.",
-          "- Monthly values are distribution medians, not a direct `P50/Run × runs` multiplication.",
+          "- **Monthly (Low/P50/High)** are the Monte Carlo P10 / P50 / P90 total-AIC bounds over 30 days.",
+          "- **Monthly (Stdev)** is the Monte Carlo standard deviation of the 30-day total-AIC distribution.",
+          "- Monthly values come from the Monte Carlo distribution and are not a direct `P50/Run × runs` multiplication.",
           "",
         ].join("\n");
 

actions/setup/js/create_forecast_issue.test.cjs

@@ -66,7 +66,12 @@ describe("create_forecast_issue", () => {
             p50_aic_per_run: 4000,
             p95_aic_per_run: 8000,
             weekly_monte_carlo: { p50_projected_aic: 12345.6 },
-            monthly_monte_carlo: { p50_projected_aic: 52000 },
+            monthly_monte_carlo: {
+              p10_projected_aic: 48000,
+              p50_projected_aic: 52000,
+              p90_projected_aic: 61000,
+              std_dev_aic: 3210,
+            },
           },
           {
             workflow_id: "wf-b",
@@ -89,13 +94,15 @@ describe("create_forecast_issue", () => {
       }
     );
 
-    expect(body).toContain("| Workflow | Runs | P50/Run | Monthly (P50) |");
-    expect(body).toContain("| [wf\\|a](https://github.com/octo/repo/actions/workflows/.github%2Fworkflows%2Fwf-a.yml) | 3 | 4,000 | 52,000 |");
+    expect(body).toContain("| Workflow | Runs | P50/Run | Monthly (Low) | Monthly (P50) | Monthly (High) | Monthly (Stdev) |");
+    expect(body).toContain("| [wf\\|a](https://github.com/octo/repo/actions/workflows/.github%2Fworkflows%2Fwf-a.yml) | 3 | 4,000 | 48,000 | 52,000 | 61,000 | 3,210 |");
     expect(body).toContain("### AW without data");
     expect(body).toContain("| [wf-b](https://github.com/octo/repo/actions/workflows/.github%2Fworkflows%2Fwf-b.yml) | 0 |");
     expect(body).toContain("AIC = 0 is treated as missing data and excluded from forecast computation.");
     expect(body).toContain("### How to read this report");
-    expect(body).toContain("Monthly values are distribution medians");
+    expect(body).toContain("Monte Carlo P10 / P50 / P90 total-AIC bounds");
+    expect(body).toContain("Monte Carlo standard deviation");
+    expect(body).toContain("Monthly values come from the Monte Carlo distribution");
     expect(body).toContain("_Forecast source run: [#123456](https://github.com/octo/repo/actions/runs/123456)._");
     expect(body).toContain("Consult the billing dashboards for accurate usage and charges.");
     expect(body).not.toContain("sampled runs but forecast AIC is 0");
@@ -125,7 +132,7 @@ describe("create_forecast_issue", () => {
       }
     );
 
-    expect(body).toContain("| wf-round | 1 | 2 | 5 |");
+    expect(body).toContain("| wf-round | 1 | 2 | 5 | 5 | 5 | 0 |");
   });
 
   it("lists workflows without data when every projected AIC is zero", async () => {
@@ -279,7 +286,7 @@ describe("create_forecast_issue", () => {
       }
     );
 
-    expect(body).toContain("| **TOTAL** | | | **42,000** |");
+    expect(body).toContain("| **TOTAL** | | | | **42,000** | | |");
   });
 
   it("sorts workflows by monthly cost descending", async () => {

docs/adr/39101-aggregate-usage-artifact-files-for-forecast-aic.md

@@ -0,0 +1,71 @@
+# ADR-39101: Aggregate All Usage-Artifact JSONL Files for Forecast AIC
+
+**Date**: 2026-06-13
+**Status**: Draft
+**Deciders**: Unknown (generated from PR #39101)
+
+---
+
+## Part 1 — Narrative (Human-Friendly)
+
+### Context
+
+The cost-forecast pipeline computes per-run AI Credit (AIC) cost from a single token-usage file produced by the main agent. As workflows began spending AIC in threat-detection steps, that spend was recorded in separate usage records inside the compact `usage` artifact and was never read by the forecast loader, so forecast totals silently undercounted real cost. The forecast issue also exposed only a single monthly P50 figure, hiding the spread of the Monte Carlo projection from anyone trying to reason about worst-case monthly spend.
+
+### Decision
+
+We will compute forecast AIC by aggregating **every** `.jsonl` file under a run's `usage` artifact directory rather than reading only the main agent usage file. For each record we prefer an explicit credit value (`ai_credits`/`aic`) and otherwise recompute AIC from raw token counts via `computeModelInferenceAIC`. When no usage-directory files are present we fall back to the existing single-file path, preserving backward compatibility. We will also widen the forecast report from a single `Monthly (P50)` column to `Monthly (Low/P50/High/Stdev)` derived from the Monte Carlo distribution.
+
+### Alternatives Considered
+
+#### Alternative 1: Keep reading only the main agent usage file
+
+The status quo. Rejected because it structurally cannot see detection spend, which lives in sibling records within the `usage` artifact — the very gap that motivated this change. No amount of per-run scaling fixes an input that omits a cost source.
+
+#### Alternative 2: Pre-aggregate AIC upstream into one summed file
+
+Have the artifact producer emit a single pre-summed usage file the forecast loader reads as-is. Rejected for this change because it pushes cost-summation and AIC-recomputation logic into artifact generation, couples the forecast format to the producer, and is a larger blast radius than reading the files that already exist. Reading the directory keeps the forecast loader as the single owner of AIC computation.
+
+### Consequences
+
+#### Positive
+- Forecast totals now include threat-detection credits, eliminating the documented undercount.
+- Both explicit-credit and token-only usage records are handled, so detection records missing `ai_credits` still contribute cost via recomputation.
+- The widened report surfaces low/high/stdev, letting readers gauge projection spread, not just the median.
+
+#### Negative
+- The loader now walks the entire `usage` directory per run, adding filesystem I/O and a `filepath.Walk` traversal that scales with artifact file count.
+- Per-record precedence logic (`ai_credits` → `aic` → recomputed) adds branching that must stay in sync with the artifact record shape; a renamed field would silently zero a cost source.
+- The forecast issue table is wider, consuming more horizontal space in the rendered report.
+
+#### Neutral
+- Behavior is unchanged for runs without a `usage` directory; the single-file path remains the fallback.
+- Sorting and totals stay centered on monthly P50, so report ranking is unaffected by the added columns.
+
+---
+
+## Part 2 — Normative Specification (RFC 2119)
+
+> The key words **MUST**, **MUST NOT**, **REQUIRED**, **SHALL**, **SHALL NOT**, **SHOULD**, **SHOULD NOT**, **RECOMMENDED**, **MAY**, and **OPTIONAL** in this section are to be interpreted as described in [RFC 2119](https://www.rfc-editor.org/rfc/rfc2119).
+
+### Forecast AIC Aggregation
+
+1. When a run directory contains a `usage` subdirectory with one or more `.jsonl` files, the AIC-only loader **MUST** compute total AIC from all such files rather than from the single token-usage file.
+2. For each usage record, an implementation **MUST** prefer an explicit credit value (`ai_credits`/`aic`) when present and positive, and **MUST NOT** also recompute AIC from token counts for that same record.
+3. When no explicit credit value is present, an implementation **SHOULD** recompute AIC from the record's token counts using the shared inference-cost function.
+4. When no `usage` directory files are found, an implementation **MUST** fall back to the existing single-file token-usage path.
+5. Records that are malformed, empty, or non-AIC **MUST** be skipped without aborting aggregation of the remaining records.
+
+### Forecast Report Shape
+
+1. The forecast table **MUST** present `Monthly (Low)`, `Monthly (P50)`, and `Monthly (High)` as the Monte Carlo P10, P50, and P90 of 30-day total AIC respectively.
+2. The forecast table **MUST** present `Monthly (Stdev)` as the Monte Carlo standard deviation of the 30-day total-AIC distribution.
+3. Sorting and totals **SHOULD** remain centered on the monthly P50 value.
+
+### Conformance
+
+An implementation is conformant with this ADR if it satisfies all **MUST** and **MUST NOT** requirements above. Failure to meet any **MUST** or **MUST NOT** requirement constitutes non-conformance.
+
+---
+
+*This is a DRAFT ADR generated by the [Design Decision Gate](https://github.com/github/gh-aw/actions/runs/27471799541) workflow. The PR author must review, complete, and finalize this document before the PR can merge.*