Defense in Depth

Safety &
Reliability

lean-ctx is designed for production use. All compression runs locally, errors degrade gracefully, and your code never leaves your machine.

Architecture

Built for Production

Every architectural decision prioritizes safety. lean-ctx processes everything locally, degrades gracefully on errors, and never modifies your files without explicit permission.

100% Local processing - your code never leaves your machine
0 Network calls by default - fully offline capable
13 tok Re-read cost - cached files cost almost nothing

100% Local Processing

All compression, caching, and analysis runs on your machine. lean-ctx is a local MCP server - your code never touches external servers.

Graceful Degradation

If lean-ctx encounters an error, it passes the original content through unchanged. Your workflow is never blocked by a lean-ctx failure.

Read-Only by Default

lean-ctx only reads files for compression. The only write operation is ctx_edit, which requires explicit user invocation.

Security

Defense at Every Layer

From path traversal protection to sandboxed execution, lean-ctx implements multiple security boundaries to protect your codebase.

path traversal protection 
$ ctx_read("../../etc/passwd")

ERROR: Path traversal blocked
  ├─ Requested: ../../etc/passwd
  ├─ Resolved:  /etc/passwd
  └─ Allowed:   /home/user/project/**

$ ctx_read("src/main.rs")

✓ Reading src/main.rs (mode: auto)
  → 42 lines, 1.2 KB → compressed to 18 tokens

Path Traversal Protection

All file paths are validated through a security chokepoint. Requests outside the project root are rejected.

Sandboxed Execution

Shell commands run with configurable timeouts and resource limits. No eval() or dynamic code execution.

No Network Without Opt-In

The only network feature is an optional daily version check (disabled by default). No telemetry, no phone-home.

Security configuration docs
Quality

Tested & Verified

Every release is validated by a comprehensive test suite, strict static analysis, and cross-platform CI - no shortcuts.

1,400+ Automated tests covering every module
0 Clippy warnings - pedantic mode enforced
3 Platforms tested - Linux, macOS, Windows

1,400+ Automated Tests

Every release passes 1,400+ unit and integration tests covering compression, caching, security guards, and edge cases.

Clippy Pedantic

Zero warnings with Rust's strictest linter. Pedantic mode catches subtle bugs, performance issues, and API design problems.

Comprehensive CI

GitHub Actions runs tests on Linux, macOS, and Windows. cargo-deny audits dependencies for vulnerabilities and license compliance.

What Happens When lean-ctx Fails?

Nothing breaks. lean-ctx passes the original content through unchanged. Your workflow is never blocked - the AI simply receives uncompressed context instead.

Transparency

Fully Open Source

Every line of code is publicly auditable. No obfuscation, no binary blobs, no telemetry by default.

lean-ctx version & stats 
$ lean-ctx --version

lean-ctx 3.4.3
  ├─ License:         Apache-2.0
  ├─ Source:          github.com/yvgude/lean-ctx
  ├─ Network calls:   0 (default)
  ├─ Telemetry:       disabled
  └─ Data collection: none

Fully Open Source

Every line of code is publicly auditable on GitHub. No obfuscation, no binary blobs, no closed-source components.

Zero Default Telemetry

lean-ctx collects nothing by default. Optional anonymous statistics require explicit opt-in and contain no code or file names.

View on GitHub
Quality Guardrail

Output Verification

Every compressed output is automatically verified for integrity. Path references, code identifiers, and structural balance are checked - ensuring nothing critical is lost in compression.

verification pipeline 
ctx_read src/auth.rs

✓ VERIFY PASS
  ├─ Paths checked:       12/12 preserved
  ├─ Identifiers:         8/8 preserved
  ├─ Structure:           balanced
  └─ Info loss score:     0.0%

Path Anchoring

File paths from the source are verified to be preserved in the compressed output.

Identifier Check

Function names, struct names, and code identifiers are tracked across compression.

Structural Integrity

Brace and parenthesis balance is verified to detect truncated code blocks.

Learn more about Output Verification
Formal Verification

Mathematically Proven

Policy invariants, compression properties, and agent handoff safety are formally verified in Lean4 — the same proof assistant used by Amazon Cedar and Mathlib. 82 machine-checked theorems with zero unproven lemmas.

82 Machine-checked theorems across policy, compression, and handoff domains
Q0–Q4 Quality Levels — from provenance tracking to formal verification
0 Unproven lemmas (sorry) — every theorem is fully machine-checked
lean4 formal verification 
$ lake build

Build completed successfully.
  82 theorems verified
  0 sorry (unproven lemmas)
  0 warnings

$ ctx_proof --format v2

ContextProofV2 · 8 claims extracted
  ├─ PathJail:       proved (Lean4) · Q4
  ├─ Budget:         proved (Lean4) · Q4
  ├─ Scope:          proved (Lean4) · Q4
  ├─ TerseQuality:   proved (Lean4) · Q4
  ├─ TerseEngine:    proved (Lean4) · Q4
  ├─ Compression:    preserved       · Q3
  ├─ Secrets:        passed           · Q2
  └─ Quality Level:  4 (Formally Verified)

Policy Invariants

PathJail escape prevention, scope isolation, budget enforcement, and context governance rules — all proven correct in Lean4.

Compression Preservation

Signatures mode preserves all exports, map mode preserves imports, aggressive mode guarantees zero secret leakage — mathematically proven.

Handoff Safety

Agent handoff state machine formally verified: terminal states are sinks, lifecycle ordering is monotonic, invalid envelopes are rejected.

Explore Lean4 Verification
Get Started

Ready to Try It?

Install lean-ctx in under a minute and see how it protects your workflow while dramatically reducing token usage.

Get Started Compare Alternatives