发布未审计的AI工作
AI Agent会幻觉文件路径、生成损坏的导入、将密钥泄露到输出中，并产生无法追溯的更改。
ctx_verify检查每个输出中的幻觉路径、损坏的导入和密钥泄露。ctx_proof生成包含Claim级别验证和Lean4支撑的形式化保证的ContextProofV2报告。
8 工具
Lean4形式化证明
跨3个领域的82个机器验证定理：策略不变量、压缩保持性和Agent Handoff安全性——全部在Lean4中验证，零sorry。
Claim-based Verification
ContextProofV2将验证分解为原子化的Claim。每个Claim被路由到相应的验证器——从确定性检查到Lean4证明。
Quality Levels 0–4
五个保证级别：溯源（Q0）、确定性（Q1）、已测试（Q2）、策略已证明（Q3）、形式化验证（Q4）。每个输出都附带其精确的信任级别。
证明构件
包含管道指标、SLO快照和溯源链的JSON和HTML证明报告。
输出检查
路径验证、标识符检查、结构验证，支持WARN/FAIL语义。
压缩不变量
形式化证明：signatures模式保留所有exports，map模式保留imports，aggressive模式零密钥泄露。
可重放性
确定性会话，支持重放哈希、CI门控和回归检测。
Agent Handoff安全性
在Lean4中形式化验证的状态机。终端状态为汇聚态，生命周期排序为单调的，无效信封被拒绝。
查看实际效果
LeanCTX生成带证明的输出。策略不变量通过82个机器验证定理在Lean4中进行形式化验证。每个上下文决策都会生成包含管道指标和溯源链的可审计证跡。输出会检查有效路径、正确标识符和结构完整性。Claim-based Verification将证明分解为原子化的可验证单元，提供Quality Levels 0-4。
7 MCP 工具
LeanCTX生成带证明的输出。策略不变量通过82个机器验证定理在Lean4中进行形式化验证。每个上下文决策都会生成包含管道指标和溯源链的可审计证跡。输出会检查有效路径、正确标识符和结构完整性。Claim-based Verification将证明分解为原子化的可验证单元，提供Quality Levels 0-4。
ctx_verify Verification observability snapshot. Action stats returns versioned JSON or compact summary (no raw content).
ctx_proof Export a machine-readable ContextProofV1 (Verifier + SLO + Pipeline + Provenance). Writes to .lean-ctx/proofs/ by default.
ctx_artifacts Context artifact registry + BM25 index. Actions: list|status|index|reindex|search|remove.
ctx_gain Gain report (includes Wrapped via action=wrapped).
ctx_heatmap File access heatmap (local-first). Actions: status|directory|cold|json.
ctx_metrics Session token stats, cache rates, per-tool savings.
ctx_cache Cache ops: status|clear|invalidate.
每个输出都附带证明
LeanCTX为每个会话生成证明构件：读取了哪些文件、压缩了什么、哪些检查通过了、Token如何使用。这使AI工作可审计、可重放、值得信赖。