Neuron

Neuro-Symbolic Logic Server for coding agents - An MCP (Model Context Protocol) server providing formal verification tools and a truth database. Uses beads, Soufflé, Z3, and MCPs to give first-order logic powers to your thinking agents.

Features

Neuron provides a set of MCP tools that enable coding agents to:

• Formal Verification: Execute Z3 theorem prover scripts to prove code equivalence, detect contradictions, and verify logical properties
• Truth Database: Store and query proven facts with proof metadata
• Datalog Analysis: Run Soufflé Datalog analyses for static analysis and logical reasoning
• Agent Orchestration: Dispatch and manage async subagents for parallel work
• Hot-Reload: Development-friendly proxy mode with hot-reload capabilities

Installation

Prerequisites

1. Python 3.10+
2. Beads (bd CLI) - Issue tracking system for coding agents:
   • Install from GitHub releases
   • Or build from source: go install github.com/steveyegge/beads/cmd/bd@latest
   • Verify installation: bd version
   • See Beads documentation for complete setup
3. Soufflé Datalog Engine (system binary, required for analyze_datalog tool):
   • macOS: brew install souffle
   • Debian/Ubuntu: apt-get install souffle
   • See Soufflé installation guide for other platforms
4. Claude Code (for MCP integration)

Install Neuron

# Clone the repository
git clone <repository-url>
cd neuron

# Install in development mode
pip install -e .

# Or install from source
pip install .

Install as MCP Server

Neuron can be registered as an MCP server for Claude Code:

# Direct mode (standard installation)
python src/neuron.py install

# Hot-reload proxy mode (recommended for development)
python src/neuron.py install --proxy

The installation process will:

• Register neuron as an MCP server with Claude Code
• Bootstrap agent definition files in .claude/agents/
• Set up the truth database at .claude/truth.db
• Configure agent coordination database at .claude/agents.db

Usage

MCP Tools

Once installed, Neuron provides the following MCP tools:

truth_add(subject, predicate, object, proof)

Record a proven fact into the Truth DB. Use this only when a verifier (Z3/Datalog) has proven a hypothesis.

truth_query(subject=None, predicate=None)

Query the Truth DB for existing proven facts. Use this before assuming capabilities or behavior about the codebase.

verify_z3(python_script)

Execute a Z3 proof script in an isolated process. The script must print 'PROVEN' or 'COUNTEREXAMPLE' to stdout. The environment already has from z3 import *.

Example:

verify_z3("""
x = BitVec('x', 32)
y = BitVec('y', 32)
solver = Solver()
solver.add(x + y == y + x)  # Commutativity
if solver.check() == sat:
    print("PROVEN")
else:
    print("COUNTEREXAMPLE")
""")

analyze_datalog(datalog_code, facts_dir=".")

Run a Soufflé Datalog analysis. Writes code to a temporary file and executes against the specified fact directory.

Example:

analyze_datalog("""
.decl edge(x: symbol, y: symbol)
.decl reachable(x: symbol, y: symbol)

edge("a", "b").
edge("b", "c").

reachable(x, y) :- edge(x, y).
reachable(x, z) :- edge(x, y), reachable(y, z).
""")

dispatch_agent(agent_name, bead_id, instructions)

Launch an async subagent. Non-blocking, returns immediately with PID. Check status via agent_status_check().

Available agents:

• analyst - Static analysis using Datalog
• implementer - Code execution and test running
• log-analyst - Log file analysis
• logician - Datalog-based logical verification
• performance-optimizer - Profiling and optimization
• researcher - Codebase exploration and documentation
• test-specialist - Test creation and coverage
• verifier - Z3 equivalence proofs

agent_status_check(bead_id=None)

Check the status of async agent tasks. Auto-detects completion via process state. If bead_id is None, returns all active agents.

agent_status_update(bead_id, status, message="")

Update the status of an async agent task. Called by subagents to report progress. Status values: pending, started, running, completed, failed.

reload_server()

Hot-reload the MCP server backend (requires proxy mode). Sends SIGHUP to the proxy process, which restarts the backend while maintaining the connection to Claude Code.

Command Line Interface

Neuron provides several CLI commands:

