Проверки вывода

После сжатия 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-сжатие

Используется сэмплирование Томпсона для обучения оптимальным порогам сжатия.

Бандиты Томпсона

Три руки (консервативная, сбалансированная, агрессивная) с разными порогами.

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