TensFormer is the typed world-model spine that the rest of the proof stack composes against.
The in-silico lab above triages every candidate through standardized assessments. TensFormer is the second, complementary spine: a JEPA-style predictive world model whose mechanism claims are projected through a typed tensor IR, exhaustively checked locally, and re-derived in Lean 4 under a shared semantic hash. Neural confidence does not imply proof; the TensFormer contract makes that boundary explicit and machine-checkable.
A graph transformer with structure-aware features (AlphaFold / Boltz-class priors) trained with JEPA-style objectives. It predicts a latent body-state shift under intervention plus a candidate mechanism hypothesis, but never claims to be the truth.
An independent open-source DSL inspired by Pedro Domingos's Tensor Logic. The neural backbone emits a typed module over biological domains; semiring-einsum gives Bool reachability and signed mechanism in one schema; finite-Bool fragments are exhaustively verified locally.
PathwayLean re-derives the same closure under reachFuel and decides each obligation with native_decide. It binds an auditIdentity checksum to TensorLang's semantic_hash so the two backends prove the same finite fragment — disagreement is itself an audit failure.
Verified mechanism hypotheses and surfaced counterexamples flow into LabSpace as testable batches. Outcomes update the relation tensors for the next iteration. The IR contract stays stable across model and biology changes.
Roles do not overlap. Neural is the only thing that learns continuous biology. TensorLang is the only thing that types and executes the symbolic projection. Lean is the only thing that issues formal proof receipts. Wet lab is the only thing that decides what is true.
A peptide mechanism graph carries the same Peptide × Target × Pathway × CellState × Endpoint axes for both tiers. The semiring choice — not the schema — controls whether the model reasons about possible reach, weighted product, or (planned) probabilistic flow.
(semiring-einsum bool-or-and "pt,tw->pw" Binds ParticipatesIn)
(einsum "pt,tw->pw" BindsSign ParticipatesInSign)
The eval harness encodes 5 peptide candidates modeling guselkumab, ustekinumab, secukinumab, a broad-JAK inhibitor, and an anti-TNF — annotated against their FDA-label intended indications and documented black-box signals. Every change to the model regenerates this table.
| Metric | v1 Bool | v2 signed | Δ |
|---|---|---|---|
| Aggregate F1 | 0.750 | 0.818 | +0.07 |
| Aggregate accuracy | 0.760 | 0.840 | +0.08 |
| Efficacy F1 | 0.800 | 0.800 | — |
| Safety F1 | 0.667 | 0.857 | +0.19 |
| Safety precision | 0.600 | 1.000 | +0.40 |
| Safety recall | 0.750 | 0.750 | — |
Smoke-test scope (5 × 5 = 25 cells per model). Aggregate F1 has high variance at this scale; per-question metrics are the more honest signal. Recall is unchanged because both tiers share the same Bool reachability backbone — the win is in eliminating false safety alarms, not in finding more risks.
Anti-IL12/IL23 (p40) blockade suppresses Th1 antiviral defense. The TB / herpes-zoster signal in the FDA label is what the verifier reproduces.
JAK2 inhibition disrupts erythropoietin signaling. Matches the well-documented anemia signal in the broad JAK-inhibitor class.
Bool reachability flagged this as a v1 false positive. The signed layer correctly reads the path product as net protective — secukinumab is an IL-17A antagonist.
$ tl verify biology_v2.tl --json efficacy_*_protects_psoriasis → passed (×3) efficacy_tnf_decoy_protects_ibd → passed safety_no_peptide_activates_storm → passed ← v1 false positive resolved safety_no_peptide_activates_infection → failed (p: ustekinumab_like) safety_no_peptide_activates_anemia → failed (p: broad_jak_pep) v1_false_positive_resolved → passed
Every TensorLang module hashes deterministically over its source. Lean's auditIdentity.artifactChecksum embeds that hash. A Swift verifier loads both, confirms they agree, and (when an elan toolchain is present) drives lake build to confirm Lean re-derives every obligation. Drift becomes an audit failure, not a silent regression.
let receipt = try LeanExternalVerifier().verify(.init( manifestPath: .../biology_v1.reasoner.json, leanSourcePath: .../BiologyV1.lean, lakeExecutable: .../.elan/bin/lake, lakeWorkingDirectory: .../Packages/PathwayLean )) receipt.module == "peptiter.biology_v1" receipt.manifestSemanticHash == "e065d18796a17c58…" receipt.leanArtifactChecksum == "e065d18796a17c58…" receipt.hashesMatch == true receipt.lakeBuildSucceeded == true receipt.status == .verified // per-property TL verdict carried through: receipt.tensorlangResults // [efficacy_* → passed, safety_no_peptide_to_anemia → failed (p: broad_jak_pep), …]
Manifest declares input/output shapes over biological domains.
Deterministic over module source. Drift is detectable.
Per-property pass/fail with explicit counterexamples.
native_decide on the same fragment — independent witness.
Lean's auditIdentity is the manifest's semantic_hash.
First-class Codable types, four-state status, testable.
The integration spine is in place. Each future change publishes a regenerated EVAL.md so we can tell which moves help and which add complexity without a measurable win. None of these are speculative product features — they are concrete extensions of the typed schema, the semiring layer, and the Lean theory.
emit_biology_v2.py enumerates every signed mechanism path through biology_v2 (23 paths across 14 peptide × endpoint pairs). The Swift LeanExternalVerifier surfaces per-path verdicts so opposing edges from the same peptide no longer cancel into a silent zero — both the protective and risk paths reach the reviewer.
BiologyV2.lean encodes 14 signed-sum theorems and 28 path-count theorems decided by native_decide; lake build is green. auditIdentity.artifactChecksum binds to TensorLang's biology_v2 semantic hash so drift between the two backends is an audit failure.
PathwayLean.Core gained SignedPathRecord plus signedSum / riskPathCount / protectivePathCount / netActivator / netProtective — generic over Peptide and Endpoint inductive types. BiologyV3.lean ships 30 qualitative theorems (net_activator / net_protective / no_net_effect, one per non-zero peptide × endpoint cell) decided by native_decide.
reactome_loader + opentargets_loader + transpile_biology compose public mechanism data with the Peptiter-specific BIOLOGY_OVERLAY (cell-state and endpoint annotations) into a SignedV2Spec. biology_v3 (10 peptides, 7 targets, 9 pathways via the IL-23/IL-17/JAK-STAT fixture) and biology_v3_signed (47 enumerated signed paths) are emitted via the same pipeline; tl verify + lake build green. Real Reactome download bootstrap (download_reactome.py + build_biology_v4.py) ships gitignored under transpiler/real/ — pyarrow-gated Open Targets Parquet adapter for the next data scale-up.
V3LabLoopOrchestrator composes ActiveLearningEngine + AssayPlanDrafter + LabJobQueue: pick highest-uncertainty candidate via Beta(α, β) priors, draft an AssayPlan (vehicle / dose schedule / plate map / risk screen all gated), route through the approval gate, walk the LabJob lifecycle drafted → approved → queued → running → returned → analyzed, attach the simulated outcome, update the belief. SCIENTIST.md §11.6 contract demonstrated end-to-end.
A log-sum-exp semiring over the committed biology_v2 schema — same domains, same einsum spec. semiring_spine.py reproduces the hard tiers exactly (14/14 decisive claims) and adds calibrated P(net-protective) + evidence strength. Now Lean-verified to v2 parity: biology_prob_v1.tl (tl check green) + BiologyProbV1.lean (native_decide, lake build green) re-derive P = protective/(protective+risk) exactly — efficacy = 100%, the broad-JAK infection catch = 0%, MAP equals the signed verdict — all three artifacts bound to one semantic hash (3d7281c9…).
Today emit_biology.py is hand-curated. A small transformer that consumes (peptide, context) and emits a BiologySpec JSON validates the boundary in INTERFACE.md before any large pretraining run.
Beyond static reachability to perturbation-conditioned trajectories. The v2 signed mechanism is a per-step influence operator; a discrete Euler update state_t + intervention → state_t+1 over scaled-integer cell-state is now Lean-verified: BiologyTemporalV1.lean (native_decide, lake build green, hash 486594b9…) proves a guselkumab_like intervention is monotone-down on treatment, halved at trough, bounded, and rebounds after washout — plus a discriminator theorem that an adverse Th17-promoting driver is NOT suppressive.
The probabilistic tier's uniform prior is replaced with live OpenTargets Platform target↔disease association scores. A noisy-OR over each path's MoA × association gives calibrated confidence varying 0.00–0.83 where the hard tier flattens to ~1. Validated: secukinumab → IBD scores only 0.23 (IL17A–IBD 0.13) — IL-17 blockade is genuinely weak/harmful in IBD — correctly down-weighted. Lean-verified and tightened: BiologyConfV1.lean encodes each score as a ±5% permille interval and native_decide pins an EXACT confidence band [lo,hi] for all 10 claims (width ≤120), proves the robust strongest/weakest, and — honestly — proves the overlapping middle is NOT strictly orderable (no false precision). hash da856445….
BiologyConfV2.lean tightens the uniform band into a claim-specific one from OpenTargets evidence breadth — band = clamp(80−20·n_datatypes,15,80) permille, so well-corroborated associations earn narrower bands. native_decide proves 2 robust orderings the uniform band could not: e.g. guselkumab→IBD [615,653] now sits above guselkumab→psoriasis [511,587] (same drug; IL23R↔IBD has 3 corroborating datatypes vs 2). And it proves the genuinely-similar IBD mid-cluster still overlaps — no false precision. hash 116deb02….
The explicit semiring abstraction is lifted into the production engine: SemiringSpine.swift defines a Semiring protocol (zero/one/⊕/⊗/edge) with Bool / signed / log-sum-exp instances and one generic contraction that runs the same mechanism chain under any tier. All three new tiers are registered in the MCP catalog; SemiringSpineTests checks the engine and that each tier's manifest hash binds its Lean auditIdentity.
peptide_ground_truth.json now covers 10 candidates (the original 5 plus risankizumab, ixekizumab, adalimumab, baricitinib, upadacitinib) with FDA-label provenance. Every release ships an EVAL.md diff via eval_harness --diff-against-base, plus an SVG badge consumable from any README or dashboard.
Claim boundary. A TensFormer verification receipt proves that a candidate's mechanism claim is internally valid under declared assumptions and that two independent verifiers agree. It does not prove the underlying biology is true. That remains the wet lab's job. The IR contract makes that distinction machine-checkable instead of editorial.
TensorLang is an independent open project inspired by Pedro Domingos's Tensor Logic: The Language of AI (arXiv:2510.12269). TensFormer is the peptide-discovery application of that IR.