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 by frenzymath — the architecture, agent contracts, skills, and behavior specs are theirs; see PARITY.md for the detailed correspondence and intentional differences.
