安全与
可靠性
lean-ctx 专为生产环境设计。所有压缩均在本地运行，错误优雅降级，您的代码永远不会离开您的设备。
为生产环境 而设计
每一个架构决策都以安全为先。lean-ctx 在本地处理一切，遇到错误时优雅降级，未经明确许可绝不修改您的文件。
100% 本地处理
所有压缩、缓存和分析均在您的设备上运行。lean-ctx 是一个本地 MCP 服务器--您的代码永远不会接触外部服务器。
优雅降级
如果 lean-ctx 遇到错误，它会将原始内容原样传递。您的工作流程永远不会因 lean-ctx 故障而中断。
默认只读
lean-ctx 仅读取文件进行压缩。唯一的写入操作是 ctx_edit，需要用户显式调用。
每一层都有 安全防护
从路径遍历防护到沙箱执行，lean-ctx 实现了多重安全边界来保护您的代码库。
$ 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
路径遍历防护
所有文件路径都通过安全检查点验证。项目根目录之外的请求会被拒绝。
沙箱执行
Shell 命令在可配置的超时和资源限制下运行。没有 eval() 或动态代码执行。
无网络除非选择加入
唯一的网络功能是可选的每日版本检查（默认禁用）。无遥测，无回传。
经过测试且 已验证
每个版本都经过全面的测试套件、严格的静态分析和跨平台 CI 验证 - 绝不走捷径。
1,400+ 项自动化测试
每个版本都通过 1,400+ 项单元测试和集成测试，覆盖压缩、缓存、安全防护和边界情况。
Clippy Pedantic
使用 Rust 最严格的 Linter 实现零警告。Pedantic 模式可捕获细微 bug、性能问题和 API 设计缺陷。
全面的 CI
GitHub Actions 在 Linux、macOS 和 Windows 上运行测试。cargo-deny 审计依赖项的漏洞和许可证合规性。
什么都不会损坏。lean-ctx 将原始内容原样传递。您的工作流程永远不会被阻断 - AI 只是接收到未压缩的上下文。
完全 开源
每一行代码都可公开审计。无混淆、无二进制文件、默认无遥测。
$ 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
完全开源
每一行代码都可在 GitHub 上公开审查。没有混淆、没有二进制 blob、没有闭源组件。
默认零遥测
lean-ctx 默认不收集任何数据。可选的匿名统计需要明确选择加入，且不包含任何代码或文件名。
输出 验证
每个压缩输出都会自动验证其完整性。
ctx_read src/auth.rs ✓ VERIFY PASS ├─ Paths checked: 12/12 preserved ├─ Identifiers: 8/8 preserved ├─ Structure: balanced └─ Info loss score: 0.0%
路径锚定
验证源文件路径在压缩输出中的保留。
标识符检查
函数名和结构体名在压缩过程中被跟踪。
结构完整性
验证括号平衡以检测截断的代码块。
数学上 已证明
策略不变量、压缩属性和代理交接安全性均已在Lean4中进行形式化验证 — 这与Amazon Cedar和Mathlib使用的是同一个证明助手。82个机器检验定理，零个未证明引理。
$ 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)
策略不变量
PathJail逃逸防护、作用域隔离、预算执行和上下文治理规则 — 全部在Lean4中证明正确。
压缩保持性
Signatures模式保留所有export，Map模式保留import，Aggressive模式保证零密钥泄露 — 数学证明。
交接安全性
代理交接状态机已形式化验证：终端状态为汇点，生命周期排序单调，无效信封被拒绝。