dsh-danus

Readme

# dsh-danus

**Verifier-gated multi-agent mathematical proof search, native to DeepSeek Harness (DSH).** A swarm of autonomous worker agents proves; a cold-start verifier is the sole authority on correctness; verified results accumulate in a content-addressed fact graph — the only source of truth; the finished work renders into a LaTeX paper or a human progress report.

Everything runs as DSH plugins (TypeScript) on your own model endpoints — no Python, no external MCP processes, cross-platform (Windows included).

## What it does

- **Truth layer** — a content-addressed, cascade-revocable fact graph (`fact_id = SHA-256(statement, proof, predecessors, ...)[:16]`), plus three-tier memory: worker-local → project global memory (BM25-searchable findings) → verified facts. Only the fact graph is truth.
- **Role-gated tools** — six tools (`gm_add`, `gm_search`, `fact_submit`, `fact_search`, `fact_revoke`, `search_arxiv_theorems`) with a structural permission table: the orchestrating *main* agent has no `fact_submit`, the *verifier* is read-only, unknown roles fail closed.
- **Cold-start verifier** — every submission runs deterministic prechecks (vacuousness thresholds + P1/P3/P5 hard prohibitions), then a **fresh, isolated headless judge session** decides: `correct = no critical errors and no gaps`. Rejections come back with repair hints; verdicts are always traced to global memory.
- **Worker swarm** — detached per-worker round loops (`danus-worker` profile), one fresh headless session per round resuming from persisted memory; graceful `.stop`, deadlines, round caps, stuck detection, cross-platform process supervision.
- **Orchestration tools** — `danus_new / assign / start / status / stop / finalize / list` for the main agent, plus a heartbeat plugin driving the 30-minute control beat and 4-hour macro audit, riding DSH native goals and subagents.
- **Rendering** — fact graph → publishable LaTeX paper (planner/writer/auditor/reviser/verifier roles, chunked PLAN→FILL→STITCH, compile gate, whole-paper math re-verification) and fact graph → human progress report, each produced by an isolated one-shot session with leak gates and provenance.
- **Observability** — a read-only dashboard served from DSH own web server (`/danus`), no extra process.
- **Model freedom** — workers, verifier, and main agent each use their own DSH profile; point any of them at any configured LLM provider (`agent-default-model` per profile).

## Verification

- **102/102 tests green** (`pnpm test`), including byte-exact golden vectors generated by the original implementation.
- Live end-to-end on a real DSH install: project scaffolding → worker round → `fact_submit` → independent cold-start judge → fact `cefabd883755ac88` in the graph.
- `PARITY.md` maps every behavior to the original, item by item.

## Quickstart

    pnpm install && pnpm test

    # three compositions: main (web profile), danus-worker, danus-verifier
    # see README.zh.md (Chinese) for the exact cordis.patch.yml blocks
    dsh --profile headless --patch ./dev-overlay.yml "Call danus_list and report the result"

## Layout

    src/core/          truth layer (pure TS, zero DSH deps)
    src/services/      verify (cold-start judge) · swarm (worker lifecycle) · write-paper · human-summary
    src/plugins/       gateway (role-gated tools) · orchestration · heartbeat · observability · ...
    src/swarm/         the worker outer loop + cross-platform process supervision
    src/shared/        layout · headless spawn · target · env
    skills/ contracts/ agent skills and role contracts
    spec/              authoritative behavior specs extracted from the original
    PARITY.md          per-feature parity checklist against the original

## License & credit

Apache 2.0 (see `LICENSE`). This project is a native TypeScript/DSH port based on **[Danus](https://github.com/frenzymath/Danus)** by frenzymath — the architecture, agent contracts, skills, and behavior specs are theirs; see `PARITY.md` for the detailed correspondence and intentional differences.