# Run the MCP server directly (called by Claude Code)
python src/neuron.py run --root-dir /path/to/project --db-path .claude/truth.db

# Run via hot-reload proxy
python src/neuron.py proxy --root-dir /path/to/project --pid-file .claude/proxy.pid

# Update agent status (called by subagents)
python src/neuron.py status <bead_id> <state> [--message "..."]

# Manage agent definitions
python src/neuron.py agents --inject --update

# Sync managed sections in CLAUDE.md and agent files
python src/neuron.py sync --claude-md CLAUDE.md --agents-dir .claude/agents

Beads Integration

Neuron integrates with Beads for issue tracking and work management. Every agent task is associated with a bead_id that corresponds to a Bead issue.

Beads Workflow

Neuron uses beads for tracking work items:

# Check available work
bd ready

# Create a new bead (work item)
bd create --title="Implement feature X" --type=task

# View bead details and dependencies
bd show bd-123

# List all beads
bd list

Key Concepts:

• Every unit of work must be tracked in a Bead
• Agent tasks reference beads via bead_id parameter
• Beads provide dependency tracking and status management
• Neuron's dispatch_agent tool requires a bead_id to track work

Using Beads with Neuron

When dispatching agents, always reference a bead:

# Create a bead first
# bd create --title="Verify code equivalence" --type=task
# Returns: bd-abc123

# Dispatch agent with bead ID
dispatch_agent(
    agent_name="verifier",
    bead_id="bd-abc123",
    instructions="Verify that obfuscated_func equals clean_func"
)

The agent's progress, logs, and results are all associated with the bead ID, making it easy to track work across the project.

Agent Management

Neuron manages agent definition files in .claude/agents/ using HTML-style markers:

<!-- BEGIN NEURON:section_name -->
<!-- Generated by neuron.py @ timestamp -->
...managed content...
<!-- END NEURON:section_name -->

Available managed sections:

• completion_protocol - How async agents report completion
• project_context - Project info and architecture refs
• search_tools - Modern search tool instructions
• neuron_tools - Available MCP tools
• dispatch_usage - Async dispatch documentation
• agent_table - Agent reference table
• hub_role - Hub orchestrator role
• prime_directive - Core principles
• epistemic_protocol - Truth verification workflow
• beads_workflow - Bead management workflow
• grounding_workflow - Assumption verification
• nav_tools - Navigation tools

Commands:

# Inject markers into all agent files
python src/neuron.py agents --inject

# Update managed sections with latest content
python src/neuron.py agents --update

# Both inject and update
python src/neuron.py agents --inject --update

Hot-Reload (Proxy Mode)

When installed with --proxy, Neuron runs behind an async proxy that maintains the connection to Claude Code while allowing the backend to restart.

Trigger reload:

• Via MCP tool: reload_server()
• Via shell: kill -HUP $(cat .claude/proxy.pid)

This is especially useful during development when modifying neuron.py.

Architecture

Databases

• Truth Database (.claude/truth.db): Stores proven facts with subject-predicate-object triples and proof metadata
• Agent Database (.claude/agents.db): Tracks agent runs, status, logs, and coordination data
• Beads Database (.beads/issues.jsonl): Managed by beads (bd) CLI for issue tracking and work management

Agent Coordination

Neuron uses a SQLite-based agent coordination system:

• agent_runs: Tracks dispatched agents with status, PID, output, and timestamps
• agent_logs: Structured logging with event types, levels, and JSON data
• Status tracking: Automatic completion detection via process monitoring

Process Management

• Zombie reaping: SIGCHLD handler automatically reaps terminated child processes
• Process monitoring: Checks process state to auto-detect completion
• Output capture: Captures stdout/stderr from async agents and stores in database

Development

Setup

# Install with dev dependencies
pip install -e ".[dev]"

# Run tests
pytest

# Format code
black src/
ruff check src/

Project Structure

neuron/
├── src/
│   └── neuron.py          # Main MCP server implementation
├── tests/                 # Test suite
├── pyproject.toml         # Project configuration
└── README.md             # This file

License

See LICENSE file for details.

Author

Mahmoud Abdelkader ([email protected])