<div align="center">

<img src="docs/images/nsforge-hero.svg" alt="NSForge — Neurosymbolic Forge" width="820">

🔥 Neurosymbolic Forge (NSForge)

*Turn concepts into verifiable, traceable formulas. NSForge is an [MCP](https://modelcontextprotocol.io/) server that forges* new formulas through deterministic, provenance-tracked derivation — the AI orchestrates, tools reify.

🌐 English | 繁體中文

</div>

💡 Why NSForge?

LLMs are great at understanding and planning, but doing symbolic math by hand makes them hallucinate, contradict themselves, and produce unverifiable results. NSForge draws a clean line:

North star: every symbol, equation, value, and line of code in a result has a tool call as its birth certificate. The amount the AI computes by hand approaches zero.

NSForge is NOT a formula database — it's a derivation factory. Formulas are inputs (from SymPy‑MCP, Wikidata, BioModels, you); the operators (compose · substitute · solve · verify · prove) are the product.

🪜 The Reification Ladder

The core idea: climb from a fuzzy concept to executable, provenance-bound code, one deterministic rung at a time.

<div align="center"> <img src="docs/images/reification-ladder.svg" alt="The reification ladder: concept → symbol → derivation → algorithm, each rung recorded in a provenance ledger" width="760"> </div>

flowchart LR
    C["💭 CONCEPT<br/>a goal"] --> S["🔤 SYMBOL<br/>typed + units"]
    S --> D["🧩 DERIVATION<br/>composed"]
    D --> V{"✅ verify"}
    V -->|"fails"| D
    V -->|"passes"| A["⚙️ ALGORITHM<br/>code"]
    A -. "emitted only if ledger complete" .-> L[["📒 provenance ledger"]]
    C -.-> L
    S -.-> L
    D -.-> L

📖 Deep dive: Reification-ladder direction · General-formula-exploration roadmap

🌍 Ecosystem: don't reinvent the wheel

NSForge works with other MCP servers, not against them.

flowchart TB
    subgraph SY["🔢 sympy-mcp · 32 tools"]
        direction LR
        SY1["Base formulas: F=ma, PV=nRT, Arrhenius"]
        SY2["Constants · ODE / PDE / matrices"]
    end
    subgraph NS["🔨 nsforge-mcp · 91 tools — YOU ARE HERE"]
        direction LR
        NS1["Derivation framework<br/>compose · verify · code"]
        NS2["Provenance repository"]
        NS3["Formula search<br/>Wikidata · BioModels · SciPy"]
    end
    subgraph US["🎯 usolver-mcp · optional"]
        US1["Z3 · OR-Tools · CVXPY · HiGHS"]
    end
    SY -->|"base formulas"| NS
    NS -->|"prepared model"| US
    NS -->|"stores CREATED formulas"| REPO[("formulas/derivations")]

📦 Installation

Requirements: Python 3.12+ and uv (recommended).

uv add nsforge-mcp          # or: pip install nsforge-mcp

<details> <summary>From source</summary>

git clone https://github.com/u9401066/nsforge-mcp.git
cd nsforge-mcp
uv sync --all-extras
uv run python -c "import nsforge; print(nsforge.__version__)"

</details>

Configure as an MCP server

{
  "mcpServers": {
    "nsforge": { "command": "uvx", "args": ["nsforge-mcp"] }
  }
}

MCP 2.1 contract and tool profiles

NSForge 0.4.0 exactly pins the stable MCP Python SDK 2.1.1 and protocol revision 2026-07-28. The 91-tool catalog and legacy response dictionaries remain compatible. A fixed startup profile keeps discovery focused without deleting a capability:

Profiles are frozen when the server starts; an unknown value fails closed. Compact profiles reject unknown fields and enforce declared enum and numeric constraints. Their concise descriptions come from the central ToolSpec registry, which also drives runtime metadata and the capability manifest. The machine-readable manifest is schema v4.

MCP 2 clients also receive:

• explicit structured_output=True while preserving the existing

structuredContent + text dual channel;

• protocol isError on application failures without changing the legacy body;
• a title, icon, behavioral annotations, and namespaced _meta on every tool;
• nsforge://manifest, nsforge://health, nsforge://north-star, the

nsforge://derivations/{result_id} compatibility resource, and immutable nsforge://runs/{run_id}, nsforge://runs/{run_id}/events, detached nsforge://sessions/{session_id}, and nsforge://artifacts/{sha256} resource templates;

• phase-event-driven progress, ResourceLink blocks for completed runs and

verification-bound artifacts, resource-updated notifications, and OpenTelemetry tool/session/run correlation.

The compact workflow uses an allowlisted no-eval expression parser. Strict task runs atomically persist immutable tenant-scoped runs, ordered phase events, provenance nodes, verification evidence, and content-addressed artifacts through a SQLite Unit of Work. Verification failure, missing or stale evidence, caller assertion, wrong tenant/subject digest, or incomplete provenance blocks artifact code generation.

Relevant process settings are NSFORGE_TENANT_ID (default local), NSFORGE_RUN_DB (default data/nsforge-strict.sqlite3), and NSFORGE_ARTIFACT_ROOT (default ./artifacts). Tenant IDs are opaque slugs; output paths must resolve inside the artifact root.

stdio remains the default. To opt in to a loopback Streamable HTTP endpoint:

NSFORGE_MCP_TRANSPORT=streamable-http \
NSFORGE_MCP_HOST=127.0.0.1 \
NSFORGE_MCP_PORT=8000 \
NSFORGE_MCP_PATH=/mcp \
uv run nsforge-mcp

Every HTTP bind enables MCP 2.1 Host/Origin validation against DNS rebinding. A non-loopback bind additionally requires an explicit acknowledgement and Host allowlist, for example:

NSFORGE_MCP_TRANSPORT=streamable-http \
NSFORGE_MCP_HOST=0.0.0.0 \
NSFORGE_MCP_ALLOW_REMOTE=1 \
NSFORGE_MCP_ALLOWED_HOSTS=mcp.example.com,mcp.example.com:* \
uv run nsforge-mcp

Browser clients must also set an exact NSFORGE_MCP_ALLOWED_ORIGINS list. An empty Origin allowlist accepts non-browser requests with no Origin header and rejects every supplied Origin. These checks are not authentication: put remote HTTP behind real authentication, authorization, and TLS. NSFORGE_TENANT_ID scopes strict run/resource lookups, but it is process configuration rather than caller authentication. Without a trusted IdP or principal resolver, one server instance remains one tenant trust boundary. Legacy sessions and saved results still use process globals plus JSON/YAML compatibility storage, so pass an explicit session_id to every stateful legacy call. Neither compatibility state nor the strict SQLite store is shared across replicas; horizontal scaling requires shared state, artifact storage, and distributed coordination. NSFORGE_MCP_HTTP_JSON_RESPONSE=1 is opt-in and cannot stream request-scoped progress; leave its default 0 for progress notifications.

MCP Tasks is not implemented by Python SDK 2.1.1, so NSForge does not advertise a private imitation. Cancelling an await around asyncio.to_thread cannot stop the worker thread; NSForge therefore never emits a false terminal progress event, while calls with timeout_s continue to use a terminable process. That isolated process persists the same canonical phase events but replays their progress only after it returns; live per-phase delivery is the default non-timeout path.

🎬 How it works — SymPy-MCP first

The golden rule: compute & verify with SymPy-MCP, then record with NSForge (provenance + human insight at every step).

flowchart LR
    A["🤖 LLM<br/>understand + plan"] --> B["🔢 SymPy-MCP<br/>compute + verify"]
    B --> C["🔨 NSForge<br/>record step + provenance"]
    C --> D{"more<br/>steps?"}
    D -->|"yes"| B
    D -->|"no"| E["✅ complete<br/>stored formula + code"]

🧭 Autonomous task orchestration (L2 / L3)

Hand NSForge a declarative Derivation Task Spec (DTS) and it runs the whole ladder for you. task_explore turns a single answer into a space of verified answers: it runs the base derivation plus every alternative, then ranks the survivors.

flowchart TD
    DTS["📋 Derivation Task Spec"] --> BASE["base derivation"]
    DTS --> ALT1["alternative 1"]
    DTS --> ALT2["alternative 2"]
    BASE --> V["verify · acceptance oracles · provenance"]
    ALT1 --> V
    ALT2 --> V
    V --> RANK["🏆 ranked candidates<br/>verified · oracles passed · simpler"]

• task_plan — reify a DTS into an ordered, provenance-tagged plan
• task_run — run the ladder end-to-end; return run/artifact links and phase progress (optional hard timeout_s)
• task_explore — return all branches with immutable evidence and linked artifacts

📖 General-formula-exploration roadmap

🎛️ Step-by-step control

Navigate and edit a derivation like a version-controlled document. Expressions are immutable (that keeps verification honest) — to change a result, rollback to a valid state and re-derive.

stateDiagram-v2
    direction LR
    [*] --> deriving
    deriving --> deriving: get_step / update_step / insert_note
    deriving --> earlier: rollback
    earlier --> deriving: re-derive a new path
    deriving --> [*]: complete + save

derivation_get_step · derivation_update_step · derivation_rollback · derivation_insert_note · derivation_delete_step — see the tool reference.

🛠️ Tools at a glance — 91 catalog tools · 17 in the recommended workflow profile

📖 Full list with every tool: Tool Reference · machine-readable capabilities.json

✅ Verification harness

One command is the ground truth. python scripts/check.py runs 14 gates — a green run is the definition of "done".

lint · format · type · security · import · manifest · mcp · test · bench · generic · provenance · package · harness · diff

• mcp — MCP 2.1 discovery, schemas, metadata, payload compatibility, resources, prompts, and legacy-client mode
• security — no high-severity Bandit finding in executable source
• bench — known derivations reproduce correctly
• generic — unseen, randomly-composed formulas derive correctly (proves NSForge is a derivation calculus, not a hand-built library)
• provenance — every benchmark derivation carries a complete tool-provenance ledger (no hand-derived leaks)
• package — build sdist/wheel, inspect runtime assets, install in isolation, and smoke-test installed MCP
• harness — version, manifest, and gate/document parity guard the verifier itself

python scripts/check.py            # all gates
python scripts/check.py --json     # machine-readable (for agents)

📚 Derivation repository

Derived formulas are stored with derivation metadata and a lineage summary — LaTeX, SymPy form, the base formulas combined, step descriptions, verification status, and clinical/physical context.

🐍 Worked example: examples/npo_antibiotic_analysis.py

🧠 Agent skills

NSForge ships 20 pre-built skills that teach agents how to use the tools — 7 NSForge workflows (nsforge-derivation-workflow, nsforge-formula-search, nsforge-verification-suite, …) plus 13 general development skills.

📖 NSForge Skills Guide

🔗 Optional: NSForge → USolver

NSForge derives the domain-smart formula; USolver finds the math-optimal values.

flowchart LR
    N["🔨 NSForge<br/>derive modified formula"] --> P["derivation_prepare_for_optimization"]
    P --> U["🎯 USolver<br/>Z3 · OR-Tools · CVXPY"]
    U --> R["optimal parameters"]

📖 Skill: nsforge-usolver-collab

🏗️ Architecture & development

DDD with a pure domain core and a replaceable MCP layer (nsforge core has no MCP dependency).

uv sync --all-extras     # set up
uv run pytest            # tests
python scripts/check.py  # full harness (14 gates)
uv run nsforge-mcp       # start the server

📖 Architecture · Contributing · NSForge vs SymPy-MCP

🗺️ Roadmap

Reification-ladder phases 1–6 are live (engine → benchmarks → suggester → self-correction → provenance → explore mode). Remaining: Lean4 formal verification (optional) and multi-agent infrastructure.

📖 ROADMAP.md · General-formula-exploration roadmap

📄 License

Apache License 2.0

<div align="center">

NSForge — Forge new formulas through verified derivation · Where Neural meets Symbolic

</div>