Machine-Checked Formalization of a Functional Genomics Study

We present an end-to-end formal replication of Chan et al., “WRN helicase is a synthetic lethal target in microsatellite unstable cancers” (Nature 568:551–556, 2019), in the Eigenius typed knowledge store. Starting from content-addressed source data, two verification institutions operate over a shared 10-layer chain: a statistics institution re-evaluates the study’s statistical tests from raw sample sets, and a justification institution checks the study’s domain conclusions in a dependent type-theory kernel. Each conclusion is represented as an explicit proof term that applies declared analysis plans to observed datasets and composes the resulting statistical propositions through typed domain rules. Every premise carries one of four warrant grades (recomputed, wrapped-runtime, declared, or linked-external), making its evidentiary basis and transitive assumption support queryable. Across the complete chain, all 12 containerized R analyses execute and 55 of 55 verdicts hold (22 native statistical analysis plans and 33 domain conclusions). Of 16 logged recomputation findings, 15 reproduce or confirm the published results and one identifies a benign sample-size discrepancy (𝑛 = 51 complete pairs in the data versus 𝑛 = 54 reported in the text, with Spearman 𝜌 =−0.74 unchanged). Three of the reproductions also expose modeling assumptions that are implicit in the published text: a choice between technical-well and biological-guide replication units in the competition-assay ANOVA(𝑃 =2.74×10−19 vs.𝑃 = 2.15×10−6, with the biological conclusion holding under both), 𝑇𝑃53-status stratification in single-cell immunofluorescence, and a saturation-ceiling convention for pan-nuclear cells in 𝛾H2AXfoci counts where dropping saturated cells reverses the sign of the interaction. All quantitative analysis classes in the paper are executed, from genome-wide limma differential-dependency models over a 187 MB matrix and paralogue co-loss regressions over a 1.6GB omics bundle to five single-cell microscopy models covering 533,137 cells, and the paper’s cited literature enters the proofs as CiTO-typed citation premises.