Verificaciones de salida

Después de la compresión, lean-ctx realiza verificaciones determinísticas para asegurar que no se perdió información crítica.

Anclaje de rutas

Extrae rutas de archivos de la salida original y verifica su preservación.

Verificación de identificadores

Detecta nombres de funciones y estructuras y verifica su preservación.

Consistencia de números de línea

Verifica que los números de línea referenciados no excedan el conteo real de líneas.

Integridad estructural

Verifica que los bloques de código tengan llaves balanceadas.

Configuración

La verificación es configurable 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 del resultado

Cuando se detectan advertencias, se agrega una línea [VERIFY] a la salida.

[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

Enrutamiento de modelos basado en intención

lean-ctx clasifica cada tarea en tres dimensiones y recomienda un nivel de modelo.

Dimensiones de enrutamiento

Salida de ctx_intent

ctx_intent ahora retorna el nivel 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

Compresión ML adaptativa

lean-ctx usa Thompson Sampling para aprender umbrales de compresión óptimos.

Bandits Thompson Sampling

Tres brazos (conservador, balanceado, agresivo) compiten con diferentes umbrales.

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

Bucle de retroalimentación

Cada resultado de compresión retroalimenta el sistema de bandits.

API del Dashboard

Acceda a las estadísticas de verificación a través de la API del dashboard.

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

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