nanoGentzen v2: Formal Logic Runtime for AI Agent Governance

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.

Core Architectural Principle

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).

Related MCP server: Mcp-Omega-Brain

The 8 Governance MCP Tools

Quickstart

1. Installation

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):

# 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

# 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:

# 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/ and the Framework Integration Matrix.

Example Walkthrough: Production Deployment

Prompt

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/ directory:

• System Architecture: Internal layers, Gentzen prover integration, and state machine transitions.

• MCP API Reference: Complete specifications for all 8 governance tools and JSON schemas.

• Security Model: Trust boundaries, cryptographic single-use certificates, and anti-replay mitigations.

• Self-Correction & Human Approval: Autonomous replanning vs. human approval escalation protocol.

• Model & Engine Integration: Dual-backend Gentzen proof engine and intuitionistic $LJ$ calculus rules.

• Hermes Agent Integration: 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 for guidelines on development setup, proof engine invariants, and pull request procedures.

License

MIT License. See LICENSE for details.