ci(codeql): treat Java like every other managed runtime — add java-kotlin matrix + scan AlloyRunner.java

.github/codeql/codeql-config.yml

@@ -26,12 +26,19 @@ paths-ignore:
   # focused on production surfaces.
   - "bench/**"
 
-  # Formal-method tool trees. TLA+ specs, Alloy models, Lean
-  # proofs — CodeQL has no language pack that understands any
-  # of these, and incidental C# helper code in these dirs
-  # (e.g. TLC driver shims) is tool-internal, not shipped.
+  # Formal-method tool trees. TLA+ specs and Lean proofs —
+  # CodeQL has no language pack that understands either.
+  # Incidental C# helper code in these dirs (e.g. TLC driver
+  # shims) is tool-internal, not shipped.
+  #
+  # `tools/alloy/**` was previously listed here. Removed
+  # 2026-04-28: `tools/alloy/AlloyRunner.java` is first-party
+  # Java that drives Alloy from .NET, and Java is a managed
+  # runtime pinned via `.mise.toml` (java = "26"). Treating
+  # that file as scannable code is consistent with how csharp
+  # / fsharp / actions are treated elsewhere; CodeQL's
+  # `java-kotlin` extractor handles it.
   - "tools/tla/**"
-  - "tools/alloy/**"
   - "tools/lean4/**"
 
   # Generated code. If any file ends in `.generated.cs` it is

.github/workflows/codeql.yml

@@ -9,8 +9,24 @@
 #
 # WHAT THIS DOES DIFFERENTLY FROM THE GITHUB DEFAULT
 # ----------------------------------------------------
-#   1. Dropped the `java-kotlin` matrix cell. Zeta is F#/C#
-#      on .NET 10; there is no Java / Kotlin source.
+#   1. `java-kotlin` matrix cell kept (was previously dropped
+#      based on the wrong assumption "no Java/Kotlin source").
+#      Zeta is primarily F#/C# on .NET 10 but
+#      `tools/alloy/AlloyRunner.java` is first-party Java — a
+#      headless JVM driver that runs `.als` Alloy specs from the
+#      formal-verification surface. Java is a managed dependency
+#      pinned via `.mise.toml` (Java 26, round-34 migration off
+#      brew/apt onto mise) and installed by `tools/setup/install.sh`
+#      on dev laptops, devcontainers, and CI runners. Treating
+#      it as scannable code is consistent with how every other
+#      managed runtime in the repo is treated; pretending
+#      otherwise gates LFG PRs (empirical 2026-04-28 LFG #661 —
+#      umbrella `CodeQL` check NEUTRAL with verbatim summary
+#      "1 configuration present on `refs/heads/main` was not
+#      found: codeql.yml /language:java-kotlin", which the
+#      `code_quality:severity=all` ruleset rule reads as
+#      "results pending"). Detection + mechanism captured in
+#      `memory/feedback_codeql_umbrella_neutral_vs_per_language_detection_pattern_aaron_2026_04_28.md`.
 #   2. `csharp` leg uses `build-mode: manual` with
 #      `./tools/setup/install.sh` + `dotnet build Zeta.sln`.
 #      The GitHub default was `build-mode: none` (source-only),
