Platform & handoff

Architecture — system layers and contracts.

The system layers and the contracts between them. How DiscoveryLab is composed end to end.

Architecture · full system at a glance

From any MCP agent to an approved lab job — then a governed improvement proposal.

Eight layers, five MCP servers, eighteen tools, three non-negotiable gates. Every box below is a file you can grep; every arrow is a typed call you can intercept; every gate is enforced in code, not policy. This is the same composite dispatcher peptiter-mcp-stdio binds to stdio, drawn out so you can see the whole system at once.

L1 · agent ingress · stateless, transport-agnostic

Any MCP host

Claude Code · Anthropic SDK · any newline-JSON-RPC 2.0 client that can spawn a child process. No SaaS round-trip — the host launches the binary as a subprocess and writes one request per line on stdin.

newline JSON-RPC over stdio

L2 · composite dispatcher + persistence

peptiter-mcp-stdio · CompositeMCPServer

MCPDispatcher routes by tool-name prefix. Every envelope audit-logged. tools/list-version pins the catalog SHA256; --concurrent N opts into a TaskGroup pool with an actor- serialized stdout writer so JSON lines never interleave.

OnDiskCache + inspector

Sub-dirs under --cache-dir: lean/, lab_loop/. peptiter-mcp-cache --evict surgically removes one entry; --prune-cache 7d evicts at startup.

tools/call dispatched by prefix

L3 · 5 first-party MCP servers · 18 tools total

