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

[![License](https://img.shields.io/badge/License-Apache%202.0-blue.svg)](LICENSE)
[![Python](https://img.shields.io/badge/Python-3.12+-green.svg)](https://www.python.org/)
[![MCP](https://img.shields.io/badge/MCP%20SDK-2.1.1-purple.svg)](https://modelcontextprotocol.io/)
[![Tools](https://img.shields.io/badge/MCP%20tools-91-8b5cf6.svg)](docs/tools-reference.md)
[![Harness](https://img.shields.io/badge/verification-14%20gates-brightgreen.svg)](#-verification-harness)

🌐 **English** | [繁體中文](README.zh-TW.md)

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

| The LLM does… | NSForge does… |
| ------------- | ------------- |
| Understand the question | Precise symbolic computation |
| Plan the derivation | Track every step's **provenance** |
| Explain the result | **Verify** (dimensions, boundary, equivalence) |
| — | Store the formula, generate code |

> **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>

```mermaid
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](docs/reification-ladder-direction.md) · [General-formula-exploration roadmap](docs/general-formula-exploration-roadmap.md)

---

## 🌍 Ecosystem: don't reinvent the wheel

NSForge works **with** other MCP servers, not against them.

```mermaid
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")]
```

| ✅ Belongs in NSForge | ❌ Use another tool |
| -------------------- | ------------------ |
| Temperature-corrected drug elimination | Basic physics formulas → sympy-mcp |
| Body-fat-adjusted volume of distribution | Physical constants → sympy-mcp |
| Renal-function dose adjustments | Clinical scores → medical-calc-mcp |
| Custom composite PK/PD models | Textbook formulas → references |

---

## 📦 Installation

**Requirements:** Python 3.12+ and [`uv`](https://docs.astral.sh/uv/) (recommended).

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

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

```bash
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

```json
{
  "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:

| `NSFORGE_TOOL_PROFILE` | Tools | Intended use |
| --- | ---: | --- |
| `legacy` _(default)_ | 82 | v0.3-compatible surface; `NSFORGE_ENABLE_MUSIC=1` still expands it to 91 |
| `workflow` | 17 | Recommended resource-first, strict agent workflow |
| `scientific` | 35 | Stateless symbolic calculation, simplification, and verification |
| `interactive` | 35 | Workflow plus session editing and handoff operations |
| `full` | 91 | Complete compatibility/discovery surface, including music |

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:

```bash
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:

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

```mermaid
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"]
```

| Task | Tool | Why |
| ---- | ---- | --- |
| Math computation | SymPy-MCP | Full ODE / PDE / matrix support |
| Formula display | `derivation_show` | User confirms each step |
| Knowledge storage | NSForge | Provenance, searchable |
| Dimension check | NSForge `check_dimensions` | Physical-unit verification |

---

## 🧭 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.

```mermaid
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](docs/general-formula-exploration-roadmap.md)

---

## 🎛️ 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.

```mermaid
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](docs/tools-reference.md#-derivation-engine-31).

---

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

| Module | # | What it does |
| ------ | :-: | ------------ |
| 🔥 Derivation engine | 31 | Stateful sessions: compose, step, track, store |
| 🔢 Calculation | 12 | Limits, series, sums, inequalities, probability |
| 🔣 Advanced algebra & transforms | 14 | expand/factor/apart… + Laplace / Fourier |
| ✅ Verification | 6 | Equality, derivative, integral, dimensions |
| 🌐 Formula search | 6 | Wikidata, BioModels, SciPy constants |
| 💻 Code generation | 4 | Python, LaTeX, report, SymPy script |
| 📝 Expression | 3 | Parse, validate, extract symbols |
| 🧭 Task orchestration | 3 | `task_plan` / `task_run` / `task_explore` |
| 🧭 Suggester | 1 | Retrieval-augmented next-step ranking |
| 🎵 Music _(full or legacy opt-in)_ | 9 | Symbolic tones → waveform, spectrum, WAV |
| 🧩 Runtime self-description | 2 | `nsforge_health` · `nsforge_manifest` (agent harness) |

> 📖 **Full list with every tool:** [Tool Reference](docs/tools-reference.md) · machine-readable [`capabilities.json`](docs/agent/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

```bash
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.

| Derivation | Domain | Description |
| ---------- | ------ | ----------- |
| [Temperature-corrected elimination](formulas/derivations/pharmacokinetics/temp_corrected_elimination.md) | PK | First-order elimination + Arrhenius |
| [NPO antibiotic effect](formulas/derivations/pharmacokinetics/npo_antibiotic_effect.md) | PK/PD | Henderson-Hasselbalch + Emax |
| [Temperature-corrected Michaelis-Menten](formulas/derivations/pharmacokinetics/temp_corrected_michaelis_menten.md) | PK | Saturable kinetics + temperature |
| [Physiological Vd by body composition](formulas/derivations/pharmacokinetics/physiological_vd_body_composition.md) | PBPK | Vd adjustment for body composition |

> 🐍 Worked example: [`examples/npo_antibiotic_analysis.py`](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](docs/nsforge-skills-guide.md)

---

## 🔗 Optional: NSForge → USolver

NSForge derives the *domain-smart* formula; [USolver](https://github.com/sdiehl/usolver) finds the *math-optimal* values.

```mermaid
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`](.claude/skills/nsforge-usolver-collab/SKILL.md)

---

## 🏗️ Architecture & development

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

```bash
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](ARCHITECTURE.md) · [Contributing](CONTRIBUTING.md) · [NSForge vs SymPy-MCP](docs/nsforge-vs-sympy-mcp.md)

---

## 🗺️ 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](ROADMAP.md) · [General-formula-exploration roadmap](docs/general-formula-exploration-roadmap.md)

---

## 📄 License

[Apache License 2.0](LICENSE)

<div align="center">

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

</div>