dsh-danus

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.