← Proof
Mechanism proof
PeptCheck v8.6 safety-axis benchmark.
The multi-axis gate benchmark — 56 scored peptide-drug entries with 100.0% full agreement across axes.
Four Lyapunov axes · seven safety axes · PeptCheck v1.9 · 100.0% honest
PeptCheck v8.6 adds source-backed noncanonical positive controls without moving a threshold.
The current reference gate scores 56/56 on the expanded PeptCheck matrix: 100.0% calibration, 100.0% held-out validation, and 100.0% full benchmark agreement. v8.5 resolved lepirudin by separating commercial withdrawal status from label-documented anti-hirudin antibody/anaphylactoid concern; v8.6 (PeptCheck v1.9) promotes cetrorelix, ganirelix, icatibant, and difelikefalin to held-out positive controls with exact noncanonical-residue maps. No safety-axis threshold moved.
60-entry benchmark · 56 scored · representative verdicts
drug · structured contextlyapimmaxisverdict
semaglutide
approved
A8 Aib, K26 gamma-Glu-2xOEG-C18-diacid
tirzepatide
approved dual GLP-1/GIP
A2 Aib, A13 Aib, K20 C20-diacid
taspoglutide
P3 safety failure
A8 Aib, G35 Aib in the C-terminal MHC-II register
Independent catch: immunogenicity axis.
anaritide
P3 failed AKI prevention
ANP(1-28); C7-C23 natriuretic disulfide loop
Renal catch: natriuretic loop plus ATN/AKI indication context.
ularitide
P3 failed TRUE-AHF
Urodilatin; C11-C27 natriuretic loop with ADHF hypotension context
Renal catch; cardiac hypotension liability remains visible as defensive depth.
ecallantide
boxed warning anaphylaxis
60-aa recombinant Kunitz domain, 3 disulfides
Immunogenicity catch: Kunitz domain plus label anaphylaxis warning.
ziconotide
boxed warning psychiatric AEs
25-aa conotoxin, intrathecal route, psychiatric contraindication
Independent catch: CNS axis.
plecanatide pediatric
boxed warning under 6
GC-C uroguanylin analog; C4-C12 and C7-C15 disulfides
v8.4 addition: second independent pediatric GC-C dehydration control.
linaclotide pediatric
boxed warning under 2
GC-C guanylin analog; three-disulfide secretagogue
Independent catch: GI axis. Adult linaclotide remains an approved control.
caspofungin
boxed warning hepatic AEs
Echinocandin macrolactam plus C16 acyl chain
Independent catch: hepatic axis.
pasireotide
boxed warning hyperglycemia
Somatostatin-family macrolactam, severe SSTR metabolic context
Independent catch: metabolic off-target axis.
lepirudin
concern-bearing withdrawal
Hirudin-like thrombin inhibitor; antibody/anaphylactoid concern
v8.5 closure: commercial withdrawal stays positive, label concern stays visible.
GLP-1(7-17) truncation
synthetic negative control
10-aa fragment
Independent catch: Lyapunov length floor for Class B GPCR engagement.
octreotide / desmopressin / approved controls
approved outside glucose axis
Routed to declared Lyapunov axis or scored safety-only
Target discrimination is no longer counted as a safety win.
# v8.4 addition: plecanatide pediatric boxed-warning row
{ "name": "plecanatide_pediatric_boxed_warning",
"outcome": "pediatric_approved_with_boxed_warning",
"sequence": "NDECELCVNVACTGCL",
"structuredModifications": [
{"kind": "cyclization", "form": "disulfide", "residues": [4, 12]},
{"kind": "cyclization", "form": "disulfide", "residues": [7, 15]}
],
"populationContext": {"ageBand": "under_6"},
"endpointContext": "TRULANCE boxed warning: serious dehydration" }
gi_tolerability_score = 0.48 > threshold 0.45
= baseline_class_b_nausea 0.18
+ pediatric_gc_c_dehydration_warning 0.18
+ compact GC-C secretagogue context
# v8.5 taxonomy closure: lepirudin concern-bearing withdrawal
benchmark label: approved_then_withdrawn_with_documented_concern
reference gate verdict: PASS_with_documented_concern
reason: FDA/EMA anti-hirudin antibody + anaphylactoid evidence
withdrawal context: EMA commercial withdrawal, not safety-drivenCurrent PeptCheck v1.9 partitions
Calibration
n=27 · TP 24 · TN 3 · FP 0 · FN 0
100.0%
Held-out validation
n=29 · TP 19 · TN 10 · FP 0 · FN 0
100.0%
Full benchmark
n=56 · TP 43 · TN 13 · FP 0 · FN 0
100.0%
Pediatric sub-matrix
n=2 · TP 0 · TN 2 · FP 0 · FN 0
100.0%
The held-out set includes broad-target approvals, boxed-warning approvals, and failed clinical programs. Endogenous references and ambiguous discontinuations are reported separately instead of being forced into the confusion matrix.
Agreement progression
Lyapunov only (v1, raw)
n=9 · TP 5 · TN 0 · FP 3 · FN 1
55.6%
+ length floor (v2)
n=9 · TP 5 · TN 1 · FP 2 · FN 1
66.7%
+ immunogenicity (v3, n=8)
n=8 · TP 5 · TN 2 · FP 0 · FN 1
87.5%
+ cardiac + GI + calibration (v4)
n=27 · TP 24 · TN 3 · FP 0 · FN 0
100.0%
+ renal + hepatic + CNS, first held-out (v5)
n=37 · TP 30 · TN 7 · FP 0 · FN 0
100.0%
+ multi-axis dispatch, honest re-counting (v6)
n=37 · TP 30 · TN 3 · FP 3 · FN 1
89.2%
+ context-aware safety (v7)
n=39 · TP 30 · TN 7 · FP 1 · FN 1
94.9%
+ expanded public peptide controls (v8)
n=51 · TP 37 · TN 9 · FP 3 · FN 2
90.2%
+ HONEST_GAPS closure (v8.3)
n=51 · TP 38 · TN 12 · FP 0 · FN 1
98.0%
+ plecanatide pediatric control (v8.4)
n=52 · TP 38 · TN 13 · FP 0 · FN 1
98.1%
+ lepirudin concern taxonomy (v8.5)
n=52 · TP 39 · TN 13 · FP 0 · FN 0
100.0%
+ noncanonical positive controls (v8.6 / v1.9)
n=56 · TP 43 · TN 13 · FP 0 · FN 0
100.0%
The visible dip at v6 is intentional: approved non-glucose peptide drugs stopped being counted as target-discrimination wins and were routed to their declared axis or scored safety-only. v8.3 through v8.6 close gaps through taxonomy, source-backed context, and structural class biology, not scalar threshold movement.
Independent adverse-signal catches
Lyapunov
1
GLP-1 truncation
Immunogenicity
1
taspoglutide
GI
2
plecanatide pediatric, linaclotide pediatric
Renal
3
nesiritide, anaritide, ularitide
Hepatic
1
caspofungin
CNS
1
ziconotide
Metabolic
1
pasireotide
Cardiac
0
no standalone adverse-signal catch yet
Mechanism-fit
0
no standalone adverse-signal catch yet
Eleven separated gates
Closed-loop stability and off-loop safety are separate biological questions. The reference gate keeps four Lyapunov axes separate from seven transverse safety axes so every refusal has a visible cause and every pass remains claim-bounded.
- Lyapunov — glucose, calcium-lowering, calcium-raising, and BP-raising controller stability.
- Safety — immunogenicity, cardiac, GI, renal, hepatic, CNS, and metabolic off-target scoring.
- Mechanism-fit — weak perturbation evidence is carried as a protocol-level check instead of being hidden inside a sequence score.
Verdict robustness · perturbation scan
44/60
robust verdicts
16/60
brittle · 7 pass · 9 fail
octreotide
PASS · margin +0.03
no single edit flips it
Knife-edge pass: 0.27 vs 0.30 metabolic threshold. Correct, but balanced on the margin.
tirzepatide
PASS · margin +0.05
8 substitutions · 1 modification drop
Approved drug whose pass is sequence-sensitive — the scan surfaces it for review.
pasireotide
fail · margin -0.07
6 substitutions · drop the macrolactam
Correct refusal, but it hinges on two annotations: a cysteine or losing the ring flips it.
Every verdict now reports how far the input must move to flip it: the signed threshold margin, plus an exhaustive scan of single-residue substitutions and modification drops. A verdict is brittle if it sits within 0.04 of its threshold or any single edit flips it. No statistics, no fitted dynamics — deterministic finite enumeration over a declared neighborhood, the same shape the Lean layer can attest to.
Machine-checked formal receipts
7 / 7
safety axes reflected into Lean 4
60 / 60
verdicts proven per reflected axis
All seven safety axes are reflected into Lean 4. On every axis, every PeptCheck verdict is proven by
native_decide to match the audited scorer — rebuilt in CI, not asserted. Three (metabolic, immunogenicity, CNS) prove the exact score in integer arithmetic; the four with continuous terms (cardiac, renal, hepatic, GI) prove the verdict via exact integer inequalities. Marquee rejections carry formal robustness guarantees: pasireotide (metabolic, 6 flipping edits), ecallantide (anaphylaxis-Kunitz, provably robust), ziconotide (CNS), caspofungin (hepatic), nesiritide (renal), and ulimorelin (motilin cardiac).Reproduce:
lake build in Packages/PathwayLean re-checks every receipt. Source: PathwayLean/Examples/SafetyAxis/*Reflection.lean.Honesty: PeptCheck v1.9 is still small: 60 entries, 56 scored after endogenous references and ambiguous/discontinued rows are reported separately. The reference gate has 43 true positives, 13 true negatives, zero false positives, and zero false negatives. Lepirudin is resolved by explicit taxonomy: a commercial withdrawal can remain positive while anti-hirudin antibody/anaphylactoid evidence remains a documented concern. Source artifacts:
experiments/peptcheck-v1/ and experiments/lyapunov-prototype/benchmark/. Every verdict is reproducible by running python3 experiments/peptcheck-v1/runner.py, and its robustness by running python3 experiments/lyapunov-prototype/perturbation_robustness.py.More on proof
Related on this track
Mechanism verification
Pathway hypotheses, Swift checks, Lean receipts.
Combination controllers
Lean-verified cross-domain combinations.
Pathway Walk
visionOS proof topology.
Why rail
Inspectable evidence for candidate decisions.
Evidence tutor
Retrieval-grounded peptide reasoning.
In-silico lab
Assessment matrix and rejection gates.
TensFormer
Typed world-model spine.
← Back to Proof index
All sections on the proof track.