kaizen-cli 0.1.35

Distributable agent observability: real-time-tailable sessions, agile-style retros, and repo-level improvement (Cursor, Claude Code, Codex). SQLite, redact before any sync you enable.
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
81
82
83
84
85

// SPDX-License-Identifier: AGPL-3.0-or-later
//! Quint model-check of MCP edge invariants (TUI stub, sync run once vs daemon), see
//! [specs/mcp-server.qnt](specs/mcp-server.qnt).

use quint_connect::*;
use serde::Deserialize;

#[derive(Debug, Eq, PartialEq, Deserialize)]
struct McpState {
    connected: bool,
    #[serde(rename = "tuiCalls")]
    tui_calls: i64,
    #[serde(rename = "tuiUnavailable")]
    tui_unavailable: i64,
    #[serde(rename = "syncDaemonAttempts")]
    sync_daemon_attempts: i64,
    #[serde(rename = "syncDaemonRejects")]
    sync_daemon_rejects: i64,
    #[serde(rename = "syncOnceFlushes")]
    sync_once_flushes: i64,
}

#[derive(Debug, Default)]
struct McpDriver {
    connected: bool,
    tui_calls: i64,
    tui_unavailable: i64,
    sync_daemon_attempts: i64,
    sync_daemon_rejects: i64,
    sync_once_flushes: i64,
}

impl State<McpDriver> for McpState {
    fn from_driver(d: &McpDriver) -> Result<Self> {
        Ok(McpState {
            connected: d.connected,
            tui_calls: d.tui_calls,
            tui_unavailable: d.tui_unavailable,
            sync_daemon_attempts: d.sync_daemon_attempts,
            sync_daemon_rejects: d.sync_daemon_rejects,
            sync_once_flushes: d.sync_once_flushes,
        })
    }
}

impl Driver for McpDriver {
    type State = McpState;

    fn step(&mut self, step: &Step) -> Result {
        match step.action_taken.as_str() {
            "init" | "step" => {
                *self = McpDriver::default();
            }
            "client_connect" => {
                if !self.connected {
                    self.connected = true;
                }
            }
            "tui_call" => {
                if self.connected {
                    self.tui_calls += 1;
                    self.tui_unavailable += 1;
                }
            }
            "sync_run_daemon" => {
                if self.connected {
                    self.sync_daemon_attempts += 1;
                    self.sync_daemon_rejects += 1;
                }
            }
            "sync_run_once" => {
                if self.connected {
                    self.sync_once_flushes += 1;
                }
            }
            other => anyhow::bail!("unexpected mcp action: {other}"),
        }
        Ok(())
    }
}

#[quint_run(spec = "specs/mcp-server.qnt", max_samples = 10, max_steps = 8)]
fn mcp_server_run() -> impl Driver {
    McpDriver::default()
}