lean-ctx 3.9.1

Context Runtime for AI Agents with CCP. 71 MCP tools, 10 read modes, 95+ compression patterns, cross-session memory (CCP), persistent AI knowledge with temporal facts + contradiction detection, multi-agent context sharing, LITM-aware positioning, AAAK compact format, adaptive compression with Thompson Sampling bandits. Supports 24+ AI tools. Reduces LLM token consumption by up to 99%.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80

use rmcp::ErrorData;
use rmcp::model::Tool;
use serde_json::{Map, Value, json};

use crate::server::tool_trait::{McpTool, ToolContext, ToolOutput, get_str};
use crate::tool_defs::tool_def;

pub struct CtxVerifyTool;

impl McpTool for CtxVerifyTool {
    fn name(&self) -> &'static str {
        "ctx_verify"
    }

    fn tool_def(&self) -> Tool {
        tool_def(
            "ctx_verify",
            "Verification observability — tool call statistics and claim-based verification.\n\
             WORKFLOW: action=stats to monitor tool usage; action=proof|v2 for Lean4 proof verification.\n\
             Actions: stats|proof|v2 (format=summary|json|both, default summary).\n\
             ANTIPATTERN: not for runtime verification during active development — use for periodic audit.",
            json!({
                "type": "object",
                "properties": {
                    "action": {
                        "type": "string",
                        "enum": ["stats", "proof", "v2"],
                        "description": "stats|proof|v2"
                    },
                    "format": {
                        "type": "string",
                        "enum": ["summary", "json", "both"],
                        "description": "Output format: summary|json|both (default summary)"
                    }
                }
            }),
        )
    }

    fn handle(
        &self,
        args: &Map<String, Value>,
        _ctx: &ToolContext,
    ) -> Result<ToolOutput, ErrorData> {
        let action = get_str(args, "action").unwrap_or_else(|| "stats".to_string());
        let format = get_str(args, "format");
        match action.as_str() {
            "stats" => {
                let out = crate::tools::ctx_verify::handle_stats(format.as_deref())
                    .map_err(|e| ErrorData::invalid_params(e, None))?;
                Ok(ToolOutput {
                    text: out,
                    original_tokens: 0,
                    saved_tokens: 0,
                    mode: Some(action),
                    path: None,
                    changed: false,
                    shell_outcome: None,
                })
            }
            "proof" | "v2" => {
                let out = crate::tools::ctx_verify::handle_proof(format.as_deref())
                    .map_err(|e| ErrorData::invalid_params(e, None))?;
                Ok(ToolOutput {
                    text: out,
                    original_tokens: 0,
                    saved_tokens: 0,
                    mode: Some(action),
                    path: None,
                    changed: false,
                    shell_outcome: None,
                })
            }
            _ => Err(ErrorData::invalid_params(
                "unsupported action (expected: stats, proof, v2)",
                None,
            )),
        }
    }
}