Stage-2 quality judge + improve loop with convergence (speca#88 eval)

.github/workflows/ci.yml

@@ -86,6 +86,46 @@ jobs:
             --health-json tests/fixtures/theorem_health.sample.json \
             --out 01e_fixture.json
           speca-lean4 verify-recall --ours 01e_fixture.json --strict
+      - name: honesty check — vendored solodit reference provenance (speca#88 stage-2)
+        run: |
+          python3 -c "
+          import hashlib, json, csv
+          meta = json.load(open('data/solodit_checklist.meta.json', encoding='utf-8'))
+          raw = open('data/solodit_checklist.csv', 'rb').read()
+          sha = hashlib.sha1(b'blob %d\x00' % len(raw) + raw).hexdigest()
+          assert sha == meta['source_blob_sha'], f'vendored bytes drifted: {sha}'
+          assert b'\r' not in raw, 'CRLF crept into the vendored reference'
+          rows = list(csv.DictReader(open('data/solodit_checklist.csv', encoding='utf-8-sig')))
+          assert len(rows) == meta['n_rows'], (len(rows), meta['n_rows'])
+          assert list(rows[0].keys()) == meta['columns'], rows[0].keys()
+          print(f'OK: {len(rows)} reference items, blob {sha} matches {meta[\"source_repo\"]}@{meta[\"source_commit\"][:12]}')
+          "
+      - name: judge + improve harness wiring with the MOCK LLM (no API key in default CI)
+        # The real LLM run is dispatch-only (judge-dispatch.yml, self-hosted
+        # authenticated Claude CLI). Here the injected-LLM seam is exercised
+        # end to end with the deterministic mock so this stays green keyless.
+        run: |
+          speca-lean4 judge \
+            --ours 01e_fixture.json --id-prefix CHK- \
+            --llm-cmd "python3 tests/fixtures/mock_llm.py" \
+            --out judge_report_mock.json
+          speca-lean4 improve \
+            --ours 01e_fixture.json --id-prefix CHK- \
+            --llm-cmd "python3 tests/fixtures/mock_llm.py" \
+            --ref-report judge_report_mock.json \
+            --out-dir improve_run_mock --max-rounds 4
+          python3 -c "
+          import json
+          rep = json.load(open('judge_report_mock.json', encoding='utf-8'))
+          assert rep['ours']['n'] == 15 and rep['reference']['n'] == 52
+          log = json.load(open('improve_run_mock/score_log.json', encoding='utf-8'))
+          assert log['rounds'] and len(log['history_overall_mean']) == len(log['rounds'])
+          assert isinstance(log['converged'], bool) and log['stop_reason']
+          props = json.load(open('improve_run_mock/improved_01e.json', encoding='utf-8'))['properties']
+          assert len(props) == 15
+          print('OK: judge report + improve score log written with the mock adapter;',
+                f\"converged={log['converged']} ({log['stop_reason']})\")
+          "
 
   lean:
     name: lean exporter build

.github/workflows/judge-dispatch.yml

@@ -0,0 +1,107 @@
+name: "judge + improve with the real LLM (speca#88 stage-2, dispatch-only)"
+
+# The default CI exercises the judge/improve harness with a deterministic
+# mock (no API key anywhere in this repo). This workflow is the ONE place the
+# real LLM runs: dispatch-only, on a self-hosted runner where the Claude CLI
+# is already authenticated (same pattern as speca's 03/04 workflows). It
+# emits the CHK checklist from the fixture health, judges it against the
+# vendored solodit reference bar, runs the improve loop, and uploads the
+# judge report + per-round score log as artifacts.
+#
+# No pull_request trigger on purpose: it occupies a shared runner and spends
+# LLM budget. Honesty: the verification step only checks the artifacts are
+# well-formed — it never asserts the bar was met or the loop converged;
+# below-bar / unconverged are valid, reportable outcomes.
+
+on:
+  workflow_dispatch:
+    inputs:
+      model:
+        description: "claude -p --model value (empty = CLI default)"
+        required: false
+        type: string
+        default: ""
+      max_rounds:
+        description: "improve loop hard cap"
+        required: false
+        type: number
+        default: 6
+      skip_improve:
+        description: "only judge (no improve loop) to bound LLM cost"
+        required: false
+        type: boolean
+        default: false
+
+permissions:
+  contents: read
+
+jobs:
+  judge-improve:
+    if: ${{ github.actor == 'grandchildrice' || github.actor == 'hirorogo' || github.actor == 'sururu-k' }}
+    runs-on: self-hosted
+    timeout-minutes: 120
+
+    env:
+      MODEL_INPUT: ${{ inputs.model }}
+      MAX_ROUNDS: ${{ inputs.max_rounds }}
+      SKIP_IMPROVE: ${{ inputs.skip_improve }}
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: install the plugin
+        run: pip install -e '.[dev]'
+
+      - name: emit the CHK checklist 01e (fixture health; generation is CHK-15, not re-implemented)
+        run: |
+          speca-lean4 emit-01e \
+            --scope tests/fixtures/bug_bounty_scope.sample.json \
+            --health-json tests/fixtures/theorem_health.sample.json \
+            --out 01e_fixture.json
+
+      - name: judge against the solodit reference bar (real LLM)
+        run: |
+          set -euo pipefail
+          LLM_CMD="claude -p"
+          if [ -n "$MODEL_INPUT" ]; then LLM_CMD="claude -p --model $MODEL_INPUT"; fi
+          speca-lean4 judge \
+            --ours 01e_fixture.json --id-prefix CHK- \
+            --llm-cmd "$LLM_CMD" \
+            --out judge_report.json
+
+      - name: improve loop (real LLM, reference scores reused from the judge report)
+        if: ${{ inputs.skip_improve != true }}
+        run: |
+          set -euo pipefail
+          LLM_CMD="claude -p"
+          if [ -n "$MODEL_INPUT" ]; then LLM_CMD="claude -p --model $MODEL_INPUT"; fi
+          speca-lean4 improve \
+            --ours 01e_fixture.json --id-prefix CHK- \
+            --llm-cmd "$LLM_CMD" \
+            --ref-report judge_report.json \
+            --out-dir improve_run --max-rounds "$MAX_ROUNDS"
+
+      - name: verify artifacts are well-formed (NOT that the bar was met)
+        run: |
+          python3 -c "
+          import json, os
+          rep = json.load(open('judge_report.json', encoding='utf-8'))
+          assert rep['ours']['n'] > 0 and rep['reference']['n'] == 52
+          print('judge:', 'ours', rep['ours'], 'reference', rep['reference'],
+                'meets_reference_bar =', rep['meets_reference_bar'])
+          if os.path.isdir('improve_run'):
+              log = json.load(open('improve_run/score_log.json', encoding='utf-8'))
+              assert log['rounds'] and log['stop_reason']
+              print('improve:', 'converged =', log['converged'],
+                    f\"({log['stop_reason']})\", 'progression =', log['history_overall_mean'])
+          "
+
+      - name: upload judge report + score log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: judge-improve-real-llm
+          path: |
+            judge_report.json
+            improve_run/
+          retention-days: 30

README.md

@@ -312,6 +312,39 @@ severity profile than the CRITICAL/HIGH-heavy benchmark, which we report rather
 than fake. Most consensus-layer findings (OOM/DoS, LMD-GHOST, BLS internals,
 eth1 ops) remain out of the FFG formal remit by construction.
 
+## Quality judge + improve loop (speca#88 stage-2)
+
+eval here is NOT recall (the #88 direction's 重要な訂正): the checklist is not
+scored on reproducing dataset bugs, but on reaching the QUALITY LEVEL of a
+professional audit checklist. `speca-lean4 judge` scores every item on five
+fixed axes (specificity, implementation_readiness, generality, actionability,
+granularity; blind rubric in `src/speca_lean4/judge.py`) and compares the
+score DISTRIBUTION against the same-rubric scores of the vendored solodit
+reference ([`data/solodit_checklist.csv`](data/solodit_checklist.csv), 52
+professional audit items, provenance pinned in
+[`data/solodit_checklist.meta.json`](data/solodit_checklist.meta.json)).
+`speca-lean4 improve` then loops judge -> sharpen low scorers (with the
+matching `data/ethereum_vulns.csv` rows as teaching material — improve input,
+never an eval denominator) -> re-judge, converging only when the reference
+bar is met AND the last 3 rounds plateau; an unconverged run ends honestly
+with `converged: false`. `recall.py`'s 0.556 stays a side reference number,
+outside the judge verdict. Full spec: [`docs/judge-loop.md`](docs/judge-loop.md).
+
+```bash
+# LLM access is injected — no API key in this repo. --llm-cmd reads the
+# prompt on stdin and writes the response on stdout, e.g. an authenticated
+# Claude CLI (the real run lives in .github/workflows/judge-dispatch.yml,
+# self-hosted, dispatch-only; default CI wires tests/fixtures/mock_llm.py):
+speca-lean4 judge --ours outputs/01e_PARTIAL_checklist-high-angle.json \
+    --llm-cmd "claude -p" --out judge_report.json
+
+speca-lean4 improve --ours outputs/01e_PARTIAL_checklist-high-angle.json \
+    --llm-cmd "claude -p" --ref-report judge_report.json \
+    --out-dir improve_run --max-rounds 6
+# -> improve_run/score_log.json (per-round progression, convergence verdict)
+#    improve_run/improved_01e.json (proposal; theorem_map.json stays canonical)
+```
+
 ## Lean exporter directly
 
 ```bash

data/solodit_checklist.csv

@@ -0,0 +1,53 @@
+id,category,subcategory,question,description
+SOL-AM-DOSA-1,DoS,withdrawal,"Is withdrawal pattern followed?","Prevent DOS during withdrawals by following pull-based approach"
+SOL-AM-DOSA-2,DoS,minimum_amount,"Is there a minimum transaction amount?","Enforce minimum amounts to prevent dust/zero transaction spam"
+SOL-AM-DOSA-3,DoS,blacklist,"How does protocol handle blacklisting tokens?","Account for USDC-like blacklisting to ensure functionality"
+SOL-AM-DOSA-4,DoS,queue,"Can forcing queue processing lead to DOS?","Design queue processing resistant to spam exploitation"
+SOL-AM-DOSA-5,DoS,low_decimals,"What happens with low decimal tokens?","Handle low decimal tokens to prevent rounding-to-zero DOS"
+SOL-AM-DOSA-6,DoS,external_call,"Does protocol handle external interactions safely?","Robust handling of external failures to maintain integrity"
+SOL-AM-DA-1,Donation,balance_reliance,"Does protocol rely on balanceOf instead of internal accounting?","Attackers can manipulate accounting by donating tokens"
+SOL-AM-FrA-1,Frontrunning,create_pattern,"Are get-or-create patterns protected?","Separate creation and interaction to prevent frontrunning"
+SOL-AM-FrA-2,Frontrunning,two_tx,"Are two-transaction actions safe from frontrunning?","Critical multi-tx actions must not be interferable"
+SOL-AM-FrA-3,Frontrunning,dust_grief,"Can users cause others' tx to revert with dust?","Prevent dust amounts from affecting contract state"
+SOL-AM-FrA-4,Frontrunning,commit_reveal,"Is commit-reveal scheme user-bound?","Two-phase commit-reveal must bind to specific users"
+SOL-AM-GA-1,Griefing,state_dependency,"Is there an external function relying on changeable states?","Ensure withdrawals not disturbed by other actors"
+SOL-AM-GA-2,Griefing,gas_limit,"Can operations be manipulated with precise gas?","Implement gas checks before critical operations"
+SOL-AM-MA-1,Manipulation,timestamp,"Is block.timestamp used for time-sensitive ops?","Miners can manipulate timestamps; use block.number for critical timing"
+SOL-AM-MA-2,Manipulation,randomness,"Is block properties used for randomness?","Use Chainlink VRF instead of predictable block properties"
+SOL-AM-MA-3,Manipulation,tx_ordering,"Is logic sensitive to transaction ordering?","Implement slippage protection that reverts on bad execution"
+SOL-AM-PMA-1,PriceManipulation,balance_ratio,"Is price calculated by token balance ratio?","Use oracles instead of balance ratios vulnerable to flash loans"
+SOL-AM-PMA-2,PriceManipulation,spot_price,"Is price from DEX spot prices?","Use TWAP or reliable oracles instead of spot prices"
+SOL-AM-ReentrancyAttack-1,Reentrancy,read_only,"Is there a view function returning stale value during interaction?","Extend reentrancy guards to view functions"
+SOL-AM-ReentrancyAttack-2,Reentrancy,state_after_call,"Is there state change after external call?","Use CEI pattern or reentrancy guards"
+SOL-AM-ReplayAttack-1,Replay,failed_tx,"Are failed transactions protected against replay?","Nonce-based mechanisms ensuring single execution"
+SOL-AM-ReplayAttack-2,Replay,cross_chain,"Is there cross-chain replay protection?","Use chain-specific domain separators"
+SOL-AM-RP-1,RugPull,admin_drain,"Can admin pull assets from protocol?","Limit admin access; enforce timelocks"
+SOL-AM-SandwichAttack-1,Sandwich,slippage,"Does protocol have explicit slippage protection?","Allow users to specify minimum output amount"
+SOL-AM-SybilAttack-1,Sybil,user_count,"Is mechanism depending on user count?","Do not rely on user count; vulnerable to sybil"
+SOL-Basics-AC-1,AccessControl,actors,"Did you clarify all actors and interactions?","Clear understanding of actors is critical for security"
+SOL-Basics-AC-2,AccessControl,missing,"Are there functions lacking access controls?","Missing access controls expose to unauthorized changes"
+SOL-Basics-AC-3,AccessControl,whitelist,"Do addresses require whitelisting?","Whitelisting adds security against malicious actors"
+SOL-Basics-AC-4,AccessControl,transfer,"Does protocol allow privilege transfer?","Two-step transfer adds security against unintentional changes"
+SOL-Basics-AC-7,AccessControl,tx_origin,"Does contract use tx.origin?","tx.origin enables forwarded calls; use msg.sender"
+SOL-Basics-AL-9,Loop,huge_array,"Is there iteration of huge array?","Block gas limit bounds operations; ensure bounded iteration"
+SOL-Basics-AL-10,Loop,dos_in_loop,"Is there DOS potential in loop?","Single failure should not revert whole operation"
+SOL-Basics-AL-11,Loop,msgvalue_in_loop,"Is msg.value used in loop?","msg.value consistent per tx; loop use indicates accounting error"
+SOL-Basics-Math-1,Math,accuracy,"Is mathematical calculation accurate?","Verify against established rules and comments"
+SOL-Basics-Math-2,Math,precision_time,"Is there precision loss in time calculations?","Precision loss leads to significant errors over time"
+SOL-Basics-Math-4,Math,div_before_mul,"Is dividing done before multiplication?","Multiply before dividing to maintain precision"
+SOL-Basics-Math-5,Math,rounding,"Does rounding direction matter?","Rounding direction matters for user share accounting"
+SOL-Basics-Math-6,Math,div_zero,"Is there division by zero possibility?","Check denominators before division"
+SOL-Basics-Math-7,Math,overflow,"Can variables overflow in Solidity >=0.8?","Variables can exceed bounds causing reverts"
+SOL-Basics-Math-10,Math,inequality,"Should < or > be <= or >=?","Incorrect inequality causes unexpected edge behavior"
+SOL-Basics-Math-12,Math,edge_values,"What happens for min/max values?","Confirm all edge cases where terms have min/max"
+SOL-Basics-Payment-1,Payment,receiver_revert,"Can receiver revert?","Receiver contracts can deny; handle with call()"
+SOL-Basics-Payment-3,Payment,force_feed,"Are there force-feeding vulnerabilities?","Selfdestruct and other mechanisms can force-feed"
+SOL-Basics-Payment-4,Payment,dust,"What is minimum deposit/withdrawal?","Dust deposits lead to rounding and DOS"
+SOL-Basics-Payment-5,Payment,withdrawal_pattern,"How is withdrawal handled?","Pull-based approach letting users withdraw"
+SOL-Basics-Function-1,Function,input_validation,"Are inputs validated?","Validate inputs to prevent unexpected behavior"
+SOL-Basics-Function-2,Function,output_validation,"Are outputs validated?","Validate outputs to prevent unexpected behavior"
+SOL-Basics-Function-3,Function,frontrunnable,"Can function be front-run?","Ensure no unexpected risk if frontrun"
+SOL-Basics-Function-5,Function,edge_inputs,"Can edge inputs (0 max) cause unexpected behavior?","Edge values need separate testing"
+SOL-Basics-Function-6,Function,arbitrary_input,"Does function allow arbitrary user input?","Restrict low-level calls with arbitrary input"
+SOL-Basics-Initialization-1,Init,state_vars,"Are important state variables initialized?","Overlooking initialization leads to critical issues"
+SOL-Basics-Type-1,Type,forced_cast,"Is there forced type casting?","Forced casting doesn't revert on overflow"

data/solodit_checklist.meta.json

@@ -0,0 +1,13 @@
+{
+  "source_repo": "NyxFoundation/speca",
+  "source_path": "benchmarks/knowledge/solodit_checklist.csv",
+  "source_ref": "main",
+  "source_commit": "8b7da09eaf87737c1cb3b281b520a4bf71a73b55",
+  "source_blob_sha": "17810eef5e78f0ad939906590b712013e3ee8dc4",
+  "introduced_in_source_commit": "9e50ee041352ef69536d8b283c775169d5647e72",
+  "fetched": "2026-07-22",
+  "columns": ["id", "category", "subcategory", "question", "description"],
+  "n_rows": 52,
+  "role": "Reference bar for the speca#88 stage-2 quality judge (src/speca_lean4/judge.py): the judge scores these professional audit-checklist items and the generated 01e items with the same blind five-axis rubric, and the generated score distribution must be at least as good as this corpus's distribution. Calibration is on QUALITY LEVEL only — the corpus is DeFi-domain, the generated checklist is consensus-domain, and no content matching against these rows enters the verdict.",
+  "note": "The #88 direction comment describes the file as 53 items; the file at the pinned blob has 52 data rows (speca commit 9e50ee04's own message also says 52). Vendored byte-identical (LF, UTF-8, git blob sha above); tests/test_judge.py recomputes the blob sha from the vendored bytes."
+}