feat: formal verification suite (OpenJML ESC/RAC + JPF) in a separate CI pipeline

[bernardladenthin]

Summary

• Adds machine-checked formal verification for StreamBuffer, run in a new, separate pipeline (.github/workflows/formal-verification.yml) kept fully apart from the synchronous Publish pipeline and never a required check (red surfaces on the PR without blocking merges).
• Four layers, from strongest guarantee to broadest coverage:
  • OpenJML ESC (deductive proof, Z3): the 14 static sequential-core methods — both offset/length validators (incl. the (off + len) < 0 integer-overflow idiom, proven equivalent to the clean bounds condition under Java wrap semantics) and the 12 trim-decision/arithmetic helpers (incl. the ceiling division proven against its multiplicative characterization and the full decideTrimExecution decision tree). A proof-count guard fails the job if the verified scope silently shrinks.
  • OpenJML RAC: the existing JUnit suite runs against RAC-instrumented classes (every JML contract checked at runtime, violations throw), forking OpenJML's own JVM so the bundled-spec bigint runtime resolves.
  • jcstress Mode.Termination: four new tests extend deadlock-freedom to every blocking entry point — the second wait phase of read(byte[], off, len) and the public waitForAtLeast API — each paired with a write and a close wakeup.
  • JPF (scheduled/dispatch job): exhaustively model-checks the concurrent read/write/close protocol over all enumerated interleavings; local Docker + JDK 11 recipe in src/test/jpf/README.md.
• Specifications live only in src/main/jml/.../StreamBuffer.jml (the .java stays JML-free / spotless-compatible). Behaviour-preserving production changes were required by the tooling and are documented inline and in CLAUDE.md (12 pure helpers made static; read/write logic lifted into private outer methods; write validator's null check inlined). SpotBugs suppressions added for the false positives that relocation surfaces (safe volatile increments under bufferLock; single-package OPM on public API; a clear constant NPE message).

Test plan

• Affected unit / integration tests pass locally
• CI is green on this branch (default pipeline verified locally; the new formal-verification workflow's first hosted run is the remaining confirmation, esp. the JPF job — green locally in Docker)
• Docs updated (README, CLAUDE.md, TODO); no CHANGELOG entry (unreleased)

Verified locally: default mvn spotless:check verify green (288 tests, SpotBugs 0), PIT 100% (192/192), ESC 14/14, RAC 277/277, jcstress 7/7, JPF "no errors detected" (~14k states, oracle validated with a negative control).

Checklist

• My commits follow Conventional Commits
• No security-sensitive changes

🤖 Generated with Claude Code

https://claude.ai/code/session_01TU5B8DDtDwKSS6ohSfoz2Y

[sonarqubecloud]

Quality Gate failed

Failed conditions
C Security Rating on New Code (required ≥ A)

See analysis details on SonarQube Cloud

Catch issues before they fail your Quality Gate with our IDE extension SonarQube for IDE

[codecov]

Codecov Report

❌ Patch coverage is 96.73913% with 3 lines in your changes missing coverage. Please review.
✅ Project coverage is 96.99%. Comparing base (04fd290) to head (702b945).
⚠️ Report is 5 commits behind head on main.

Files with missing lines	Patch %	Lines
.../java/net/ladenthin/streambuffer/StreamBuffer.java	96.73%	0 Missing and 3 partials ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main     #158      +/-   ##
============================================
+ Coverage     96.88%   96.99%   +0.10%     
- Complexity       94      116      +22     
============================================
  Files             1        1              
  Lines           257      266       +9     
  Branches         33       29       -4     
============================================
+ Hits            249      258       +9     
  Misses            2        2              
  Partials          6        6              

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

[coveralls]

Coverage is 99.248% — claude/formal-verification into main. No base build found for main.