Make it inspectable.
Keep the source, specifications, and experiment records close to the result. A claim should have somewhere to lead.
An independent software organization
Software with
something
to prove.
Formal verification. Local intelligence. Traceable systems.
Four projects, connected by a belief that good software should stand up to a closer look.
Built in the open. Measured in the details.Discover the collection
01 — The collection
Different disciplines.
A shared standard.
From a mathematical contract to the system underneath it. Each project explores a different part of the same question: what can we actually trust?
01 / Formal verification
+
t-proof-engine
A specification language that checks programs across seven proof systems, and challenges every result with a deliberately broken twin.
7 proof systemsExplore project
02 / Local intelligence
+
dawnr
An offline assistant for documents, files, and computer tasks, with reviewable changes, sandboxed commands, and a path to formally checked code.
Local by defaultExplore project
03 / Model research
+
locallm
A transformer training toolkit covering tokenization, training, exact checkpoint resumption, and inference, with an inspectable experimental record.
92.9M parameter modelExplore project
04 / System provenance
+
tup
A Linux From Scratch build driven by recorded commands, hashed source archives, explicit deviations, and independent boot witnesses.
139 build-page receiptsExplore project
Public source, documented results, explicit limitations. See each repository for its license.
02 — The connections
Every link
has a purpose.
These projects grew together. Explore how the assistant, its learning tools, its verifier, and its foundation relate.
01 / The verification layer
Programs with a precise contract. Proofs with a second check.
The checking layer behind dawnr. A model can propose a program; the proof systems decide whether it meets its stated contract. The same engine also checks standalone math and flight-code routines.
Inside t-proof-engine02 / The assistant layer
Local assistance, with a record of what actually happened.
The place the projects meet. dawnr uses the proof engine to check generated programs and connects the model research to practical work on a computer. It carries a pinned engine version so its results remain traceable.
Inside dawnr03 / The learning layer
The whole training path, from data to inference.
The model research layer. locallm investigates training from scratch, while the proof engine provides a demanding way to evaluate generated code. Its record includes both successful engineering and experiments that did not transfer.
Inside locallm04 / The foundation layer
Trace the finished system back to the bytes it was built from.
The foundation. A verifier depends on the software underneath it. tup extends the evidence trail toward the operating system: which source bytes were used, which commands ran, and what the released image actually did.
Inside tupA closer look / t-proof-engine
The work
behind the words.
In the published math showcase, each solution is checked against a specification, challenged with a broken twin, and run against the judge’s stored outputs.
Read the complete resultsUVa math showcaseRecorded 08 Oct 2026
23problems proved in
at least one system
at least one system
179,549judge-output
lines matched
lines matched
3 / 23problems proved
in all seven systems
in all seven systems
Proof coverage varies by problem. Some specifications encode mathematical models. The full record names the scope and limitations.
03 — Our approach
Let the details
do the talking.
Tup brings independent software research into one place. The aim is useful tools with enough evidence for someone else to inspect, question, and build on.
Measure the claim.
State what was tested, under which conditions, and what the result establishes. A passing example is only the beginning.
Keep the misses.
Failed predictions and corrected results belong in the record. They tell us where the next useful question starts.
04 — Get in touch
Good ideas deserve
good company.
Questions about the projects, research, or a possible collaboration?