Verificações de saída

Após a compressão, lean-ctx realiza verificações determinísticas.

Ancoragem de caminhos

Extrai caminhos de arquivo e verifica sua preservação.

Verificação de identificadores

Detecta nomes de funções e estruturas e verifica sua preservação.

Consistência de números de linha

Verifica que os números de linha referenciados não excedam a contagem real.

Integridade estrutural

Verifica que os blocos de código tenham chaves balanceadas.

Configuração

A verificação é configurável por perfil.

# 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

Formato do resultado

Quando avisos são detectados, uma linha [VERIFY] é adicionada.

[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

Roteamento de modelos baseado em intenção

lean-ctx classifica cada tarefa em três dimensões e recomenda um nível de modelo.

Dimensões de roteamento

Saída do ctx_intent

ctx_intent agora retorna o nível de modelo recomendado.

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

Compressão ML adaptativa

lean-ctx usa Thompson Sampling para aprender limiares ótimos de compressão.

Bandits Thompson Sampling

Três braços competem com diferentes limiares.

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

Loop de feedback

Cada resultado de compressão alimenta o sistema de bandits.

API do Dashboard

Acesse estatísticas de verificação via API do dashboard.

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

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