DiscoveryLab designs interventions across modalities — peptides, small molecules, designed proteins, and microbiome-mediated routes — then finds the combination that holds a disease variable in its target state across the full dosing cycle, even when every agent on its own falls short. Every result ships with a machine-checked stability proof and a pre-registered wet-lab experiment whose kill-criterion is named in advance — so a hypothesis is testable, not just plausible.
Strongest in peptide discovery — receptor-aware families distilled from a ~10¹³ sequence space — but the verification layer is modality-general, and combinations span all three paths.
Honest scope These are certified designs with documented surrogate efficacies — in-silico, not clinical claims. Every proof binds to an orthogonally measurable endpoint; one external wet-lab factorial is the validation gate.
Every competitor ships a model that scores and a story about why. We ship a proof. DiscoveryLab encodes its core claims in Lean 4 — the same proof assistant used to verify mathematics and safety-critical systems — and recompiles every one of them in CI. A claim that doesn't pass doesn't ship. This is the moat: not a better score, a checkable guarantee.
A drug acting on a disease variable is modeled as a feedback controller; Lean proves the closed loop descends — V̇(x) ≤ −ε‖x‖² for every state — in exact integer arithmetic. Generic 2-, 3-, and n-state framework.
One theorem certifies a combination is stable at the dosing-cycle peak AND trough, in-band, below the over-suppression ceiling, and strictly better than any monotherapy. Each receipt also carries an 81-world ±15% potency × PK-trough robustness margin, so the verdict doesn't hinge on the surrogate numbers.
Each safety axis (CNS, cardiac, hepatic, renal, GI, immunogenicity, metabolic) is re-encoded in Lean and proven to compute the exact same verdict as its audited scorer — pinned to the source hash, so drift breaks the build.
Mechanism graphs are checked path-by-path with signs, catching the cancellation-hides-signal failure an unsigned check misses — the formal backbone of every attributed claim.
A receipt proves the math is correct given the model and its documented surrogate constants — it is an in-silico certificate, not a clinical claim, and the only bridge to the clinic is a pre-registered wet-lab factorial with its kill-criterion named in advance. We state that line plainly because it is exactly what a serious reviewer checks — and being able to state it is the difference between a verified design and a generated one.
That same discipline runs at generation time: designed sequences are screened against configured select-agent and toxin deny-lists before any wet-lab handoff, hits are blocked, and the screen fails closed if its database cannot load — an operational, rank-only gate, not a comprehensive biorisk clearance.
The framework is general — new indications are new instantiations, not new mathematics. Receipts we are composing next:
DiscoveryLab now has a learned peptide generator behind the receptor-first lane: receptor-peptide PDB complex pairs train the sequence model, receptor context conditions candidate generation, and no-wet-lab runs can rehearse the feedback loop with clearly marked MockLab simulations.
Build 2 adds a BioFoundation Adapter Layer for deterministic, TranscriptFormer, Geneformer, scVI, AIDO.Cell, Arc State, AlphaGenome, and BioHub ESM-style provider contracts. It turns cell-state, protein, variant, perturbation, and execution-plan context into explicit scorecard JSON instead of untracked model notes.
evidence_graph.py build accepts repeatable --biofoundation scorecards and creates biofoundation_context, calibration-state, organ-state, target-cell, protein, variant, perturbation, and execution-plan claims with benchmark next actions when outputs remain rank-only.
Peptide + designed-protein + small-molecule combinations are certified as Lyapunov-stable feedback controllers that are control-adequate where no monotherapy is — proven in Lean (lake build, CI-recompiled), robustness-checked over an ±15% surrogate-error grid, and shipped with a pre-registered factorial. Three worked examples (C5a, IL-6, glucose); reproduce with peptiter-reproduce-combination.
receptor_inverse_complex_gru_v2 learns from 12,643 PepBDB receptor-peptide PDB complex pairs, conditions on receptor sequence and hotspot context, runs locally on Apple Silicon MPS, and emits learned receptor-first peptide hypotheses.
The Swift lane still keeps the deterministic residue-preference fallback, but it can now ingest generated_candidates.json, rank model-backed RIG candidates, carry model provenance, and export assay-gated LabCandidate batches.
The feedback retraining path now looks for measured returned assay rows, writes an audit report, and deliberately skips model training when only MockLab, fixture, or absent labels are available.
The receptor-inverse candidates can flow through a MockLab simulator that emits simulated outcomes across 9 assay axes, then trains sandbox-only heads behind an explicit --allow-simulated gate.
Round 1 MockLab outcomes rank the 30 receptor-inverse candidates, classify mock promote/revisit/reject decisions, generate 12 second-round analogs, and send them through a second simulated feedback/retraining pass.
LabSpace batches can export synthesis, purification, stability, binding, activity, and toxicity-style readouts into lab_feedback.csv. MockLab exports remain simulated-only, while non-MockLab provider rows become measured retraining inputs.
The new loop runner exports LabSpace returns, executes the measured-label retraining gate, optionally trains simulated sandbox heads, and writes a single promotion-status report so MockLab rehearsal cannot be confused with wet-lab evidence.
GHK-Cu, MOTS-c for the NAD/SIRT axis, a BRC4-like RAD51 peptide, and a BLM DDR fragment now have sequence-level descriptor cards. IK14800 is kept as a metadata hold until a source-confirmed sequence is attached.
The Swift library now registers GHK, MOTS-c, RAD51/BRC-like, and BLM fragment seeds, while IK14800 is explicitly blocked from analog generation because the repository has no primary sequence.
The default registry tracks Reactome, GO-CAM, and Open Targets source releases, evidence namespaces, redistribution policy, layer/status counts, blocked claims, and linked executable islands.
Each card records context of use, calibration state, update cadence, uncertainty method, validation endpoints, governance boundaries, allowed claims, and blocked clinical claims.
PeptiterModelMCPServer now exposes list_world_model_sources, inspect_pathway_assertions, and body_twin_model_card so external agents see the same governance contract as the tests.
The adapter layer now accepts cell atlas, protein sequence, regulatory variant, perturbation, and external execution-plan contexts and emits scorecards with provider provenance, calibration state, caveats, and bounded claim language.
deterministic, transcriptformer, geneformer, scvi, aido-cell, arc-state, alphagenome, and biohub-esm are registered as explicit contracts so frontier biology priors can be planned or imported without pretending every provider has already run.
BioFoundation scorecards now attach to candidate graphs beside ChemCheck-ESA, creating biological-context claims and benchmark next actions while blocking rank-only outputs from becoming go/no-go evidence.
ESM-2 embeddings remain the common 2560-dimensional candidate state consumed by task heads, benchmarks, and Swift scoring.
The current run retrained six heads with 1024-wide MLPs, scaffold splits, leakage reports, PyTorch checkpoints, source and compiled Core ML artifacts, and repository predictions.
ActiveLearningBatchExporter can now delegate expected-improvement or upper-confidence-bound acquisition to a BoTorch Python bridge before exporting wet-lab batches.
The site now separates infrastructure progress from biology claims: trained heads and pathway priors can prioritize candidates, but assay results still decide biological truth.
Pathway assertions now carry source release, license, context, evidence, knowledge status, confidence, executable-island links, and explicit blocked claims.
Local scoring prefers committed .mlmodelc bundles, requests all available Core ML compute units, and shares one Float32 MLMultiArray across all loaded heads for a candidate embedding.
The requested DNA-repair and skin-repair peptides are now separated into scored sequence records and evidence holds, with assay gates for stability, permeability, toxicity, synthesis, pathway fit, and perturbation evidence.
ReceptorHotspotMap, ResiduePreferenceMatrix, ReceptorConditionedPeptideDesigner, NegativeDesignPanel, and ReceptorFirstBatchExporter now turn a target interface into ranked peptide hypotheses with residue-level rationales.
receptor_inverse_complex_gru_v2 trained on 12,643 receptor-peptide PDB complex pairs, beat a smoothed unigram amino-acid baseline by 71.8% on validation perplexity and 72.7% on test perplexity, and generated 30 exact-novel quality-filtered candidates.
Measured feedback retraining now has an executable audit gate; it will train only from returned assay labels and currently records skipped_no_measured_labels instead of promoting simulated data.
MockLab now turns receptor-inverse candidates into 270 simulated good/bad assay rows and a sandbox-only retraining run, while the measured-feedback path still rejects those rows by default.
The mock active-learning planner ranks first-round outcomes, proposes 12 second-round analogs, simulates 108 more assay rows, and retrains a second sandbox model without touching measured-feedback claims.
Provider-returned LabSpace batches can now be exported to the same backbone lab_feedback.csv contract, preserving MockLab simulation labels and letting real provider rows enter the measured retraining gate.
A single command now chains LabSpace export, measured retraining, optional simulated sandbox retraining, and a promotion-status report with separate artifact directories for measured and simulated outputs.
The new adapter converts frozen-model or deterministic biological context into an auditable scorecard before the Agentic Evidence Graph is allowed to reason over it. The graph records provider provenance, calibration state, caveats, and next benchmark actions instead of treating model output as assay evidence.
The proof run used 12,643 PepBDB receptor-peptide PDB complex pairs, trained on Apple Silicon MPS, selected epoch 12, reached 5.382 validation perplexity versus a 19.058 unigram baseline, and generated 30 exact-novel quality-filtered candidates across RAD51, GLP1R, and BRD4 contexts.
A dry run sampled random good/bad outcomes for all 30 receptor-inverse candidates across binding, activity, stability, permeability, synthesis, purification, aggregation, and toxicity-style gates. The normal retraining path skipped those rows; only the explicit sandbox run trained from them.
The planner scored the first 30 candidates from simulated feedback, kept five mock promotes, generated 12 exploit/explore analogs, ran MockLab again, and trained a second sandbox model from 108 additional simulated rows.
DiscoveryLab is organized around a compact navigation spine: discovery inputs, product workflow, mechanism proof, recursive discovery, epigenome rescue, platform handoff, and competitor comparison. Each route preserves the detailed sections while giving readers a clear task-oriented path.
Start with phenotype, contraindications, pathway context, and testable therapeutic intent.
Move from natural parent peptides and evidence-backed source systems into bounded scaffold families.
Reduce combinatorial sequence space with receptor, motif, stability, synthesis, and family constraints.
Carry each program through Program, Discover, Evidence, Portfolio, and Handoff workspaces.
Check pathway reachability, blockade, safety, conservation, perturbation support, and Lean receipts.
Turn lab returns, proof failures, reviewer corrections, and eval regressions into gated improvement proposals.