Verification Checks

After compression, lean-ctx performs deterministic checks to ensure no critical information was lost. Four types of checks run automatically.

Path Anchoring

Extracts file paths from the original output and verifies they are preserved in the compressed version. Missing paths indicate potential context loss.

Identifier Check

Detects function names, struct names, and other code identifiers in the source and checks their preservation. Identifiers >= 8 characters missing are flagged as high severity.

Line Number Consistency

When line numbers are referenced in the output, verifies they don't exceed the source file's actual line count. Opt-in check for precision-critical workflows.

Structural Integrity

Checks that code blocks have balanced braces and parentheses. A mismatch greater than 2 indicates truncated or malformed output.

Configuration

Verification is configurable per profile. Enable or disable individual check types based on your use case.

# 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

Result Format

When warnings are detected, a [VERIFY] line is appended to the tool output showing the warning types and information loss score.

[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

Intent-based Model Routing

lean-ctx classifies each task into three dimensions (What, How, Do) and recommends a model tier. This is a recommendation, not enforcement - the agent decides.

Routing Dimensions

ctx_intent Output

The ctx_intent tool now returns the recommended model tier alongside the intent classification.

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

Adaptive ML Compression

lean-ctx uses Thompson Sampling to learn optimal compression thresholds per language and file type. The system adapts automatically based on task outcomes.

Thompson Sampling Bandits

Three bandit arms (conservative, balanced, aggressive) compete. Each arm represents different entropy and Jaccard thresholds. The system explores early and exploits the best-performing arm over time.

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

Feedback Loop

Every compression outcome feeds back into the bandit system. Successful completions with high compression ratios reward the active arm. Periodic decay prevents stale data from dominating.

Dashboard API

Access verification statistics and Prometheus metrics via the dashboard API.

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

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