Lean4 FV property provider: EIP spec → `01e` properties + Kurtosis tests

[grandchildrice]

M2 · track:2-D · lean — target 7/14 (step 1) · depends on the provider-seam issue (#87) · blocks the full-EIP generation (#90) and Kurtosis reproduction (#92) issues · part of #86

Important

ステータス 2026-07-22 時点（正本 / タスク管理はこの issue を基準とする）

ゴール（gohan 確定）: spec ごとに「実装即応で汎用な 01e チェックリスト」を作ることが成果物。品質は judge harness で solodit 参照バーと比較し、vuln dataset を教材にした自己改善で仕上げる。各 spec の 01e は 02c→04 まで走らせて findings を確認して検証する。02以降の本番実行は gohan マシン。

アーキテクチャ: ① Lean4 = critical な safety/liveness spec のみ形式化 → ② その定理を背骨に judge/improve ループで 01e を作る（eval は recall でなく LLM-as-judge の品質評価、vuln dataset は improve の教材）→ ③ 02c→04 を naive な speca で走らせて findings を見る。

手順（この順で回す）:

1. gasper spec の 01e を作る ← ✅ 第1ドラフト完了（下記）
2. その 01e で 02c→04 まで走らせる（findings を見て 01e の実効性を検証）← ⬜ 次の P0
3. 並行して他 spec の 01e を作る（fab、Full-EIP property generation + bug-DB cross-check #90 方向）← ⬜
4. それらも 02c→04 で走らせる ← ⬜

今どこ: 手順1が第1ドラフト完了。手順2が未着手で、ここが次の critical path。

完了したもの:

• プラグイン基盤: v0.1.0 / speca 配線（#115）/ pin 強制（#137）/ lean provenance 貫通（#136）/ CI smoke green
• gasper 01e 第1ドラフト: plugin#21 の CHK-15（gasper-lean4 定理から派生、ethereum-vuln-dataset の実バグに紐付けた実装即応な15項目）。emit-01e --property-provider lean で 76 properties（機械 lowering 61 + CHK-15）を emit。手書き項目が proved を騙らない honesty 修正済み（descends-from-*）
• 判定ハーネス: plugin#22 の judge（5軸 blind）+ improve ループ + 収束判定。実 sonnet judge で CHK-15 = 4.04 / solodit 参照バー 2.50 → バー到達

未達 / 留保（「バー到達 = 完了」ではない）:

• 手順2（gasper 01e を 02c→04 で実走）が未着手 — この 01e で実際にクライアントの findings が出るか未検証
• CHK-15 は手書きで作ったものを judge で測っただけで、improve ループが実 LLM で未完走（sonnet/opus とも cyber safeguard に refuse）。「自己改善で作る」機構は未実証
• judge の自己選好（Claude 生成を Claude 採点）— 別系統モデルでの再確認が要る（留保3点）
• ① は gasper のみ（手順3）

優先順位: P0 = 手順2（gasper 01e = CHK-15 を 02c→04 で実走し findings 確認、gohan マシン）+ 別系統 judge で自己選好チェック / P1 = 手順3（他 spec の 01e、#90 方向）/ P2 = #92 Kurtosis 配管

プロセス: author による self-merge 禁止（approve 後にレビュア側でマージ）。チェックボックス更新には根拠 PR + 検証内容を併記。

Background

With the provider seam from #87 in place, implement the lean generation method. It takes the program graphs SPECA already extracts in 01b — the .mmd subgraphs carrying RFC-2119 invariant annotations (e.g. INV-001: Precompile MUST NOT revert) — for a given EIP, encodes the relevant invariants as Lean 4 propositions, attempts the proofs, and emits two artifacts: properties in the 01e schema, and a Kurtosis devnet test per property that checks the same invariant against a running client.

Where Lean runs — dedicated external plugin

Lean 4 execution does not live in speca. It ships as a dedicated plugin repository, NyxFoundation/speca-lean4-plugin (the heavy lean/lake toolchain stays out of the core speca dependency tree). speca references it as a version-pinned, officially-certified plugin through the plugin boundary defined in #87; the lean provider in speca invokes the plugin across that seam. Build the plugin repo, then wire speca's lean provider to it.

Tasks

• 1. Create NyxFoundation/speca-lean4-plugin: a lake-built Lean 4 workspace reusing modeling patterns from NyxFoundation/gasper-lean4, exposing a stable invocation interface (subprocess / CLI contract) that speca's lean provider calls. Pin the lean / lake version in the plugin repo, and pin the plugin version from speca (resolution point from Pluggable property providers and reproduction backends #87). Make CI install/resolve it. — ✅ v0.1.0 リリース、speca 側 pin + CI 解決は PR #115。ただし pin の「強制」(checkout 照合)は未了 → Pluggable property providers and reproduction backends #87 の残項目
• 2. Take one pilot end to end before generalizing. — ✅ パイロットは EIP-7951 から gasper に変更(方針コメント参照)。gasper-lean4 Core 定理群 → 01e で一気通貫
• 3. Per invariant: generate the Lean proposition, run the proof attempt, and record the outcome — proved, counterexample, or unknown — next to the emitted property. — ✅ plugin の provenance パイプライン(collectAxioms で sorry-free 検証 → lean_status: proved | unknown)
• 4. Emit 01e-schema properties from the provider. Carry the proof status in a provider field (lean_status), never by mutating a core field. — ✅ additive lean_* フィールドとして実装、コアフィールド無変更を PR #115 レビューで検証済み
• 5. Emit a Kurtosis fixture per property under outputs/kurtosis/<eip>/<property_id>/ (devnet config + assertion), and reference the path from the property record. — ✅ speca 実行時の fixture 実出力を #135 で実装（scaffold まで。devnet 実行は Kurtosis reproduction of confirmed findings #92）
• 6. Wire provider: lean in speca (dispatching to speca-lean4-plugin) and add a CI job mirroring 01e-properties.yml. — ✅ PR #115(properties-lean smoke ジョブ含む)
• 7. Write docs/lean-direction.md in speca — one paragraph stating the Spec→Lean4 rationale for the EF check-in (see [M2] Milestone 2 tracking #86). — ✅ #135 でマージ済み
• 8. Tests on the pilot: at least one proved property with a runnable Kurtosis fixture; output validates against the 01e schema. — ⬜ proved property の emit とスキーマ検証は✅(CI smoke)だが、runnable Kurtosis fixture が未達(Task 5 待ち)

Interfaces & contracts

• Output validates as 01e with core fields unchanged. Additive fields allowed: lean_status, lean_artifact (path to the .lean proof), kurtosis_test (fixture path).
• The lean provider talks to speca-lean4-plugin only through the Pluggable property providers and reproduction backends #87 plugin boundary — no Lean/lake dependency vendored into speca.
• Kurtosis fixtures are self-contained and runnable by the reproduction backend (Kurtosis reproduction of confirmed findings #92) with no manual edits.

Done when

• NyxFoundation/speca-lean4-plugin exists, is version-pinned, and is resolved by speca as an official plugin.(pin の強制照合のみ Pluggable property providers and reproduction backends #87 残項目)
• uv run python3 scripts/run_phase.py --phase 01e with provider: lean on the pilot produces schema-valid properties + Kurtosis fixtures.(properties は✅ / fixtures が⬜)
• At least one invariant is machine-proved in Lean and its property is emitted.(gasper Core: accountable safety k_safety'、slashable bound、plausible liveness ほか)
• Re-running is deterministic (same inputs → same properties and paths).(未検証)
• The pilot is documented well enough to add a second EIP without reading the PR.(統合パイプライン仕様は plugin PR #19 でレビュー中)

方針コメントのTODO対応状況(2026-07-02 コメント参照)

• 1. ethereum-vuln-dataset の label を整理して伝達 @grandchildrice — ✅ label_design.md 確定、データセット本体も利用可(Refine the historical vulnerability dataset #89 close 済み)
• 2. gasper-lean4 to 01e-properties @hirorogo — ⬜ 生成物(v0.1.0)は完成。fusaka 01e / ethereum-vuln-dataset との「精度整合」検証が未了(plugin の precision workstream PR #14 はマージ済み、続きは PR #19)
• 3. 主要 spec の lean4 化 @0xfab0131 @banr1 — ⬜ 現状 gasper のみ
• 4. lean 生成 01e に対して SPECA(03/04)を走らせる @hirorogo — ⬜ 未着手

Review checklist

• Lean execution lives in speca-lean4-plugin, not vendored into speca; the boundary matches Pluggable property providers and reproduction backends #87.
• Lean toolchain pinned and reproducible from a clean checkout; CI installs/resolves it.
• Core 01e fields unchanged; Lean / Kurtosis data is additive.
• Proof outcomes are recorded honestly — an unknown or counterexample is never silently dropped or relabeled proved.
• One pilot fully working beats partial coverage of many.

Out of scope

Full-set generation and bug-DB cross-check (#90). Running Kurtosis at scale (#92).

[grandchildrice]

方針

まずgasperで小さくテストする

fusaka audit contest の脆弱性をSPECAが再現できる01e出力例がここに詰まっているので、Lean4 Pluginの生成物がこれと粒度が正しく一致するか検証する

そのうえでSPECAの03/04フェーズを実行してみる

TODO

1. etehreum-vuln-datasetのlabelを整理して伝達する @grandchildrice
2. gasper-lean4 to 01e-propertiesをつくる @hirorogo (in https://github.com/NyxFoundation/speca-lean4-plugin )
   • fusaka 01eと精度が整合するまで https://github.com/NyxFoundation/speca/releases#release-bench-rq2a-20260508-speca
   • etehreum-vuln-datasetと精度が整合するまで https://github.com/NyxFoundation/ethereum-vuln-dataset/blob/main/docs/critical_high_findings.md
3. いくつか主要specについてlean4化しまくる @0xfab0131 @banr1 (in https://github.com/NyxFoundation/speca-lean4-plugin )
4. 1でつくった01eに対してSPECA走らせる @hirorogo
5. lean4 to 01e-propertiesをつくってSPECA走らせる

[grandchildrice]

label設計案
https://github.com/NyxFoundation/ethereum-vuln-dataset/blob/main/docs/label_design.md#label--the-protocol-area

[grandchildrice]

TODO 1「ethereum-vuln-dataset の label を整理して伝達する」完了報告:

• label 設計は docs/label_design.md で確定(layer / label = プロトコル領域、+ stride / cwe_top25)。
• データセット本体も data/ethereum_vulns.parquet(2,225行、スキーマは data/manifest.json)として利用可能になりました。Lean4 プラグイン側の 01e 出力との粒度検証にはこの label 軸を使ってください。

残項目(既知新規バグ4件の行追加)は #89 に記載。

[sururu-k]

TODO 2(gasper-lean4 → 01e-properties 精度整合の検証)実測 — plugin main 599d8d8c

方針コメント TODO 2 の「fusaka 01e ベンチマーク / ethereum-vuln-dataset との精度整合」を、plugin main 最新(599d8d8c, PR #19 マージ後)のコードとデータで実測した。README の既存数値(25 props 時代の M2/M3 表)との差分も含めて報告する。

測定条件(何を入力に使ったか)

• コード・データ: speca-lean4-plugin main 599d8d8c の tarball(gh api 経由取得)。
• proof health: fixture ではなく、main 599d8d8c の CI run 29739801157(conclusion: success)の成果物 lean-health-and-01e 内 lean/health.json を使用。つまり lean_status は CI 上の実 Lean 実行(lake exe speca-export、sorry-free 検証)由来。25 定理すべて resolved、25/25 proved、provenance は全件 hand-written。
• ベンチマーク: bench-rq2a-20260508-speca release(16 ファイル・186 properties)。アーカイブ sha256 a545db98…ece6b2 が manifest と一致することを確認済み。
• scope: CI と同一の tests/fixtures/bug_bounty_scope.sample.json(sample fixture。よって bug_bounty_eligible の数字はスコープ実データ由来ではない。下の限界の節を参照)。
• 実行系: Python 側パイプライン(emit-01e / verify-recall / verify-precision)をローカルで実行。Lean はローカルでは走らせていない(health は上記 CI 成果物)。

実行コマンドと生出力

emit-01e(CI と同一フラグ)

$ PYTHONPATH=src python -m speca_lean4.cli emit-01e \
    --scope tests/fixtures/bug_bounty_scope.sample.json \
    --health-json <ci-artifact>/lean/health.json \
    --out 01e_local.json --out-dir 01e_local_shards

wrote .../01e_PARTIAL_safety-accountable.json: 9 properties (9 proved, 9 bug-bounty-eligible, 8 must-establish-decomposed)
wrote .../01e_PARTIAL_safety-cases.json: 10 properties (10 proved, 10 bug-bounty-eligible, 10 must-establish-decomposed)
wrote .../01e_PARTIAL_safety-bound-witness.json: 13 properties (13 proved, 13 bug-bounty-eligible, 10 must-establish-decomposed)
wrote .../01e_PARTIAL_finality-justification.json: 10 properties (10 proved, 10 bug-bounty-eligible, 9 must-establish-decomposed)
wrote .../01e_PARTIAL_finality-quorum.json: 8 properties (8 proved, 7 bug-bounty-eligible, 5 must-establish-decomposed)
wrote .../01e_PARTIAL_finality-liveness.json: 11 properties (11 proved, 0 bug-bounty-eligible, 11 must-establish-decomposed)
total: 61 properties across 6 shard(s)
wrote 01e_local.json: 61 properties (61 proved, 49 bug-bounty-eligible, 53 must-establish-decomposed)

ローカル生成の 01e_local.json・shard 6 ファイルは、CI 成果物の 01e_lean.json・01e_lean_shards/ と byte 単位で完全一致。

verify-recall --strict

$ PYTHONPATH=src python -m speca_lean4.cli verify-recall --ours 01e_local.json --strict --out recall_local.json

label-grounded recall (domain v1-narrow, denominator: 9 in-domain of 37 vendored consensus-slice findings): 0.556 (5 covered)
  [x] lighthouse:networking:PR#9106 (beacon-chain:effective-balance-updates / consensus_divergence): covered by PROP-lean-bound-001,PROP-lean-bound-002,PROP-lean-bound-003
  [x] lodestar:scope-networking:PR#3045 (beacon-chain:effective-balance-updates / consensus_divergence): covered by PROP-lean-bound-001,PROP-lean-bound-002,PROP-lean-bound-003
  [x] nimbus:consensus:PR#3232 (beacon-chain:justification-and-finality / integer_overflow_underflow): covered by PROP-lean-justification-001,PROP-lean-justif-001,PROP-lean-justif-002
  [x] nimbus:consensus:PR#461 (beacon-chain:justification-and-finality / integer_overflow_underflow): covered by PROP-lean-justification-001,PROP-lean-justif-001,PROP-lean-justif-002
  [ ] 7c9dca6ca3831090 (beacon-chain:slashing / missing_bounds_check): UNCOVERED -> out_of_model
  [ ] bc36f78358adeec5 (beacon-chain:slashing / integer_overflow_underflow): UNCOVERED -> new_target
  [ ] lighthouse:networking:PR#1009 (beacon-chain:slashing / integer_overflow_underflow): UNCOVERED -> new_target
  [x] lighthouse:networking:PR#5037 (beacon-chain:slashing / consensus_divergence): covered by PROP-lean-slashing-001,PROP-lean-slashing-002,PROP-lean-justif-safety-002
  [ ] nimbus:consensus:PR#2392 (beacon-chain:slashing / integer_overflow_underflow): UNCOVERED -> out_of_model
gap table: {'out_of_model': 2, 'new_target': 2}
(exit 0 — strict ゲート通過)

recall レポートも CI 成果物 recall_report.json と完全一致。

verify-precision(ベンチ照合)

$ PYTHONPATH=src python -m speca_lean4.cli verify-precision \
    --ours 01e_local.json --ours-dir 01e_local_shards \
    --benchmark-dir bench/speca --out precision_report.json

benchmark corpus: 16 files, 186 properties (props/file 11.62 +/- 3.72, assertion len 93.55 +/- 14.62)
ours: 61 properties | schema validity 100% | vocabulary conformance 100%
granularity: props/file z=13.27, assertion mean z=12.13, assertion within bench 1-sigma: 2%
severity: ours {'CRITICAL': 12, 'HIGH': 30, 'MEDIUM': 19} vs bench {'CRITICAL': 95, 'HIGH': 81, 'MEDIUM': 10} | KL=0.3924 nats
label-grounded recall (D6, domain v1-narrow, denominator 9 in-domain of 37 vendored slice rows): 0.556 (5 covered, gaps: {'out_of_model': 2, 'new_target': 2})
[deprecated prose table] recall vs critical_high_findings (in-domain n=3 of 14): strict 0.333 | lenient 0.667 (full=1, partial=1)
sharded granularity: 6 files, props/file 10.17 +/- 1.72 | finality-justification=10 (z=-0.44), finality-liveness=11 (z=-0.17), finality-quorum=8 (z=-0.97), safety-accountable=9 (z=-0.7), safety-bound-witness=13 (z=0.37), safety-cases=10 (z=-0.44) | all within bench 1-sigma: True

数値まとめ

粒度整合(vs bench-rq2a-20260508-speca、16 ファイル 186 props)

指標	実測(main 599d8d8c, 61 props)	ベンチ	判定
schema validity	100%	—	整合
vocabulary conformance	100%	—	整合
props/file(shard 6 分割)	10.17 ± 1.72、全 shard z ∈ [-0.97, +0.37]	11.62 ± 3.72	全 shard 1-sigma 内(ただし後述のとおり構築による)
props/file(単一ファイル)	61(z = +13.27)	同上	不整合(想定どおり。provider 呼び出し用の後方互換形)
assertion 長	平均 270.82 ± 99.48 字、平均 z = +12.13、ベンチ 1-sigma 帯内は 61 本中 1 本(1.6%)	93.55 ± 14.62 字	不整合
text 長	平均 z = +0.92、1-sigma 内 55.7%	100.84 ± 27.17	概ね整合
severity 分布	C12 / H30 / M19、KL(ours‖bench) = 0.3924 nats	C95 / H81 / M10	分布形は依然乖離(ベンチは CRITICAL 偏重、こちらはフラット)

ラベル接地 recall(vs ethereum-vuln-dataset vendored slice、rev 3d48a9c6)

• 分母: vendored slice 37 行 → domain v1-narrow フィルタで 9 件(除外 28 件の内訳: severity Info のクロール行 20、root_cause が FFG モデル外〔missing_input_validation 等〕7、attack_path peer 1)。
• label recall = 0.556(5 / 9)。gap 4 件は全件トリアージ済み: new_target 2(slashing の overflow 系 — bc36f78358adeec5〔唯一の High 格付け in-domain 発見であり未カバー〕、lighthouse PR#1009)、out_of_model 2(slashing-protection DB / REST API 面)。
• --strict ゲート(未トリアージ uncovered・stale gap・未 emit プロパティ参照ルール)は通過、exit 0。
• 旧 prose ベース recall(strict 0.333 / lenient 0.667、分母 3)は recall_prose_deprecated としてのみ報告される。分母定義が違うため label recall と直接比較不可。

再現性・決定性

• ローカル実行(Windows / Python 3.12)の emit-01e 出力・recall レポートが CI(ubuntu / Python 3.11)成果物と byte 一致。
• verify-precision / verify-recall をそれぞれ 2 回実行し、レポート JSON が完全一致。
• issue の Done when にある「Re-running is deterministic(未検証)」のうち、パイプライン手順 [2]-[5](Python 側)は同一入力 → 同一出力を実測で確認できた。手順 [1](Lean export)の決定性はローカルに Lean 環境がないため未検証。

README 既存数値との突合(食い違い)

1. assertion 長が大きく悪化しており、README に未記載。 README の M0-M3 表(25 props、1:1 時代)は assertion mean z = -0.2 だが、B1 must-establish 分解後の現 main(61 props)では mean z = +12.13、1-sigma 帯内 1.6%。README の「post-decomposition」段落は props/file の 1-sigma 整合と severity 分布は載せているが、assertion 長の退行に触れていない。原因は分解ではなく assertion 本文の構造で、非分解の base 8 本が平均 379.5 字、-me 53 本が平均 254.4 字と、どちらもベンチ平均 93.6 字の 3-4 倍(Lean pretty-print の仮説・結論を条件文として埋め込む形式のため)。
2. KL は README 表の 0.6004 nats(25 props)から 0.3924 nats に変化(61 props での再計測)。README 本文はこの更新値を未記載。
3. それ以外(shard 全 6 ファイル 1-sigma 内、severity C12/H30/M19、label recall 0.556、schema/vocab 100%)は README の記述と実測が一致した。

解釈(良く見せないための注記)

• 「props/file が 1-sigma 内」は構築による整合であって創発的な整合ではない。 shard 境界は theorem_map.json で人手チューニングされており、M3 の目的自体が「ベンチ粒度帯に載せるための分割」だった。指標がその設計目標を満たしたことの確認であり、独立な検証ではない。
• recall の「covered」は (label, root_cause) クラス単位の人手ルールによる主張。 label_match_rules.json の rationale は人が書いた判断で、機械検証されるのは構造整合(参照プロパティが実 emit されておりラベルが一致すること)のみ。個別 finding と Lean 定理の意味的対応を検証したものではない。分母 9 も小さく、domain 定義 v2(missing_input_validation 等を追加予定)に成長させれば recall は下がる方向。
• lean_status: proved 61 件は「61 個の無条件事実」ではない。 61 props の内訳は base 8 + must-establish 分解 53。-me プロパティの proved は「親定理が Lean で条件付きに証明済み」の意味で、assertion 文も「implementation must preserve [前提]; if so, …」という条件形。実装が前提を満たすかは Kurtosis 側(Task 5、未達)の領分。
• kurtosis fixture は scaffold であり何も実証しない(verdict: null、devnet 実行なし)。今回の測定はすべて 01e 生成物と静的データの照合であり、実装検証は含まれない。
• カバレッジは gasper Core(FFG)のみ。 LMD-GHOST、BLS 内部、eth1 ops、OOM/DoS 系は構造上モデル外。ベンチ 16 ファイルも Ethereum 固有ではない汎用 rq2a コーパス(libsass、memcached、linux 等)であり、粒度・語彙の分布比較としてのみ意味を持つ。
• scope が sample fixture。 bug_bounty_eligible 49/61 は tests/fixtures/bug_bounty_scope.sample.json 由来で、実 speca run の BUG_BOUNTY_SCOPE.json に対する数字ではない。
• gasper_ref が main で sha 固定されていない。 theorem_map.json の gasper_ref: main のため、Lean 側の証明状態は CI 実行時点の gasper-lean4 main に依存する。再現性の観点では固定化が望ましい。

自己改善ループ所見

• 1周目: (i) 当初 theorem_health.sample.json(fixture)を使う予定だったが、main の CI 成果物に実 Lean 実行由来の health.json があることを確認し、そちらに切替(fixture 数値の混入を回避)。(ii) ベンチアーカイブ sha256 の manifest 照合 OK。(iii) ローカル出力 = CI 成果物の byte 一致を確認。(iv) README 未記載の assertion 長退行(z=+12.13)を検出。
• 2周目: (i) 「1-sigma 内」がチューニング構築による点を明示することにした。(ii) recall のルールベース性(人手 rationale、クラス単位マッチ)を分母・分子の定義リスクとして明記。(iii) 唯一の High 格付け in-domain finding が未カバーであることを確認。(iv) -me 53 件の proved の意味論(条件付き)を確認。(v) 分母 37→9 の除外内訳(Info 20 / root_cause 7 / attack_path 1)を全件確認。(vi) gasper_ref 未固定を検出。
• 3周目: 報告済み z 値・比率を独立再計算(props/file z 13.27、assertion z 12.13、1-sigma 内 1/61=0.016、5/9=0.556)し全一致。verify-precision / verify-recall の再実行でレポート JSON 完全一致。新規 findings なしにつき終了。

確認できなかったこと

• Lean export(手順 [1])のローカル再実行と決定性(Lean toolchain 未導入。health は CI 成果物を信頼)。
• 実 speca run の scope での bug_bounty_eligible。
• ルール rationale の意味的妥当性(例: nimbus PR#3232 は dataset ラベル上 justification-bits overflow だが、PR タイトルは REST JSON 関連。dataset のラベル付けを ground truth として受け入れた)。
• Kurtosis fixture の実行(scaffold のみ、devnet 未実行)。

[sururu-k]

TODO 4（lean 生成 01e に SPECA 03/04）実行結果

方針コメントの TODO 4「lean 生成 01e に対して SPECA(03/04) を走らせる」を実行した。結論から言うと 01e(lean) → 02c → 03 → 04 は最後まで通り、Lean 由来 property から CONFIRMED_POTENTIAL の finding が 1 件出た。ただしその finding は再実行で再現しなかった。 以下、実行の生ログ・成果物・できなかったことを含めて報告する。

実行環境: ブランチ feat/issue-88-lean-kurtosis-fixtures（PR #135、main 未マージ）, speca HEAD 2d9a749e。

---

0. 前提の整理: 03/04 とは何か、何が必要か

scripts/orchestrator/config.py の PHASE_CONFIGS を読んだ結果、01e から 04 までの依存は次の通り。01e の直後に 03 は来ない。間に 02c が必須。

phase	入力	出力	model	実体
01e	01b_PARTIAL_*.json	01e_PARTIAL_*.json	(provider)	lean provider は Claude を呼ばない
02c	01e_PARTIAL_* + 01b_PARTIAL_*	02c_PARTIAL_*.json	sonnet	Claude CLI セッション、コード位置解決
03	02c_PARTIAL_*	03_PARTIAL_*.json (audit_items)	sonnet	property 1件=1セッション、最大50ターンの3段階形式監査
04	03_PARTIAL_*	04_PARTIAL_*.json (reviewed_items)	sonnet	FP フィルタ3ゲート + severity 較正

03/04 は Claude CLI を必須とする経路（scripts/orchestrator/runner.py _build_cmd）。加えて 04 の load_items は BUG_BOUNTY_SCOPE.json / TARGET_INFO.json / 01b_SUBGRAPH_INDEX.json の存在を強制する（無いと PhaseAbortError）。03 の worker prompt は解析対象リポジトリが target_workspace/ に clone されている前提。

このため以下を用意した:

• target_workspace/ = ethereum/consensus-specs @ 8c12caee279d77b322446d33440b37479117dcde（gh api tarball 経由。git push/直DL は egress 制限で固まるため）
• TARGET_INFO.json を手書き（0c は SPECA_TARGET_WORKSPACE + git メタデータを要求するが tarball 展開には .git が無い）
• BUG_BOUNTY_SCOPE.json / 01b_PARTIAL_ci_smoke.json は lean 01e 生成時のものを流用

対象を consensus-specs にしたのは、gasper-lean4 Core 定理群が制約するのが Gasper の justification/finalization/slashing であり、その実行可能な参照実装が pyspec だから。

---

1. 途中で止まった箇所と、その切り分け

最初の 02c 実行は全バッチ失敗した。 生ログ:

[W0] Batch 0: subtype=success but no parseable results found
[W0] Batch 0 result snippet: API Error: Sonnet 5 has safety measures that flagged this
message for a cybersecurity topic. To learn about the Cyber Verification Program and
apply for access, visit our help center: ...
[W0] Claude failed for batch 0 (exit 1)
WARNING: Phase 02c produced 0 batch successes despite $0.47 spent.
Phase 02c aborted: Phase 02c: 2 batch(es) failed

これを lean 固有の問題と取り違えないため、2軸で切り分けた:

cwd=C:\tmp\speca  + --model sonnet + プロンプト "Reply with exactly: OK"  → 上記の API Error
cwd=C:\tmp\speca  + --model haiku  + 同じプロンプト                       → "OK"
cwd=C:\Users\...  + --model sonnet + 同じプロンプト                       → "OK"
cwd=C:\tmp\speca  + --model opus   + 同じプロンプト                       → "OK"

つまり 無害なプロンプトでも speca リポジトリを cwd にした Sonnet 5 だけが拒否される。lean 由来 property とも、assertion の形式とも、01e の内容とも無関係の環境要因（speca の repo context が Sonnet 5 の cyber safeguard を踏む）。02c/03/04 の PhaseConfig はいずれも model="sonnet" なので、この環境では既定構成のまま 03/04 は走らない。 以降は --model で回避した。

なお同時に出ていた Ignoring 18 permissions.allow entries ... this workspace has not been trusted は runner が --dangerously-skip-permissions を渡すため実行の阻害要因ではない。信頼設定の書き換えは権限設定の変更にあたるため行っていない。

---

2. 実行したコマンドと結果

02c（全 54 property、haiku）

uv run python scripts/run_phase.py --phase 02c --workers 1 --max-concurrent 1 --model haiku --force

  ✓ outputs\01e_PARTIAL_W0B0_1784548876.json: 54 properties validated
Loaded 54 items
  Severity gate: min_severity=Low (dropping below)
Early exit: 0 items
To process: 54 items
✅ Phase 02c completed in 215.6s
   Total results: 54

54/54 が resolution_status: resolved、全件 resolution_method: grep_fallback、解決先は specs/phase0/beacon-chain.md。シンボルと行範囲を実ファイルと照合して正しいことを確認した（例: process_slashings → L1782、実際の def process_slashings も L1782）。severity gate は CRITICAL/HIGH/MEDIUM の大文字表記でも Severity.from_str が .capitalize() するため通過し、0件も落ちていない。

03（opus）

property 1件 = 1 Claude セッション最大50ターンなので 54 件全部は現実的でなく、代表サブセットで2ラウンド実施した。

ラウンド1（process_justification_and_finalization を covers する 6 件、定理ファミリを分散）:

✅ Phase 03 completed in 260.1s / Total results: 6 / Batch successes: 6 / Batch failures: 0 / $1.74

→ 6件すべて not-a-vulnerability。

ラウンド2（process_slashings / process_effective_balance_updates を covers する 9 件）:

✅ Phase 03 completed in 388.8s / Total results: 9 / Batch successes: 9 / Batch failures: 0 / $2.55

→ not-a-vulnerability × 8、potential-vulnerability × 1（PROP-lean-bound-001-me1）。

04（opus）

uv run python scripts/run_phase.py --phase 04 --workers 2 --max-concurrent 2 --model opus --force

Loaded 9 items
Early exit: 8 items
To process: 1 items
✅ Phase 04 completed in 64.8s

04 の apply_early_exit は vulnerability / potential-vulnerability のみを LLM に回すので、ラウンド1（全件 not-a-vulnerability）では LLM レビューが一度も走らず全件 PASS_THROUGH だった。ラウンド2でようやく実レビュー経路を踏み、CONFIRMED_POTENTIAL が出た:

{
 "property_id": "PROP-lean-bound-001-me1",
 "review_verdict": "CONFIRMED_POTENTIAL",
 "original_classification": "potential-vulnerability",
 "adjusted_severity": "High",
 "reviewer_notes": "Gate 1 passed: process_effective_balance_updates has 6 non-test callers
  (process_epoch at phase0 L1428, altair L653, capella L322, electra L903, fulu L375, gloas
  L1137) ... Gate 2 passed: BUG_BOUNTY_SCOPE.json declares no trust_assumptions, and Phase 03's
  attack path enters via attestation withholding on p2p:beacon_attestation, a listed untrusted
  entry point. Gate 3 passed: ... in-scope 'consensus layer: fork choice, justification,
  finalization' ... verdict is CONFIRMED_POTENTIAL since the decrease-side gap (inactivity-leak
  and slashing penalties propagating into weight without consuming act or ext) is a concrete
  deviation from the Lean bound, but reaching an actual conflicting k-finalization below the
  bound requires an unquantified >1/3 offline share sustained across a long leak.",
 "spec_reference": "specs/phase0/beacon-chain.md::process_effective_balance_updates::L1814-1828"
}

内容としては「Lean の slashable_bound は stake 乖離の原因を activation churn と exit churn だけに限定しているが、pyspec では inactivity leak / slashing penalty による effective_balance 減少がどちらの churn も消費せずに weight に伝播するので、その bound が成立しない」という指摘。Lean 側の仮説が実装で成り立たない箇所を突いており、Lean 由来 property の狙い通りの当たり方をしている。

---

3. 検証結果

3-1. additive フィールドは下流で「誤解釈」される前に消える

これが今回いちばん確度の高い発見。lean_status / lean_artifact / kurtosis_test は 02c の時点で 100% 落ちる。実測:

02c full-set entries: 54
  lean_status:   0/54
  lean_artifact: 0/54
  kurtosis_test: 0/54

原因は設定側のホワイトリスト。base.py は 01e の provider 経路で明示的に

# 01e (base.py _run_01e_with_provider)
self.config.output_fields = []   # "additive provenance fields ... must survive into the PARTIAL"

として 01e では additive フィールドを守っているが、02c に同等の免除が無い:

02c context_fields = [property_id, text, type, assertion, severity, covers, reachability, exploitability, _id_prefix]
02c output_fields  = [property_id, text, type, assertion, severity, covers, reachability, exploitability, code_scope, code_excerpt]
03 context_fields  = [... code_scope, code_excerpt]      # lean_* なし
04 context_fields  = [property_id, audit_result, text, assertion, covers, severity, type]  # lean_* なし

帰結:

• issue 本文の契約「Additive fields allowed: lean_status, lean_artifact, kurtosis_test」は 01e artifact の中でしか成立していない。1ホップで消える。
• Kurtosis reproduction of confirmed findings #92 の Kurtosis 再現バックエンドは詰む。 Phase04Orchestrator.run は self.results（= 04 の reviewed_items）を verification backend に渡すが、そこに kurtosis_test は無い。Task 5 で fixture を出しても、現状の配線では 04 から参照経路が繋がらない。

3-2. proved は下流で「検証済み」として過大評価されていない（ただし設計ではなく偶然）

03 は lean_status: proved を一度も見ていない（3-1 の通り落ちている）。それでも Lean のセマンティクスは assertion の自然言語テキスト経由で漏れて届いている（assertion が "... if so, k_safety' guarantees [...]" の形で定理名と結論を埋め込んでいるため）。実際 03 の proof_trace は定理名を名指しする:

The residual gaps (validator-set churn changing total_active_balance across epochs, and is_slashable_validator refusing slashing past withdrawable_epoch) are exactly the theorem's fixed-vset/stake hypotheses and are the documented weak-subjectivity assumption (specs/phase0/weak-subjectivity.md L65-72), not an implementation gap.

重要なのは 03 が「Lean で証明済みだから OK」で済ませず、pyspec の行番号を挙げて論証を再構築し、Lean の仮説と実装のズレを残余ギャップとして分離している点。正直さの観点では合格。ただし これは設計的な担保ではない。lean_status が構造化フィールドとして届いていたら過大評価される余地はあり、いま守られているのは単にフィールドが落ちているからである。

なお artifact 側には別の正直さの問題がある。54件すべてが lean_status: proved だが、同じ 54 件すべての lean_proof_source が "... (model parameters elided in sample fixture) ..." で省略されており、lean_type_consistency は ok 35 / unchecked 11 / 欠損 8。証明本体が省略された状態で proved が一律に立っている。

3-3. assertion 形式（Lean pretty-print 埋め込み）の 03/04 への影響

この artifact での実測は assertion 平均 194.1 字（最小 96 / 最大 336）、text 平均 123.0 字。事前に共有された「平均 270 字・z=+12.13」は再現できなかった（prompt provider 側の比較コーパスがローカルに無く、独立検証もできていない）。数値の食い違いは測定対象フィールドの違いの可能性がある。

処理への悪影響は観測されなかった:

• 03 は 9件中9件、6件中6件がバッチ成功、リトライ 0、空結果 0、スキーマ検証警告 0。
• assertion に含まれる Unicode 数式（τ, ∩, ≤, ∃, ⋯）は 02c/03/04 を素通りした。ローカル Windows コンソールでは cp932 で表示できないが、run_phase.py の _configure_io_for_utf8() が吸収しており実行は壊れない。
• 03 の出力スキーマは prompt provider の実データ（sherlock-rq1/nethermind_fusaka の 03_PARTIAL 18件）と完全に同形: [attack_scenario, checklist_id, classification, code_path, proof_trace, property_id]、severity は両方とも未設定。04 も同形。

一方で別種の悪影響が見つかった。lean 側の covers 割り当てが不正確な場合がある。slashable_bound（quorum 重みの定理）が covers: process_effective_balance_updates に割り当てられており、02c はそれを字義通り解決してしまう。03 は自力で訂正した:

02c が解決した位置: specs/phase0/beacon-chain.md::process_effective_balance_updates::L1814-1832
03 が実際に監査した位置: specs/phase0/beacon-chain.md::weigh_justification_and_finalization::L1509-1533

03 が救っているだけで、02c 単体では誤った位置を出している。

3-4. 03 の判定は再実行で再現しない

上記 CONFIRMED_POTENTIAL の元になった 03 の判定を、同一入力・同一モデルで 2 回追試した:

実行	classification	指摘した機構	code_path
1回目	potential-vulnerability	inactivity leak / slashing penalty が churn を消費せず weight に伝播	phase0 process_effective_balance_updates L1814-1828
2回目	not-a-vulnerability	同じ drift を認識した上で「hysteresis / MAX_EFFECTIVE_BALANCE 等の設計定数で意図的に bounded」と判断	phase0 process_effective_balance_updates L1814-1828
3回目	potential-vulnerability	Electra の churn カウンタが3分割で consolidation 分が別勘定	electra process_consolidation_request L1940-1949

verdict が 3回中2回で割れるだけでなく、3回とも指摘している機構が違う。したがって「lean 生成 01e から SPECA が finding を出す」は再現性のある性質としては主張できない。今回 04 の LLM レビュー経路まで到達できたこと自体が 1/3 の分岐に依存している。

3-5. 01e(lean) の決定性と provenance

入力が本当に lean 由来であることは確認した。outputs/ に置いた 01e は 1 ファイルのみで、lean provider 実行時の成果物と sha256 一致（c38eba11a6fd...）、54件全件が lean_status / lean_artifact / lean_proof_code を保持。

ただし 54 という数を単発実行で再現できなかった:

uv run python scripts/run_phase.py --phase 01e --property-provider lean --output-dir <tmp>
→ lean provider: 18 Kurtosis fixture scaffold(s) ... (7 properties without an Executable checker keep kurtosis_test null)
→ lean provider: 25 properties from NyxFoundation/speca-lean4-plugin@v0.1.0

pin されている v0.1.0 相当の plugin で単発 emit すると 25 properties / 18 fixtures / 7 null。今回監査に使った 54 件は protocol area ごとに 6 分割した shard emit（合計 61 件）の部分集合であり、25 件との id 重複はわずか 8 件。同一 plugin 状態内では決定的（2回実行して output-dir 差分を除き完全一致）だが、plugin 状態をまたぐと property 集合が入れ替わる。issue の Done-when「Re-running is deterministic」は、plugin 状態を固定した条件付きでしか成り立たない。

---

4. できなかったこと・確認できていないこと

• 既定構成（sonnet）での 03/04 は走らせていない。 この環境では Sonnet 5 の cyber safeguard が speca リポジトリの context で無害なプロンプトごと拒否するため、02c は haiku、03/04 は opus で実行した。モデル差が結論に与える影響は測っていない。
• 54 件全部は 03 に通していない。 03 はサブセット計 15 件（ラウンド1: 6 件、ラウンド2: 9 件）+ 追試 2 件。全数実行の分布は不明。
• 02c は haiku で実行しており、コード位置解決の品質は本番相当ではない。ただし 03 は 02c の位置を自分で訂正して監査しているため（3-3）、03 の結論が haiku 品質に制約された形跡は無い。
• prompt provider 由来 property との同一条件比較は行っていない。 3-3 の比較は既存の fusaka 実行成果物（別ターゲット・別時期）とのスキーマ形状の照合に留まる。assertion 長の 270 字 / z=+12.13 は独立に再現できていない。
• Kurtosis fixture の実行はしていない。 KurtosisVerificationBackend.verify は NotImplementedError を投げる未実装スタブで、そもそも kurtosis_test が 04 まで届かない（3-1）。
• 05 は走らせていない（TODO 4 の範囲外）。

---

5. 提案（issue のチェックボックスは触っていない）

1. 02c/03/04 の context_fields / output_fields に lean provenance の免除を入れる。 最低でも kurtosis_test を 04 まで通さないと Kurtosis reproduction of confirmed findings #92 の再現バックエンドが機能しない。01e で output_fields = [] にしている意図が 1 ホップで無効化されている。
2. lean_status を下流に通すなら、同時に過大評価防止の明文化が要る。 現状 03 が健全なのはフィールドが落ちているためで、通した瞬間に「proved だから検証済み」に倒れる余地がある。
3. lean_proof_source が省略された状態の proved は、Review checklist の「Proof outcomes are recorded honestly」に照らして再確認が必要。
4. lean → 01e の covers 割り当ての精度（slashable_bound → process_effective_balance_updates など）を見直すと 02c の誤解決が減る。
5. 03 の判定ゆらぎは Lean 由来 property 固有かどうか未検証。prompt provider 側でも同様なら SPECA 全体の性質であり、別 issue で扱う価値がある。

---

再現用の成果物はローカルの C:\tmp\speca\outputs\ 配下（02c_PARTIAL_*, 03_PARTIAL_* 9件, 04_PARTIAL_*, 追試は _round2_backup/rerun{1,2}_03.json）に残してある。

[grandchildrice]

【統合済み・無効】 このコメントの内容は二転三転したため、#88 確定方針コメントに統合して無効化しました。対応はそちらだけ見てください。（履歴として本文は残置）

元の内容（参照用・無効）

方針の再設定(2026-07-20): #88 は EF grant の成果物として最優先。作業が critical path から逸れています

論文(RQ/査読)側の都合は一旦この issue から切り離します。#88 は EF Grant M2 の 2-D 成果物であり、評価軸は「Lean で検証した spec 由来の property が、実際のクライアント監査で実バグを出せるか」の一点です。以下はその軸だけで判断しています。

1. 意図するアーキテクチャ(確定)

3段構成です。これは本 issue の 2026-07-02 方針コメント TODO の 3 / 4 と同じもので、新方針ではなく元の意図の再確認です。

段	役割	責務の境界
① Lean4 プラグイン	Ethereum の critical な safety / liveness property の spec のみを重点的に形式化する	ここで作るのは「機械検査された事実」。01e の最終形ではない
② 01e 生成	①の Lean4 コード + ethereum-vuln-dataset を入力に、LLM が 01e を生成する	Lean が「何が成り立つべきか」、dataset が「実際にどう壊れてきたか」を与え、LLM が実装監査向けの property に落とす
③ 02c → 03 → 04	naive な speca をそのまま流し、全クライアントを監査する	Lean 非依存。property の出自を問わず等価に扱う

2. 現状との差分 — ②が存在しません

①は gasper のみですが方向は合っています。③は #91 の設計(left stage once / right stage per implementation)と整合します。問題は②です。

• base.py:779-781 — provider が prompt 以外だと Claude CLI のバッチループを丸ごと迂回します。lean パスに LLM は一切通りません。
• 01e の中身はプラグインの emit-01e / emit-kurtosis による Lean 定理からの決定論的な 1:1 lowering です。
• LLM 的な拡張の唯一の継ぎ目 run_refinement_pass は providers.py:426 で no-op、既定も False。
• ethereum-vuln-dataset が生成に一切効いていません。 DatasetPropertyProvider.generate() は NotImplementedError(providers.py:387-396)。provider は排他選択なので、「Lean と dataset の両方から1つの property を作る」状態が現在の型では表現できません。

結果として、property 数はLean を書いた本数が上限(現在 gasper 54件)になり、過去バグの知見はゼロ寄与です。grant の評価軸が「実バグを出せるか」である以上、ここが効いてきます。

3. 優先順位の是正

直近3本の PR(#135 Kurtosis fixture / #136 lean フィールドの 02c-04 貫通 / #137 pin 強制)は、いずれも #92(8/22)と #87 のためのインフラです。品質は高いのですが、#88 自身の critical path である方針TODO の 3 と 4 が手つかずのまま、後段の配管が先行しています。

• 3. 主要 spec の lean4 化 @0xfab0131 @banr1 — ⬜ 現状 gasper のみ
• 4. lean 生成 01e に対して SPECA(03/04)を走らせる @hirorogo — ⬜ 未着手

4 が未着手であることが最大のリスクです。①→③の一気通貫がまだ一度も通っておらず、「Lean 由来の property で本当にクライアントの findings が出るのか」が誰も検証していない状態で、その先の再現(#92)の配管だけが積み上がっています。ここで前提が崩れると積んだ配管ごと無駄になります。

優先順位を以下に固定します。

優先	内容	対応
P0	方針TODO 4: lean 生成 01e で 02c→03→04 を1クライアント分だけ完走させ、findings を見る	配管より先。今週中
P0	②の設計(Lean 出力 + dataset → LLM で 01e 生成)を決める	下記
P1	方針TODO 3: gasper 以外の critical spec の Lean4 化	①の範囲拡大
P2	Task 5 / #92 関連の配管(#135 ほか)	P0 の結果を見てから

4. ②の実装方針(要議論、独断では決めません)

現在の --property-provider lean は「LLM を迂回する」設計で、②とは非互換です。素直な形は:

• lean プラグインの出力を 01e の最終形ではなく、prompt パスへの入力コンテキストとして扱う(証明済み定理の言明・lean_status・checker 参照)
• 01e 生成は **prompt パス(LLM)**に戻し、そこに Lean 由来コンテキストと ethereum-vuln-dataset の該当行を注入する
• lean_status 等の provenance は、LLM が名乗るのではなく注入元から決定論的に付与する

注意点として、これは #136 でマージ済みの passthrough_fields の前提と衝突します。 #136 は「worker はこれらのフィールドを受け取らないので、worker 由来の値は捏造とみなして落とす」という trust model ですが、②では worker が Lean コンテキストを受け取る側になるため、規則の置き直しが必要です。#136 の機構自体は活かせますが、②の設計を確定してから調整します。

@hirorogo @banr1 P0 の 2 件について、今週中に着手可否と見積もりをこの issue に返してください。②の実装方針に異論があれば併せてお願いします。

5. プロセス(重要)

#136 と #137 が author 自身によって self-merge されています。

• fix(orchestrator): carry lean provenance fields (lean_status/lean_artifact/kurtosis_test) through 02c/03/04 #136: 私が「技術的には approve だが、方針確認のためマージは保留」と明記したレビューの約30分後に author がマージ
• feat(providers): operative plugin version pins + pre-seam-anchored default-path identity guard (#87 Tasks 6/8) #137: レビュー0件のまま author がマージ

main の CI は green(3dfa9224 で全ジョブ success)なので実害は出ていませんが、#133 で main を壊しかけた経緯がある以上、この運用は続けられません。以後 speca の PR は author による self-merge を禁止とし、レビュアの approve 後にレビュア側でマージします。保留を明記したレビューは保留として扱ってください。

あわせて、タスクの状況管理はこの issue 上で行うことを徹底します。PR 本文の自己申告ではなく、issue のチェックボックスを正本とします。チェックを進める際は根拠 PR と検証内容を併記してください。

[grandchildrice]

【統合済み・無効】 このコメントの内容は二転三転したため、#88 確定方針コメントに統合して無効化しました。対応はそちらだけ見てください。（履歴として本文は残置）

元の内容（参照用・無効）

@sururu-k @0xfab0131

前のコメントで方針を書きましたが、リポジトリが6個に分かれていて全体像が見えにくくなっているので、いったん全部説明し直します。今どこがつながっていて、どこが切れているのかを共有したいです。長くなりますが、読んでから作業を再開してください。

それぞれのリポジトリが何をする場所か

speca が本体です。監査パイプラインが 01a → 01b → 01e → 02c → 03 → 04 の順で走ります。前半（01系）が「何を検査すべきか」を決める工程、後半（02c以降）が「対象クライアントのコードを実際に監査する」工程です。この境界が今回いちばん大事なので覚えておいてください。

gasper-lean4 は Lean 4 で Gasper を形式化したリポジトリです。ここはすでに完了していて public になっています。ここで証明した定理が、監査で使う property の元ネタです。

gasper-lean4-formal-verification は、その前身です。6/29 に gasper-lean4 が作られてから引き継がれました。今は使いません。

speca-lean4-plugin は、speca と Lean の間に挟まる橋渡しです。speca に lean や lake の重いツールチェーンを持ち込みたくないので分けてあり、speca はプラグインをバージョン固定で外から呼ぶだけ、という関係です。それに加えて、gasper 以降の形式化作業はこのリポジトリに集約する方針にしています。lean/（lakefile.lean / SpecaExport/）が Lean のワークスペースです。新しく spec を Lean 化するときは、gasper-lean4 に足すのではなくここに入れてください。

ethereum-vuln-dataset は、11クライアントの過去の実バグを STRIDE / CWE ラベル付きで集めたものです。これが後で効いてきます。

kurtosis-harness は、監査で見つけた findings を devnet で実際に再現するためのものです。これは #92 の話で、まだ先の工程です。

本来やろうとしている流れ

3段です。

① Lean で spec を形式化する。 ただし全部ではなく、Ethereum の critical な safety / liveness property に絞って深くやります。ここで作るのは「機械検査された事実」であって、監査に使う property そのものではありません。ここを取り違えると後段の設計が全部ずれます。

② Lean のコードと ethereum-vuln-dataset の両方を入力にして、LLM に 01e を書かせる。 Lean が「仕様上なにが成り立つべきか」を、dataset が「実際のクライアントでどう壊れてきたか」を与えて、LLM がその2つを突き合わせて実装監査向けの property に落とす、という組み立てです。

③ 02c 以降は素の speca をそのまま流して、全クライアントを監査する。 ここは Lean のことを何も知らなくていい。property がどこから来たかに関係なく同じ扱いをします。

今の実装は②が丸ごと抜けています

これが今回いちばん伝えたいことです。

--property-provider lean を指定すると、base.py:779-781 で Claude CLI のバッチループを丸ごと迂回します。つまり lean のパスには LLM が一枚も入っていません。プラグインが emit-01e で Lean の定理を1対1で機械変換したものが、そのまま 01e の最終出力になっています。

LLM で膨らませるための継ぎ目は用意されているのですが、providers.py:426 の run_refinement_pass は中身が空（no-op）で、有効化フラグも既定 off です。

そして ethereum-vuln-dataset が生成に一切効いていません。DatasetPropertyProvider.generate() は providers.py:387-396 で NotImplementedError を投げるだけです。しかも provider は排他選択なので、「Lean と dataset の両方を見て1つの property を作る」という状態が今の型では表現できません。

結果どうなっているかというと、property の数が「Lean を書いた本数」で頭打ちになります。今 gasper で54件です。過去バグの知見はゼロ寄与です。EF grant の評価軸は「実際にクライアントのバグを見つけられるか」なので、ここが効いてきます。

sururu-k へ

まず、書いているコードの質は高いです。#136 で 54件中0件が 02c で落ちているのを実測から特定した進め方も、early-exit のバッチ衝突を自分で見つけて直したのも良かったです。そこは疑っていません。

問題は向いている方向です。#135（Kurtosis fixture の出力）、#136（lean フィールドを 02c-04 に貫通させる）、#137（pin の強制）は、3本とも #92 と #87 のための配管です。上の図でいうと ③ より後ろの工程の準備です。

一方で ①→③ の一気通貫がまだ一度も通っていません。「Lean 由来の property を流したとき、クライアントのコードから本当に findings が出るのか」を誰もまだ見ていない状態で、その先の再現の配管だけが積み上がっています。もしここで前提が崩れたら、積んだ配管ごと作り直しになります。先に一本通してください。

もう一つ、設計上の話です。#136 は「worker はこれらのフィールドを受け取らないのだから、worker が出してきた値は捏造とみなして落とす」という trust model で作られています。この判断は今の構成では正しいのですが、②を入れると worker（LLM）が Lean のコンテキストを受け取る側になるので、前提ごと置き直しになります。#136 の機構自体は活かせるはずなので、捨てるという話ではありません。ただ②の設計が決まるまで、この方向にこれ以上積まないでください。

マージの件

まず訂正から。前のコメントで私が書いた「pilot テストの失敗が silent green になる」という指摘は誤りでした。 #135 のレビューで blocking として出したものですが、成立していません。

該当ステップの run: ブロックは冒頭で set -euo pipefail を実行しています（PR #135 時点で既に L138 にありました）。スクリプト内の set -o pipefail はそれ以降のパイプライン全体に効くので、pytest ... | tee の失敗はきちんと伝播します。pytest が落ちればジョブは赤くなります。

私のミスは調べ方です。shell: の指定と defaults.run.shell の有無だけを grep して、「shell: bash が無い → pipefail が無い」と結論しました。run: ブロック自身が set で pipefail を立てている可能性を確認していません。手元で bash -e と bash -eo pipefail の差を実測して裏取りした気になっていましたが、検証したのは GitHub の既定シェルの一般論であって、実際のスクリプトではありませんでした。結論を出す前に対象そのものを読むべきでした。すみません。

したがって #135 に実害はなく、main は壊れていません。#139 / #140 で対応してもらった shell: bash の追加も、バグ修正ではなく多重防御です（両 PR の本文で前提の誤りを正確に指摘してもらっていて、そのとおりです）。

そのうえで、マージの進め方については指摘を維持します。こちらは技術的な当否とは別の話です。

#135 は CHANGES_REQUESTED のまま 13:37 に、#136 は私が「マージは保留」と明記した約30分後に、#137 と #138 はレビュー0件で、いずれも author 自身がマージしています。#138 に至っては、私が self-merge をやめてくださいと書いた 14:23 の9分後に作成して 14:39 にマージされています。

特に #135 についてお願いしたいのは、その場で反論してほしかったということです。私の指摘は間違っていたわけですが、PR には一言も返信がないまま merge されました。「L138 に set -euo pipefail があるので前提が違います」と書いてもらえれば、私はその場で撤回していました。黙ってマージされると、こちらは間違ったまま次の判断に進みます。実際そうなって、前のコメントで事実と違うことを書きました。

レビューは通す通さないの関門ではなく、認識を突き合わせる場だと思っています。おかしいと思ったら遠慮なく反論してください。そのうえで、マージ自体は approve 後にレビュア側で行います。

0xfab0131 へ

gasper-lean4 は完了・public 化まで終わっているので、そこは問題ありません。お疲れさまでした。

お願いしたいのは、次の形式化の置き場所を移してもらうことです。上に書いたとおり、gasper 以降の形式化は speca-lean4-plugin の lean/ に集約する方針にしています。プラグイン側は今 sururu-k と hirorogo が触っていて、あなたのコミットがまだ入っていません。Lean の中身を一番分かっているのはあなたなので、ここに合流してほしいです。最初に lean/SpecaExport/ と docs/pipeline.md を見て、gasper の定理がどう 01e に降りているかを確認してもらえると早いと思います。

細かい点ですが、gasper-lean4-formal-verification#5（[add] usecses - #5 Develop/sketch）が 6/24 から開いたままです。このリポジトリはもう使わないので、中身が生きているなら移し、終わっているならクローズしてください。開けたままだと後から入った人が必ず迷います。

そのうえで判断してほしいのが、gasper の次にどの spec を Lean 化するかです。この issue の 2026-07-02 方針コメントの TODO 3「主要 spec の lean4 化」が、あなたと banr1 のアサインで残っています。これが #90（目標 7/31、残り11日）の前提になっていて、Lean 側が gasper だけだとカバレッジを測る対象が揃いません。全体の律速はここです。

候補の選定に迷うなら、それ自体を相談してください。手が回らない状況なら早めに言ってもらえればアサインを見直します。

次にやってほしいこと

sururu-k は、まず shell: bash の修正 PR。そのあと配管ではなく、lean 生成の 01e を使って 02c → 03 → 04 を1クライアント分だけ完走させて、出てきた findings をこの issue に貼ってください。件数と中身の質を見て、②の設計を決めます。

0xfab0131 は、gasper の次に形式化する spec の候補を挙げてください。作業は speca-lean4-plugin の lean/ に入れてください。旧リポジトリの PR #5 の扱いも決めてもらえると助かります。

②をどう作るか（Lean の出力を 01e の完成品ではなく LLM への入力コンテキストとして扱う案を考えています）については、私の案に異論があれば聞かせてください。今週中にここで決めたいです。