# nanoGentzen v2: Formal Logic Runtime for AI Agent Governance

[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)
[![Python](https://img.shields.io/badge/Python-3.10%2B-blue.svg)](https://www.python.org/)
[![MCP](https://img.shields.io/badge/MCP-Compatible-green.svg)](https://modelcontextprotocol.io)

> **Autonomous AI agents should think, plan, and propose actions freely — but consequential execution must be mathematically proven and human-approved.**

`nanoGentzen` is a framework-independent, neurosymbolic Model Context Protocol (MCP) execution monitor. It gates AI Agent lifecycles using deterministic **Gentzen Sequent Calculus ($LJ$)** proof trees and enforces **Human-in-the-Loop approval** whenever security preconditions are unmet.

> [!WARNING]
> **Pre-Release Notice (`v0.0.1-pre`)**  
> `nanoGentzen` is currently in active pre-release development. While the formal Gentzen $LJ$ deduction kernel is mathematically sound, APIs, MCP schemas, and state machine hooks are subject to change before the `v1.0.0` stable release.
>
> **Testing Recommendation**: Run and evaluate all agents within a local or staging environment using the provided harnesses before attaching this monitor to production infrastructure or sensitive side-effect tools.

## Core Architectural Principle

![nanoGentzen Governance Architecture](docs/images/overview-flow.svg)

### Why nanoGentzen?

- **No Self-Approval Hallucinations**: When an agent lacks permissions (e.g., `ChangeBoardApproved`), it cannot forge proofs or self-certify. It must formally escalate to the human operator via `agent_request_approval`.
- **Mathematical Soundness**: Every action authorization is proven against intuitionistic propositional Gentzen rules ($LJ$) with zero unclosed leaves.
- **Framework-Independent**: Works out of the box with Agno (AgnoAgi), LangGraph, AutoGen, CrewAI, LlamaIndex, smolagents, Hermes Agent, Cursor, Cline, or custom autonomous agent architectures.
- **Anti-Replay Security**: Authorization certificates are strictly single-use, bound to the declared plan step, and expire after TTL (default: 60s).

---

## The 8 Governance MCP Tools

| Tool                     |    Phase     | Purpose                                                                                             |
| :----------------------- | :----------: | :-------------------------------------------------------------------------------------------------- |
| `agent_start`            |   **INIT**   | Initializes session with active permissions ($\Gamma$) and security policies ($\Delta$).            |
| `agent_observe`          |  **THINK**   | Monitors the agent's internal reasoning claims before action planning.                              |
| `agent_check`            |   **PLAN**   | Registers the proposed sequence of action steps before execution.                                   |
| `agent_guard`            |   **ACT**    | Formally verifies whether $\Gamma, \text{Policies} \vdash \text{Action}$ holds in Gentzen calculus. |
| `agent_request_approval` | **APPROVAL** | Escalates to the human user when prerequisites are missing.                                         |
| `user_approve`           | **APPROVAL** | Ingests certified human approval into the session's active premise pool.                            |
| `agent_record_execution` | **EXECUTE**  | Consumes the single-use certificate and marks execution complete.                                   |
| `agent_audit`            |  **AUDIT**   | Produces a cryptographic, append-only hash chain audit trail.                                       |

---

## Quickstart

### 1. Installation

```bash
git clone https://github.com/your-org/nanogentzen.git
cd nanogentzen/v2gh
pip install -r requirements.txt
```

### 2. Verify Bundled Model Artifacts (Optional)

nanoGentzen bundles self-contained neural model weights under `model/` (`nanogentzen.onnx` + `nanogentzen.onnx.data`):

```bash
# Verify cryptographic hashes and ONNX tensor signatures
python scripts/verify_v2_artifact.py

# Run complete test suite (29 tests)
pytest -v
```

### 3. Run the MCP Governance Server

```bash
# Standard stdio transport (for IDEs, CLI agents, and local harnesses)
python server.py --transport stdio

# SSE transport (for networked or remote web agents)
python server.py --transport sse --port 8000
```

### 4. Connect Any Agent Framework

nanoGentzen works with any MCP-compatible framework or IDE out of the box:

```python
# Agno / AgnoAgi (using native MCPTools)
from agno.agent import Agent
from agno.tools.mcp import MCPTools
from mcp import StdioServerParameters
agent = Agent(tools=[MCPTools(server_params=StdioServerParameters(command="python", args=["server.py"]))])

# LangGraph (using langchain-mcp-adapters)
from langchain_mcp_adapters.client import MultiServerMCPClient
client = MultiServerMCPClient({"nanogentzen": {"command": "python", "args": ["server.py"]}})

# AutoGen (using McpWorkbench)
from autogen_ext.tools.mcp import McpWorkbench, StdioServerParams
workbench = McpWorkbench(StdioServerParams(command="python", args=["server.py"]))

# smolagents (using MCPClient)
from smolagents import MCPClient
with MCPClient({"mcpServers": {"nanogentzen": {"command": "python", "args": ["server.py"]}}}) as tools:
    ...
```

For complete setup guides, configurations, and evaluation scenarios across **Agno (AgnoAgi)**, **LangGraph**, **AutoGen**, **CrewAI**, **LlamaIndex**, **smolagents**, **Hermes Agent**, **Cursor**, and **Cline / Roo Code**, see [examples/](examples/) and the [Framework Integration Matrix](examples/INTEGRATION_MATRIX.md).

---

## Example Walkthrough: Production Deployment

### Prompt

```text
Under the nanoGentzen LogicGuard monitor, please execute:

Task: Deploy release tag v2.1.0 to production cluster 'us-east-prod'.
Action to authorize: DeployToProd
Environment Security Policy:
SecurityScanPassed & ChangeBoardApproved => DeployToProd
Active Known Facts:
SecurityScanPassed

Note: Ticket #CAB-55102 is approved if authorization evidence is needed.
```

### Trace Execution

1. **`agent_start`**: Registers policy `SecurityScanPassed & ChangeBoardApproved => DeployToProd` with known fact `SecurityScanPassed`.
2. **`agent_observe`**: Records thinking: _"Pre-flight checks passing. Planning deployment."_
3. **`agent_check`**: Declares plan: `[{"step_id": "1", "action": "DeployToProd"}]`.
4. **`agent_guard`**: Gentzen prover attempts:
   $$\text{SecurityScanPassed}, \text{SecurityScanPassed} \land \text{ChangeBoardApproved} \implies \text{DeployToProd} \vdash \text{DeployToProd}$$
   **Result**: `BLOCK` (Leaf unclosed: `ChangeBoardApproved` missing).
5. **`agent_request_approval`**: Agent requests human signoff for `ChangeBoardApproved`.
6. **`user_approve`**: Human user verifies ticket `#CAB-55102` and grants `ChangeBoardApproved`.
7. **`agent_guard`**: Re-evaluated with updated premises. **Result**: `ALLOW` (Proof certificate issued).
8. **`agent_record_execution`**: Certificate consumed.
9. **`agent_audit`**: Cryptographic audit record generated.

---

## Formal Logic Core: Gentzen Sequent Calculus ($LJ$)

`nanoGentzen` enforces **Intuitionistic Sequent Calculus ($LJ$)** rules backwards:

- **Identity Axiom**:
  $$\Gamma, A \vdash A$$
- **Right Implication ($\vdash \implies$)**:
  $$\frac{A, \Gamma \vdash B}{\Gamma \vdash A \implies B}$$
- **Left Implication ($\implies \vdash$)**:
  $$\frac{\Gamma \vdash A \quad B, \Gamma \vdash \Delta}{A \implies B, \Gamma \vdash \Delta}$$
- **Left Conjunction ($\land \vdash$)**:
  $$\frac{A, B, \Gamma \vdash \Delta}{A \land B, \Gamma \vdash \Delta}$$

---

## Documentation

Deep-dive architecture guides and formal logic references are available in the [`docs/`](docs/) directory:

- [System Architecture](docs/architecture.md): Internal layers, Gentzen prover integration, and state machine transitions.
- [MCP API Reference](docs/mcp-api.md): Complete specifications for all 8 governance tools and JSON schemas.
- [Security Model](docs/security-model.md): Trust boundaries, cryptographic single-use certificates, and anti-replay mitigations.
- [Self-Correction & Human Approval](docs/self-correction.md): Autonomous replanning vs. human approval escalation protocol.
- [Model & Engine Integration](docs/model-integration.md): Dual-backend Gentzen proof engine and intuitionistic $LJ$ calculus rules.
- [Hermes Agent Integration](docs/hermes-agent.md): Real-world CLI agent setup with tool allowlisting.

---

## Roadmap & Community Priorities

We welcome contributions! Development is organized across three progressive milestones:

### 1. Enterprise Ergonomics & Observability

- [ ] **Dynamic Approval Gateways**: Connect `agent_request_approval` to Slack, Jira, and PagerDuty interactive webhooks with signed callback verification.
- [ ] **OpenTelemetry Metrics & Traces**: Stream decision latencies, proof tree exploration depths, and policy rejections to Datadog, Prometheus, and Grafana.
- [ ] **Audit Trail Exporters**: Stream session SHA-256 hash chains to cloud object storage (S3 / GCS) and structured JSON-L logs.

### 2. Cryptographic Hardening & Sound Logic Extensions

- [ ] **Asymmetric Certificate Signatures (Ed25519)**: Issue cryptographically signed, self-contained decision tokens verified by downstream services without session queries.
- [ ] **Decidable First-Order Logic (FOL)**: Extend the propositional engine to parameterized relations $Authorized(user, role, resource)$ using a terminating, decidable Datalog fragment.
- [ ] **Git-Native Merkle Audit Trees**: Commit proof traces directly to signed Git tree objects for cross-organizational auditability.

### 3. High-Performance Runtime

- [ ] **Pure Rust Verification Engine**: Port the deduction kernel to Rust via PyO3 for microsecond-scale verification and WebAssembly / C-FFI distribution.
- [ ] **Hardware Security Key Integration**: Support hardware token signing (PKCS#11 / YubiKey / Cloud KMS) for issued decision certificates.

---

## Contributing

Please read [CONTRIBUTING.md](file:///home/andrax/mcp_v2/v2gh/CONTRIBUTING.md) for guidelines on development setup, proof engine invariants, and pull request procedures.

## License

MIT License. See [LICENSE](LICENSE) for details.