Research, with the logs attached.
We study how to make AI systems checkable: what a model computed, what an agent did, and how much of either can be proven. Every result ships with its code, its raw logs and a list of what it does not show.
Notes and papers
Short, written for a technical reader, and linked to the repository that backs each number.
Provable AI inference on a gaming GPU: what fits in 16 GB, and what it does not prove
Twelve patches, one store-bought graphics card, and 770 proofs accepted by a verifier we never touched.
Research note 02Allow or block, with proof: a guard's decision about one exact agent action
A guard we trained ourselves, 40 proved decisions, 12 forgeries caught, and one honest mistake that is still graded “proven”.
Paper · code ↗Every memory needs a WHY: learning from what happened next
An experience deserves to shape future behaviour when keeping it improves later decisions. A controlled simulation, with its negative result reported.
Programmes
Three lines of work that share one question: when an AI system says something happened, what is the evidence, and how strong is it?
Proofs of inference on consumer GPUs
We ported Anthropic's open-source FlashProve prover from a datacenter H100 to a 16 GB gaming card, then measured what fits: a real tiny model, layers at Llama 4 Maverick's width, and full batches of 64 requests.
Graded evidence for agents
Receipts for an agent's actions that state a level for every claim, from observed to computation-proven, and a checker that recomputes each level instead of trusting the issuer.
Learning from what happened next
Which experiences should change an agent's future behaviour? Our first experiment tested consequence-aware memory in a controlled simulation. It does not establish transfer to language-model agents.
Open source
Run it yourself. The repositories hold the patches, the scripts and the logs with their checksums; the proofs are attached as a release.
flashprove-consumer-gpu
The 12-patch port of FlashProve's CUDA prover to an RTX 5070 Ti, with every run's logs, the tamper tests, the scaling study and a replication template.
Apache-2.0 · Checker, receipts, proofsgraded-agent-evidence
The receipt format, the independent checker, the public encoder and two receipt bundles, with the 12 proofs behind them in the release. One command re-checks every receipt.
Code, results, papermemory-experiment
Memory Experiment 1: eighteen policies, the confirmatory seeds, and the draft paper “Every Memory Needs a WHY”.
Method
How we keep ourselves honest. These rules come from our research charter and apply to every proving and evidence experiment.
One experiment at a time
Each has a success condition and a stop condition, stated before it runs. A failed conversion check or a rejected proof stops the work; it is never patched around.
The judge is never ours
Proofs are accepted only by the unmodified upstream verifier, built from a separate pristine checkout. We never edit a source file to change a result.
Raw logs, kept
Commands, full logs, exit codes, hashes and hardware are stored with every run. Published numbers trace to a log line and a checksum.
Limits come first
Every write-up has a section on what it does not show. We do not say “first” without a documented prior-art search, and we never show a bare “verified”.
Have a GPU? Check us.
The single most useful contribution is running our port on your own card, especially another consumer GPU or native Linux.