検証チェック

圧縮後、lean-ctxは決定論的チェックを実行し、重要な情報が失われていないことを確認します。

パスアンカリング

ファイルパスを抽出し、圧縮版での保持を検証します。

識別子チェック

関数名や構造体名を検出し、保持を検証します。

行番号の一貫性

参照される行番号がソースファイルの実際の行数を超えていないか検証します。

構造的整合性

コードブロックの括弧のバランスを確認します。

設定

検証はプロファイルごとに設定可能です。

# Profile-specific verification settings
[verification]
enabled = true
# Optional explicit mode (recommended for clarity):
#   "warn" (default) -> FAIL only on High severity warnings
#   "fail"           -> FAIL on Medium+High warnings (strict)
mode = "warn"
check_paths = true
check_identifiers = true
check_line_numbers = false  # opt-in
check_structure = true

# Legacy alias (still supported):
# strict_mode = true

結果フォーマット

警告が検出されると、[VERIFY]行が出力に追加されます。

[VERIFY] WARN(mangled_identifier=2, missing_path=1) loss=15.0%
[VERIFY] FAIL(brace_mismatch=1, missing_path=1) loss=40.0%

Proof artifacts (ContextProofV2)

82 Lean4 theorems back the proof system, covering policy invariants (PathJail, Budget, Scope), compression safety, and the terse engine (TerseQuality, TerseEngine).

# MCP
ctx_proof action="export" format="summary"

# CLI
lean-ctx proof --summary

Verification observability (versioned stats)

# MCP
ctx_verify action="stats" format="json"

# CLI
lean-ctx verify --json

意図ベースのモデルルーティング

lean-ctxは各タスクを3つの次元に分類し、モデルティアを推奨します。

ルーティング次元

ctx_intent出力

ctx_intentは推奨モデルティアを返すようになりました。

INTENT_OK id=42 type=fix_bug source=heuristic conf=90% subj=file(auth.rs)
| route: dimension=how model_tier=standard reason=fix_bug(how) + complexity -> standard

適応ML圧縮

Thompson Samplingを使用して最適な圧縮しきい値を学習します。

Thompsonサンプリングバンディット

3つのアーム（保守、バランス、積極）が異なるしきい値で競合します。

Threshold Bandits (Thompson Sampling):
  rs_feedback (pulls: 120):
    conservative: α=15.2 β=8.1 mean=65% entropy=1.20 jaccard=0.80
    balanced:     α=22.3 β=5.2 mean=81% entropy=0.90 jaccard=0.70
    aggressive:   α=8.4 β=12.0 mean=41% entropy=0.60 jaccard=0.55

フィードバックループ

各圧縮結果がバンディットシステムにフィードバックされます。

ダッシュボードAPI

ダッシュボードAPIで検証統計にアクセスします。

# Verification stats
curl http://localhost:3179/api/verification

# Prometheus metrics (includes verification counters)
curl http://localhost:3179/metrics | grep verification