MCP-PIF-CLJS: A Self-Modifying MCP Server with Formal Reasoning

A Model Context Protocol (MCP) server written in ClojureScript that explores homoiconicity, formal reasoning, and metaprogramming to enable runtime tool creation and safe self-modification capabilities. It allows models like Claude to create and execute new tools during runtime, evaluate lambda calculus expressions, perform type inference, and prove logical theorems—all without restarting the server.

This project combines Clojure's code-as-data philosophy with formal methods, providing a unique platform for exploring self-verifying code, type-driven development, and automated reasoning within an AI-assisted environment.

🚀 Quick Start

Prerequisites

Node.js 16+
Java 11+ (for ClojureScript compiler)

Installation

Clone and build:

git clone <repository-url>
cd MCP-PIF
npm install
npx shadow-cljs compile mcp-server

Configure Claude Desktop:

Edit your Claude Desktop config file:
- macOS: ~/Library/Application Support/Claude/claude_desktop_config.json
- Windows: %APPDATA%\Claude\claude_desktop_config.json
```
{
  "mcpServers": {
    "mcp-pif-cljs": {
      "command": "node",
      "args": ["/full/path/to/MCP-PIF/out/mcp-server.js"]
    }
  }
}
```
Restart Claude Desktop

Building a .dxt Package

For easier use and distribution, you can create a .dxt package:

./package-dxt.sh

This creates mcp-pif-cljs.dxt which can be installed via drag-and-drop in Claude Desktop.

🛠️ Available Tools

Base Tools

memory-store - Store key-value pairs in memory
memory-retrieve - Retrieve stored values
journal-recent - View recent activity journal
server-info - Get comprehensive server information (all tools, state, statistics)

Meta-Programming Tools

meta-evolve - Create new tools at runtime (arithmetic, string, lambda, typed)
execute-tool - Execute any tool by name (including dynamic ones)

Formal Reasoning Tools

lambda-eval - Evaluate lambda calculus expressions with beta reduction
type-check - Perform Hindley-Milner type inference on expressions
prove - Automated theorem proving for propositional logic

💡 Example Usage

Basic Memory Storage

You: "Store my favorite programming language as ClojureScript"
Claude: I'll store that for you using the memory-store tool.

You: "What's my favorite programming language?"
Claude: Your favorite programming language is ClojureScript.

Creating Custom Tools

You: "I need a tool that calculates the area of a circle"

Claude: I'll create that tool for you using meta-evolve...
[Creates tool with code: (args) => Math.PI * args.radius * args.radius]

You: "What's the area of a circle with radius 5?"
Claude: The area is 78.54 square units.

Lambda Calculus & Formal Reasoning

You: "Evaluate the lambda expression for identity function applied to 42"
Claude: Using lambda-eval with expression: [(λ x x) 42]
Result: 42 (reduced in 1 step)

You: "What's the type of function composition?"
Claude: Using type-check on (λ f (λ g (λ x [g [f x]])))
Type: ((a → b) → ((b → c) → (a → c)))

You: "Prove that if A implies B and we have A, then B follows"
Claude: Using the prove tool with modus ponens...
Proof found! B is derived from premises A and A→B.

The Dynamic Tool Workflow

Due to MCP client caching, newly created tools must be called via execute-tool:

Create a tool:

Use meta-evolve to create "multiply":
- code: "(args) => args.x * args.y"
- tool-type: "arithmetic"

Verify creation:

Use server-info
(You'll see "multiply [RUNTIME]" in the tools list)

Execute the tool:

Use execute-tool with:
- tool-name: "multiply"
- arguments: { x: 6, y: 7 }
Result: 42

🏗️ Architecture

┌─────────────────┐     ┌──────────────────┐     ┌─────────────────┐
│   AI Client     │────▶│  MCP Protocol    │────▶│   Meta Engine   │
│   (Claude)      │     │  (stdio/jsonrpc) │     │ (Self-Modifier) │
└─────────────────┘     └──────────────────┘     └─────────────────┘
                               │                          │
                               ▼                          ▼
                        ┌──────────────────┐     ┌─────────────────┐
                        │   Tools/Memory   │     │    Journal DB   │
                        │   (Extensible)   │     │   (DataScript)  │
                        └──────────────────┘     └─────────────────┘

Project Structure

src/mcp/
├── core.cljs        # Main server & request routing
├── protocol.cljs    # JSON-RPC/MCP protocol handling
├── tools.cljs       # Tool definitions and handlers
├── meta.cljs        # Self-modification engine
├── evaluator.cljs   # Safe JavaScript evaluation
├── journal.cljs     # Activity logging (DataScript)
├── lambda.cljs      # Lambda calculus evaluator
├── types.cljs       # Hindley-Milner type inference
└── proof.cljs       # Automated theorem proving

🔒 Safety Mechanisms

Sandboxed Execution: Limited to arithmetic and string operations
Code Validation: Blocks dangerous operations (file system, network, process)
Namespace Protection: Core namespaces cannot be modified
Activity Journal: All actions are logged and auditable
Session-Only: Changes don't persist between restarts

🧪 Development

# Development build with hot reload
npx shadow-cljs watch mcp-server

# Run tests
npm test

# Create .dxt package
./package-dxt.sh

Testing the Server

# Basic protocol test
node test-clean-protocol.js

# Dynamic tools test
node test-dynamic-tools.js

# Formal reasoning test
node test-formal-reasoning.js

🎯 Philosophy

This project explores the intersection of:

Homoiconicity: Code as data, data as code
Self-Reference: A system that can reason about itself
Controlled Evolution: Safe boundaries for self-modification
Formal Methods: Type systems and proof checking for verified computation
Human-AI Collaboration: AI proposes, human uses

📋 Roadmap

Completed:

Basic MCP server in ClojureScript
Runtime tool creation
Universal tool executor (workaround for client caching)
.dxt packaging support
Lambda calculus evaluator with Church encodings
Hindley-Milner type inference system
Automated theorem proving for propositional logic

In progress:

Tool composition (tools that use other tools)
Namespace evolution
Import capabilities from other MCP servers
Persistent tool storage
Dependent type system
SMT solver integration
Self-verifying tool creation

⚠️ Important Notes

Tool Persistence: Tools only exist while server is running
Client Caching: Use execute-tool to call runtime-created tools
Real Computation: Tools execute actual code, not LLM approximations
Experimental Server: Work in progress, tools may not work as expected

🤝 Contributing

This is an experimental project exploring metaprogramming in the context of AI tools. Contributions that enhance self-modification capabilities or improve safety are welcome!

📄 License

MIT

"The significant problems we face cannot be solved at the same level of thinking we were at when we created them." - Einstein

This project asks: What if our tools could evolve their own thinking?

Model Context Protocol