@@ -207,6 +223,10 @@ jobs:
               # SC2222 (later pattern shadowed by earlier one).
               src/*|tests/*|tools/*) code_changed=true ;;
               *.cs|*.fs|*.fsproj|*.csproj|*.sln) code_changed=true ;;
+              # Java surface: tools/alloy/AlloyRunner.java is the
+              # only first-party Java today; java is a mise-pinned
+              # runtime per .mise.toml.
+              *.java) code_changed=true ;;
               *.py|pyproject.toml|requirements*.txt) code_changed=true ;;
               *.js|*.jsx|*.ts|*.tsx|*.mjs|*.cjs) code_changed=true ;;
               package.json|package-lock.json|tsconfig*.json) code_changed=true ;;
@@ -377,6 +397,22 @@ jobs:
             build-mode: none
           - language: csharp
             build-mode: manual
+          # java-kotlin scans `tools/alloy/AlloyRunner.java` —
+          # a single-file JVM driver with no Maven/Gradle build,
+          # so `build-mode: none` (CodeQL's source-only pack)
+          # produces a real DB. Java 26 is on PATH via mise per
+          # tools/setup/install.sh; the GitHub-hosted runner has
+          # mise-shimmed Java available after the install step
+          # below, but we don't need to invoke `javac` ourselves.
+          #
+          # JVM language preference (B-0075): Kotlin > Scala >
+          # Java. New JVM code lands in Kotlin by default;
+          # AlloyRunner.java is grandfathered until its next
+          # non-trivial rewrite. The `java-kotlin` extractor
+          # scans all three so this matrix cell does not need
+          # to change when the preference activates.
+          - language: java-kotlin
+            build-mode: none
           - language: python
             build-mode: none
           - language: javascript-typescript

docs/backlog/P2/B-0076-disowned-runtime-sweep-python-typescript-2026-04-28.md

@@ -0,0 +1,118 @@
+---
+id: B-0076
+priority: P2
+status: open
+title: Disowned-runtime sweep — Python + TypeScript surface (same pattern PR #662 fixed for Java)
+effort: S
+ask: extend the codeql.yml analyze matrix to cover python + javascript-typescript like PR #662 did for java-kotlin
+created: 2026-04-28
+last_updated: 2026-04-28
+tags: [codeql, disowned-runtime, python, typescript, dependency-honesty, b-0075-sibling]
+---
+
+# B-0076 — Disowned-runtime sweep: Python + TypeScript
+
+## Source
+
+Discovered 2026-04-28 immediately after PR #662 landed the Java
+side of this same pattern. EVIDENCE-BASED audit:
+
+```bash
+find . -type f \( -name "*.py" -o -name "*.ts" \) \
+  -not -path "*/node_modules/*" -not -path "*/.git/*" \
+  -not -path "*/.claude/worktrees/*" \
+  -not -path "*/references/upstreams/*" \
+  -not -path "*/bench/*" 2>/dev/null
+```
+
+Returns first-party files:
+
+- **Python (2):**
+  - `tools/hygiene/sort-tick-history-canonical.py`
+  - `tools/hygiene/fix-markdown-md032-md026.py`
+- **TypeScript (2):**
+  - `eslint.config.ts`
+  - `tools/invariant-substrates/tally.ts`
+
+(Lean's `tools/lean4/.lake/packages/...` JS files are vendored
+and already excluded via `tools/lean4/**` in
+`.github/codeql/codeql-config.yml` paths-ignore.)
+
+## The disowned-runtime pattern (per CURRENT-aaron.md §28)
+
+When a runtime is in `.mise.toml`, every surface that touches it
+(CodeQL matrix, install path, workflow comments) must treat it
+consistently. The failure shape is "X is managed for install but
+workflow Y pretends X doesn't exist."
+
+EVIDENCE that this pattern applies to Python + TypeScript:
+
+- `.mise.toml:25` → `python = "3.14"` (managed)
+- `.mise.toml:28` → `bun = "1.3"` (TypeScript runtime, managed)
+- `.github/workflows/codeql.yml` analyze matrix (after PR #662):
+  `actions / csharp / java-kotlin` — **no python, no
+  javascript-typescript**
+- Path-gate uploads empty SARIF for python +
+  javascript-typescript (mitigates the umbrella-NEUTRAL surface
+  symptom) but does NOT scan the actual `.py` / `.ts` files
+
+The current state silently scans nothing for Python and TS code
+even though the runtimes are managed and the files exist. Same
+shape as Java pre-#662.
+
+## Why P2 (not P1, not P3)
+
+- Not P0/P1: no current incident; Python/TS code paths are small
+  (4 files total) and tooling-only (hygiene scripts + lint
+  config + small invariant tool). No production-path security
+  exposure today.
+- Not P3: the pattern matches an active discipline (CURRENT-aaron
+  §28) and Aaron's recent framing is moving toward "managed
+  means scanned." Sleeping on it accumulates the same disownment
+  PR #662 just resolved.
+
+## Scope
+
+`.github/workflows/codeql.yml` analyze matrix gains two cells:
+
+```yaml
+- language: python
+  build-mode: none
+- language: javascript-typescript
+  build-mode: none
+```
+
+`.github/codeql/codeql-config.yml` may need adjustment depending
+on whether any current paths-ignore entry covers a python or ts
+file path that should now be scanned. Audit `bench/**`,
+`tools/lean4/**`, `references/upstreams/**` for masking effects
+on the 4 first-party files.
+
+`tools/invariant-substrates/tally.ts` should be confirmed
+in-scope (it's a Zeta tool — first-party). `eslint.config.ts`
+is repo-wide config; CodeQL scans configs as expected.
+
+## Acceptance
+
+- [ ] `Analyze (python)` and `Analyze (javascript-typescript)`
+      legs added to the matrix and pass on a smoke PR
+- [ ] Findings (if any) on the 4 first-party files surface as
+      code-scanning alerts in Security tab
+- [ ] codeql.yml header doc updated to enumerate all 5
+      first-party-runtime languages (actions / csharp /
+      java-kotlin / python / javascript-typescript) consistently
+- [ ] `feedback_codeql_umbrella_neutral_vs_per_language_detection_pattern_aaron_2026_04_28.md`
+      updated with "all five legs honest" note when this lands
+
+## Composes with
+
+- PR #662 (the Java leg of this same pattern; this row extends
+  the same fix to Python + TS)
+- B-0075 (JVM language preference; this row is the
+  non-JVM-runtime sibling)
+- CURRENT-aaron.md §28 (dependency-honesty rule — the
+  discipline this row applies)
+- `.mise.toml` (the source of truth for what "managed" means)
+- `feedback_codeql_umbrella_neutral_vs_per_language_detection_pattern_aaron_2026_04_28.md`
+  (the deeper structural cause section; this row is one of the
+  fallout cleanups it predicts)

docs/backlog/P3/B-0075-jvm-language-preference-kotlin-scala-java-2026-04-28.md

@@ -0,0 +1,109 @@
+---
+id: B-0075
+priority: P3
+status: open
+title: JVM language preference — Kotlin > Scala > Java; sweep fallout when JVM code is added or rewritten
+effort: S-per-fallout
+ask: future-direction substrate; trigger sweep when JVM code touches the repo
+created: 2026-04-28
+last_updated: 2026-04-28
+tags: [jvm, kotlin, scala, java, language-preference, alloy-runner, future-direction]
+---
+
+# B-0075 — JVM language preference: Kotlin > Scala > Java
+
+## Source
+
+Aaron 2026-04-28T14:48Z, after PR #662 landed `tools/alloy/AlloyRunner.java`
+honestly back into the CodeQL surface:
+
+> *"also i'm a big fan of kotlin we should prefere jvm languages in this
+> order kotlin, scala, java  backlog this any any updates that fall out"*
+
+## The preference
+
+When Zeta adds new JVM-targeted code (or non-trivially rewrites existing
+JVM code), prefer the language in this order:
+
+1. **Kotlin** — first choice. Aaron's stated favorite. Modern,
+   null-safe, concise, interoperates with Java, ships fast.
+2. **Scala** — second choice. Functional-first, mature, FP-friendly
+   (composes with the F# / DBSP factory aesthetic).
+3. **Java** — third choice. Use only when Kotlin / Scala friction
+   outweighs the language-preference cost (e.g. trivial single-file
+   tooling where Kotlin's gradle / kotlinc dependency would be heavier
+   than `javac AlloyRunner.java`).
+
+The CodeQL `java-kotlin` extractor scans all three; the security-scanning
+surface doesn't change with the language choice.
+
+## Trigger
+
+Apply this preference when:
+
+- A new JVM-targeted file lands (any `.kt`, `.scala`, `.java`)
+- Existing JVM code is non-trivially rewritten (>20 lines, refactor, or
+  feature extension — not bug fixes)
+- A new JVM-based tool is integrated (Spark, Flink, Kafka client,
+  custom Alloy / TLA harness, etc.)
+- A round of formal-verifier work expands the JVM tool surface
+
+## Known fallout
+
+- **`tools/alloy/AlloyRunner.java`** (existing first-party JVM file) is
+  the natural candidate for a Kotlin migration the next time it gets
+  non-trivial work. Current state: 1 file, single-purpose Alloy driver,
+  CodeQL-scanned via PR #662. Migration not urgent; trigger when the
+  file is touched for non-bug-fix reasons.
+
+  - Kotlin migration adds: gradle / kotlinc / kotlin-stdlib runtime
+    dependency
+  - Kotlin migration buys: null-safety, less ceremony, modern syntax
+  - Decision criterion: when the file gets a substantive feature
+    (e.g. JSON output, multi-spec composition, parallel-runs), the
+    rewrite cost amortizes; until then, keep as Java
+  - Composes with `.mise.toml` already pinning Java 26 — Kotlin would
+    need a parallel `kotlin = "<version>"` mise pin
+
+- **`tools/setup/manifests/{apt,brew}` comments** mention "OpenJDK
+  moved off brew/apt onto mise" — accurate today; if Kotlin migration
+  lands, comments should mention "JDK + Kotlin via mise" for clarity.
+
+- **`docs/research/build-machine-setup.md`** documents the mise pin
+  rationale; would gain a "JVM languages we prefer" note when this
+  preference graduates from backlog.
+
+## Why P3 (deferred / convenience)
+
+No JVM code is currently being added. The preference is future-direction
+substrate that pays off as the JVM surface grows. Promoting to P2/P1
+when:
+
+- Aaron names a specific JVM project he wants to start
+- A round of formal-verifier work expands the harness
+- The Alloy runner needs a feature the current Java surface doesn't
+  support cleanly
+
+## Acceptance
+
+- [ ] Preference indexed in `MEMORY.md` so future-Otto sees it at
+      session bootstrap (covered by this row's existence + the row's
+      indexing in the BACKLOG.md / per-row index)
+- [ ] When the next JVM file lands, the PR description cites this
+      row's preference order and explains the language choice (Kotlin
+      by default, Scala / Java with rationale)
+- [ ] If `tools/alloy/AlloyRunner.java` gets a non-trivial rewrite,
+      the rewrite ships in Kotlin with a `tools/alloy/AlloyRunner.kt`
+      replacement + a brief migration note in the commit message
+
+## Composes with
+
+- PR #662 (the codeql java-honesty fix that surfaced this preference
+  as fallout-worthy substrate)
+- `.mise.toml` (where any Kotlin / Scala pin would live)
+- `feedback_speculation_leads_investigation_not_defines_root_cause_aaron_2026_04_28.md`
+  (the EVIDENCE-BASED labeling discipline this row exemplifies — the
+  preference IS labeled, the trigger conditions ARE listed, the
+  fallout IS enumerated)
+- `docs/research/build-machine-setup.md` (the eventual sweep target
+  when the preference activates)