验证检查

压缩后，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 将每个任务分为三个维度并推荐模型层级。

路由维度

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压缩

lean-ctx 使用Thompson采样学习最优压缩阈值。

Thompson采样赌博机

三个臂（保守、平衡、激进）以不同阈值竞争。

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