Research approach
Make the boundaries
part of the work.
A useful specification connects the scientific question to the computation. A useful verification report says exactly where its evidence stops.
Begin with the scientific question
Identify the comparison, the experimental unit and the data available. Record choices that could change the interpretation.
For a single-cell counts matrix, the initial convention is genes in rows and cells in columns. Sample membership and study design require separate metadata.
Synthetic counts · 3 genes × 4 cells
From a matrix to a traceable result.
Read a gene across the cells. Follow its counts into a simple summary, keeping the row identity attached.
| Gene | Cell 1 | Cell 2 | Cell 3 | Cell 4 |
|---|---|---|---|---|
| Gene A | 0 | 2 | 7 | 1 |
| Gene B | 4 | 0 | 1 | 3 |
| Gene C | 1 | 5 | 0 | 2 |
Metadata travels alongside. Sample, donor and condition labels require a separate record keyed to cell identifiers.
Gene A: one row, four observations
Counts per cell · shared scale: 0–8
0 + 2 + 7 + 1 = 10
Total: 10 counts · Nonzero in 3 of 4 cells.
Gene B: one row, four observations
Counts per cell · shared scale: 0–8
4 + 0 + 1 + 3 = 8
Total: 8 counts · Nonzero in 3 of 4 cells.
Gene C: one row, four observations
Counts per cell · shared scale: 0–8
1 + 5 + 0 + 2 = 8
Total: 8 counts · Nonzero in 3 of 4 cells.
What does this small result establish?
It describes the displayed counts: a sum and a count of nonzero entries. It is not a differential-expression result.
A zero count does not establish biological absence. Cells do not, by themselves, define independent biological replicates.
Invented data for explanation. This arithmetic does not model normalization, uncertainty, batch effects or a biological comparison.
Give each stage a contract
A contract describes required inputs and the properties of an output. It can include dimensions, provenance, contrast meaning and dependencies between stages.
Contracts are reviewed with the people who understand the intended analysis. Ambiguity is a finding to resolve before proof work.
Match evidence to the claim
Some questions need a test. Others benefit from a runtime check or a machine-checked proof. These forms of evidence can work together.
We are exploring AI-assisted construction of specifications and proofs. Proposed proofs must pass a proof checker; humans must review what the specification means.
Automating proof construction does not remove the need to examine assumptions, axioms or links to executable code.
Specification → model → execution
A precise claim needs a visible boundary.
Start with a sentence a scientist can review. Then separate its formal meaning from the program that runs.
“Grouping results for a report preserves the declared comparison family and its adjustments.”
- Membership: retain the family identity and full membership record.
- Binding: keep each adjusted value with its comparison.
- Presentation: change the display without silently changing the correction.
Formal scope
A model of regrouping
A proof could show that this operation preserves the specified properties for inputs covered by its assumptions.
The claim is about the formalized operation.
Execution scope
The actual analysis run
Parsers, Python or R code, numerical libraries and the runtime need their own connection to the model.
A model proof alone does not verify this run.
The missing link is an evidence obligation. Examples include a verified implementation or a checked translation, with their assumptions stated.
What must the evidence report make explicit?
- The exact property, covered code revision and supplied evidence.
- Unproved obligations and any assumptions linking the model to execution.
- Trusted components, such as arithmetic, libraries, compilers, proof-checker axioms and hardware.
- Scientific assumptions that the computational claim does not establish.
Conceptual example; no executable proof is supplied. Specification review, model validity and biological interpretation remain separate responsibilities.
Report what is covered
A scoped report should name the property, code revision, evidence, trusted components and known gaps. It should make unproved obligations easy to find.
A verified component can still be used incorrectly. Composition requires checking that one stage’s output satisfies the next stage’s input contract.
Open methods, project-specific work
We intend to release reusable tools and examples as open source. Paid project work would cover scientific analysis, adaptation, review and targeted verification.
There is no released general verification platform yet. See what is being developed.