literature/*

4 adapters: PubMed, Semantic Scholar, Europe PMC, local fixture. Returns EvidenceCards with provenance + ClaimTriples.

literature/searchliterature/list_adapters

lean/*

Wraps LeanExternalVerifier. Hash-bound receipt with native_decide proofs + per-path attribution. cachedHash / noCache short-circuits.

lean/verifylean/list_modules

lab_loop/*

V3LabLoopOrchestrator behind a typed surface. cachedFingerprint short-circuit. lab_loop/inspect re-reads cached Trace by fingerprint.

lab_loop/runlab_loop/inspectlab_loop/list_named_loops

improvement/*

Recursive Discovery Loop proposals. Evaluate, verify, approve, promote, inspect, and rollback artifact changes without rewriting authority boundaries.

improvement/proposeimprovement/evaluateimprovement/verifyimprovement/approveimprovement/promoteimprovement/inspectimprovement/rollback

model/*

Local-model candidate emission. Outputs explicitly self-identify as candidate_unverified — must round-trip through lean/verify before anything downstream.

model/emit_biology_specmodel/extract_claim_triplesmodel/suggest_mechanism_canvasmodel/list_training_sources

L4 · backing modules · what each server actually drives

research

LiteratureCopilot (4 adapters) · EvidenceCard (Codable + provenance) · ClaimExtractor (typed predicate vocabulary) · EvidenceGraph + EvidenceGraphMechanismBridge.

verifier

LeanExternalVerifier · biology_v0 / v1 / v2 / v3 / v3_signed manifests · BiologyV0–V3.lean · PathwayLean.Core · lake build round-trip.

orchestrator

V3LabLoopOrchestrator · AssayPlanDrafter (vehicle / dose-span / plate / risk gates) · LabJobQueue (one-way state machine) · ActiveLearningEngine (Beta α,β).

improvement

RecursiveDiscoveryLoopPolicy · ImprovementProposal · ValidationPlan · ImprovementMCPServer · promotion receipts · rollback records.

local model

PeptiterModelMCPServer · BiologySpec emitter · ClaimTriple extractor · MechanismCanvas drafter · ModelTrainingSourceInventory · DeepShitMacModelBundle wiring · BioFoundation scorecard imports.

Gate 1 · Audit boundary

Model output is candidate_unverified. Period.

Every model/* response carries verification.status = candidate_unverified and a caveats array reminding callers to round-trip through lean/verify. Generative breadth is allowed; formal narrowing is required. Nothing the local model emits crosses this line without a hash-bound Lean receipt.

candidate ↦ lean/verify ↦ hash-bound receipt

L5 · TensFormer ↔ Lean verification spine

TensorLang manifest · semantic_hash · Lean theorem

The TensorLang DSL (semiring-einsum, threshold, fixpoint) compiles biology_v* artifacts down to a finite reasoning fragment. The same fragment is encoded in Lean (BiologyV0–V3) with native_decide proofs for every signed-sum and path-count theorem. semantic_hash binds the two — a Lean receipt is only valid against the manifest hash it was produced from. Per-path attribution flows back so reviewers see protective vs risk paths, not just the summed sign.

verified mechanism + attribution

L6 · closed-loop orchestration

V3LabLoopOrchestrator → AssayPlanDrafter → draft AssayPlan

Drafter encodes safety as code: vehicle present, dose schedule spans 3 orders of magnitude, plate map has no double-assigned wells, risk screen returns no biosecurity / dual-use flags. Pass → .readyForReview. Fail → .rejected with the specific reason. A reviewer never sees an unsafe plan in the queue.

Gate 2 · Approval gate

L4 ceiling. Every executable lab job requires human review.

LabJob has a one-way state machine (drafted → approved → queued → running → returned → analyzed). The .approved transition can only fire from a human reviewer in the workbench. No L5+ autonomy is enabled in code — pre-approved experiment classes within budget + safety bounds are scoped for a future SCIENTIST.md milestone, gated on a hardened approval system.

approved → queued → running → returned

L7 · lab queue + active learning + returned evidence

LabJobQueue + ActiveLearningEngine (Beta α, β)

CandidateBelief is a Beta(α, β) conjugate prior. Outcomes flip the next-experiment pick on every assay: positive bumps α, negative bumps β, inconclusive widens without bias. pickNextExperiment chooses the highest-posterior-variance candidate so the loop spends its budget where it learns the most. Trace is persisted via OnDiskCache so cold restarts answer lab_loop/inspect by fingerprint. Returned results, failed gates, and reviewer corrections can then enter improvement/propose.

Gate 3 · Promotion gate

Recursive discovery cannot recursively expand its own authority.

ImprovementProposal artifacts can change ranking, retrieval, mechanism templates, assay selection, prompts, schemas, and eval harnesses. Proposals that touch safety gates, claim thresholds, wet-lab permissions, or verifier requirements are classified as forbidden and cannot be promoted by the loop.

returned evidence ↦ improvement/propose ↦ reviewed artifact

L8 · Recursive Discovery Loop

ImprovementProposal → eval gates → human approval → promotion receipt

The improvement server turns wet-lab outcomes, Lean failures, reviewer corrections, eval regressions, counterevidence, and agent self-critiques into auditable proposals. Every proposal names affected artifacts, expected gain, risk class, validation plan, rollback plan, and evidence. Promotion creates a receipt; failure creates a regression case.

External feeders + CI surface

external data

PubMed E-utilities · Semantic Scholar Graph API · Europe PMC REST · Reactome (TSV) · Open Targets (Parquet) · BioFoundation provider scorecards. All optional — fail-loud rather than silently fall back to fixtures.

biofoundation adapters

deterministic · TranscriptFormer · Geneformer · scVI · AIDO.Cell · Arc State · AlphaGenome · BioHub ESM contracts emit scorecards with calibration state before graph ingestion.

CI / regression bench

eval_harness regenerates eval_badge.svg + EVAL.md on every PR · sticky PR comment via marker · check_overlay_sync.py blocks BIOLOGY_OVERLAY drift · pathway-lean.yml runs lake build · regression tests gate merges and prevent previously failed improvement proposals from reappearing.

Box — a typed module (Swift type, MCP tool, or persisted artifact). Every label maps to a file you can grep.

Highlighted box — the single composite dispatcher that fan-outs every agent call.

Dashed gate — an audit or approval boundary the platform refuses to skip. Enforced in code, not in a policy memo.

Related on this track

Experiments

Validation and assay planning.

AI Scientist

Research loop and next-action reasoning.