Add package-scoped NullAway measurement and gate proof

.claude-plugin/plugin.json

@@ -1,7 +1,7 @@
 {
   "name": "java-guardrails",
   "displayName": "Java Guardrails",
-  "version": "0.2.0",
+  "version": "0.3.0",
   "description": "Deterministic quality gates (PMD, SpotBugs, Error Prone, ArchUnit, JaCoCo, NullAway, Lincheck, PIT) with calibrated settings and playbooks for installing them one at a time on an existing Java code base, so an agent refactors until the build is green.",
   "author": { "name": "Mark Pollack" },
   "repository": "https://github.com/markpollack/java-guardrails",

.github/workflows/ci.yml

@@ -52,6 +52,8 @@ jobs:
             echo "$out" | grep -qF -- "$l" || { echo "::error::plain measured: missing: $l"; fail=1; }
           done < fixtures/assess/plain/expected-measured.txt
           exit $fail
+      - name: NullAway compiler proof and negative controls
+        run: ./jbang tests/NullAwayTest.java .
       - name: SKILL.md validates against the Agent Skills spec
         run: npx -y skills-ref validate .
       - name: Manifests are valid JSON and point at the root

CHANGELOG.md

@@ -1,5 +1,10 @@
 # Changelog
 
+## 0.3.0 (unreleased)
+
+- NullAway package inventory, report-mode measurement, planted-violation proof and adoption playbook.
+- Optional NullAway routing from assess; explicit package scope, independent of cleanup of other Error Prone checks.
+
 ## 0.2.0 — 2026-10-27
 
 See `.github/release-notes/0.2.0.md`.

README.md

@@ -23,12 +23,18 @@ base's own facts, which `assess` reads (below), not from the table.
 | Is executed code wrong in a known shape? | Error Prone defaults at ERROR | a compile under JDK 21; every change | **Proven end to end on two code bases**: measured, decided, installed, green, falsified. Three real bugs on the second. |
 | What must be refactored before the others can see it? | PMD size, complexity and duplication | minutes, then the refactoring; a target, then a gate | **Proven end to end on two code bases**: measured, decided, installed, green, falsified; measured on a third, where the references did not fit (`evidence/agent-journal.md`). |
 | Is the structure drifting? | ArchUnit no-cycles | seconds after compile; every change | **Proven on two code bases**; on the second, gating the cycle-free modules while the core's 13 measured cycles wait for their own session. Layers not yet. |
-| | NullAway, Lincheck | | Outlines. |
+| Can null cross a non-null contract? | NullAway, explicit package scope | a compile under JDK 21; every change | Measurement and falsification implemented; see `evidence/nullaway.md` for the scope proven. Optional, outside the default gate order. |
+| | Lincheck | | Outline. |
 | Does the executing test check anything? (advanced) | PIT, scoped | tens of minutes whole-module, about two scoped; changed classes during work, whole module at acceptance | Playbook written from one code base's record; a profile, never a gate, never in the order. |
 
 Maven only. A Gradle slice is planned; `measure` already works on Gradle projects, the gate
 install does not.
 
+For nullness checking, ask to adopt NullAway on a selected package (`playbooks/30-nullaway.md`).
+It runs through Error Prone's compiler integration; you can select NullAway before cleaning up
+other Error Prone checks. `measure-nullaway --inventory` lists package defaults without a build.
+The report and planted-violation proof require the profile, JSpecify, and JDK 21+.
+
 ## Getting started
 
 You need a JDK 17 or newer (21 or newer for the Error Prone gate), a Maven project with the
@@ -182,6 +188,9 @@ taking the change is your decision.
 ./jbang falsify <target> spotbugs
 ./jbang falsify <target> jacoco
 ./jbang falsify <target> archunit
+./jbang measure-nullaway <target> --inventory       # package defaults, no build
+./jbang measure-nullaway <target> --module module-path
+./jbang falsify <target> nullaway --module module-path --package com.example
 ```
 
 The aliases resolve from `jbang-catalog.json` in the current directory, so from anywhere else
@@ -245,7 +254,7 @@ Next, in order:
 - **Gradle**: the measures already work on Gradle projects; the gate install does not.
 - **ArchUnit, the rest**: breaking cycles that run through public types, and a layering rule
   the owner confirms.
-- **Tier 3**: NullAway and Lincheck from the first code base's record; PIT's scoped playbook
+- **Tier 3**: Lincheck from the first code base's record; PIT's scoped playbook
   is written, a script to run it is not.
 - **Windows** proof of the scripts, and a self-test fixture so CI runs the measures and the
   plants against known counts.

SKILL.md

@@ -5,7 +5,7 @@ license: Business Source License 1.1; see LICENSE
 compatibility: Requires a JDK 17 or newer and a Maven project with the Maven wrapper. The bundled JBang wrapper resolves everything else on first run. Gradle is not yet supported.
 metadata:
   author: markpollack
-  version: "0.2.0"
+  version: "0.3.0"
 ---
 
 # java-guardrails
@@ -48,13 +48,19 @@ owner edits the line. The tier says how proven a gate is, not when to install it
 | Error Prone defaults at ERROR | Is executed code wrong in a known shape? | a compile under JDK 21; every change | `playbooks/11-errorprone.md` | proven on two code bases |
 | PMD size, complexity and duplication | What must be refactored before the others can see it? | minutes, then the refactoring; a target, then a gate | `playbooks/10-pmd.md` | proven on two code bases; measured on a third |
 | ArchUnit no-cycles, then layers | Is the structure drifting? | seconds; every change | `playbooks/20-archunit.md` | no-cycles proven on two code bases; layers not yet |
-| NullAway, Lincheck | tier 3 | | `playbooks/30-*.md`, `31-*.md` | outline |
+| NullAway (optional, explicit package scope) | Can null cross a non-null contract? | a compile under JDK 21; every change | `playbooks/30-nullaway.md` | measurement and falsification implemented; see `evidence/nullaway.md` for proven scope |
+| Lincheck | tier 3 | | `playbooks/31-lincheck.md` | outline |
 | PIT, scoped (advanced) | Does the executing test check anything? | tens of minutes whole-module, about two scoped; changed classes during work, whole module at acceptance | `playbooks/32-pit.md` | written from one code base's record; a profile, not a gate, never in the order |
 
 Follow a playbook step by step. Every step is marked **script**, **AI**, **notify** or **stop**.
 Do not write a gate's playbook from memory; an outline means the gate is not yet proven and you
 say so.
 
+For NullAway, follow playbook 30: inventory package defaults, choose adoption scope, measure,
+fix, and falsify each claimed package. It needs Error Prone's compiler integration; other Error
+Prone findings need not be cleaned up first. NullAway is outside the default `GATE_ORDER` in this
+increment. A configured processor with no marked scope, or a zero report count, is not proof.
+
 ## Stops: notify or decide
 
 Some steps need the owner: which modules are test code, how to go green, which exemptions to
@@ -105,7 +111,9 @@ is kept and ignored; `PROJECT_*` is never claimed by the kit, so the target's ow
 <kit>/jbang <kit>/scripts/SpotBugsMeasure.java   <target> [--top N]     # needs the plugin slice installed
 <kit>/jbang <kit>/scripts/JacocoMeasure.java     <target>               # needs nothing installed; runs the tests
 <kit>/jbang <kit>/scripts/ArchUnitMeasure.java   <target> [--top N]     # needs nothing installed; compiles
-<kit>/jbang <kit>/scripts/Falsify.java      <target> pmd | cpd | errorprone | spotbugs | jacoco | archunit
+<kit>/jbang <kit>/scripts/NullAwayMeasure.java   <target> [--module path] [--inventory] # inventories without a build; otherwise needs the profile and JDK 21
+<kit>/jbang <kit>/scripts/Falsify.java      <target> pmd | cpd | errorprone | spotbugs | jacoco | archunit | nullaway
+<kit>/jbang <kit>/scripts/Falsify.java      <target> nullaway [--module path] [--package com.example] # existing JSpecify-marked package
 ```
 
 `assess` reads files and the git log, runs PMD and CPD in-process under a time limit

configs/nullaway/package-info.java.tmpl

@@ -0,0 +1,3 @@
+// Replace com.example with the selected package. This default does not include subpackages.
+@org.jspecify.annotations.NullMarked
+package com.example;

evidence/nullaway.md

@@ -0,0 +1,49 @@
+# NullAway: package adoption and gate proof
+
+## Local compiler fixture, 2026-10-27
+
+`./jbang tests/NullAwayTest.java .` builds a temporary Maven project from the kit's actual
+Error Prone profile, properties and JVM arguments, using JDK 21, Maven 3.9.9, Error Prone
+2.50.0, NullAway 0.13.8 and JSpecify 1.0.0.
+
+The fixture has one marked package and one unmarked child package. A null returned from a
+non-null method produces one unique NullAway report finding and fails the ordinary compile.
+Fixing it produces zero findings; falsification then proves the gate with a new nullable return
+inside the existing marked package. Disabling NullAway cannot pass that proof. Comment-only
+markers, an unrelated compiler failure, and a colliding target-owned probe cannot pass either.
+Sources remain unchanged after the probe, including negative runs. The fixture also compiles a
+dropped exception with other Error Prone checks disabled, while the NullAway plant still fails:
+other Error Prone cleanup is not a prerequisite for nullness adoption.
+
+The source inventory counts **exact package defaults**, not all checked declarations. It does
+not recursively treat child packages as marked, or claim class/method annotation coverage.
+`assess` reports processor presence and scope requiring proof; it retains the default gate order.
+
+## MCP Java SDK: one existing package, 2026-10-27
+
+An isolated export of the previous trial target at `61a1db89a477f80783c8563bf68c2bba0c8e131b`
+was used. No target checkout was modified or pushed. The scope was the two-file
+`mcp-core=io.modelcontextprotocol.json.schema` package, with a new JSpecify package default and
+the JSpecify dependency in `mcp-core`. The other nine core packages stayed unmarked.
+
+| Measurement | Result |
+|---|---|
+| Report-mode compile after marking | 3 unique NullAway diagnostics |
+| Findings | Two factories construct a validation response with a null component; the default schema validator passes null to the successful-response factory |
+| Fix | Mark the documented nullable response components and successful-response parameter `@Nullable`; also preserve the documented nullable schema parameter of `assertConforms` |
+| Report-mode compile after annotation changes | 0 NullAway findings |
+| `falsify nullaway --module mcp-core --package io.modelcontextprotocol.json.schema` | Build red, `[NullAway]` names the planted nullable return; probe removed |
+| Normal restored `clean verify`, selected module and its dependencies | Green; 452 tests, zero failures/errors/skips; existing PMD/CPD, SpotBugs and coverage checks pass |
+
+Commands, invoked from the kit with the scratch target substituted for `<target>`:
+
+```
+./jbang scripts/NullAwayMeasure.java <target> --module mcp-core
+./jbang scripts/Falsify.java <target> nullaway --module mcp-core --package io.modelcontextprotocol.json.schema
+<target>/mvnw -B -P errorprone -Dspring-javaformat.skip=true -pl mcp-core -am clean verify
+```
+
+Prediction: no existing assess rule predicted these findings. Package marking exposed incomplete
+nullability contracts already documented in the API; this experiment establishes annotation and
+enforcement mechanics, not three new runtime bugs. It proves only the selected package, not
+whole-SDK null safety or nullness across unmarked module boundaries.

fixtures/nullaway/.mvn/wrapper/maven-wrapper.properties

@@ -0,0 +1,19 @@
+# Licensed to the Apache Software Foundation (ASF) under one
+# or more contributor license agreements.  See the NOTICE file
+# distributed with this work for additional information
+# regarding copyright ownership.  The ASF licenses this file
+# to you under the Apache License, Version 2.0 (the
+# "License"); you may not use this file except in compliance
+# with the License.  You may obtain a copy of the License at
+#
+#   http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing,
+# software distributed under the License is distributed on an
+# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
+# KIND, either express or implied.  See the License for the
+# specific language governing permissions and limitations
+# under the License.
+wrapperVersion=3.3.2
+distributionType=only-script
+distributionUrl=https://repo.maven.apache.org/maven2/org/apache/maven/apache-maven/3.9.9/apache-maven-3.9.9-bin.zip

fixtures/nullaway/README.md

@@ -0,0 +1,17 @@
+# NullAway compiler proof
+
+Run from the kit root on JDK 21+:
+
+```
+./jbang tests/NullAwayTest.java .
+```
+
+The Java runner creates an isolated temporary Maven target using the shipped Error Prone profile,
+properties and JVM arguments. These wrapper files are Apache Maven Wrapper 3.3.2 (Apache-2.0),
+using Maven 3.9.9. The runner keeps its scratch directory for inspection and prints the path.
+
+It proves a real NullAway diagnostic appears in report mode, the normal compile fails, fixing the
+source clears it, and falsification catches a planted nullable return. Negative controls disable
+the checker, remove the package annotation, collide with an existing target file and break the
+build. None can pass proof or overwrite target sources. An unmarked child package stays outside
+its parent's package default. The new probe is removed after both positive and negative runs.