selected researchall 12 →
- 2026-09-25 — agents / formal verification 25 bugs in free-threaded CPython, found by agents Agents confirmed 25 bugs in CPython’s free-threaded build, 18 with no earlier report found in the tracker search. Of five reports I filed upstream, two now have fixes merged into CPython main. TLAPS and Lean proofs checked a locking model; replays of real runs showed five places CPython departs from it.
-
2026-09-27 — agents / formal verification
Agents turned a one-kernel Lean proof into a checker that certified 25 PyTorch kernels
One Lean theorem and a small checker certified 32-bit size arguments for 25 torch.compile kernels: 15 of 35 development cases and 10 of 24 held out, each proof bound to the live compilation’s guards. Two of nine tuned kernels got faster.
first experiment, one kernel: A Lean proof let agents cut a compiled PyTorch workload’s runtime by 26%
- 2026-10-23 — interp / patching Agents traced a lookup pathway in Qwen3 Agents traced how Qwen3 looks up the value for a named item: three stages, each carried by a few attention heads. Six head locations found in Qwen3-0.6B were fixed in advance and tested in Qwen3-1.7B, where a separate search had found the other two stages. Interventions there moved the answer preference in the predicted direction on 92.2–100% of held-out prompts, and the transfer test passed every registered gate.
-
2026-10-18 — interp / probes
What Llama’s internal signals reveal about factual accuracy
On 742 held-out FActScore claims, a layer-19 probe on Llama 3.1 8B reaches AUROC 0.802, against 0.735 for P(True) and 0.740 for subject popularity, though no clear advantage over popularity is detected once whole biographies are resampled. Within biographies it keeps a signal after position controls and, in an exploratory test, adds to P(True). A preregistered decomposition attributes most of its direct signal to attention heads.
initial study: Testing internal signals for factual accuracy in legal answers and biographies
- 2026-10-05 — agents / formal verification Agents reused proofs of OpenSSL routines across three callers Agents verified three experimental x86-64 callers in HOL Light by applying machine-checked contracts for two unchanged Debian OpenSSL routines through their actual linkage, instead of re-deriving the routines in each caller’s proof. The held-out caller missed its three-hour cap, then completed in a separately recorded successor.
selected softwareall 30 →
-
A Dafny-verified application core that a coding agent builds an application around, with a judge that says which properties of the result are proved, model-checked, tested, or awaiting human review. Research prototype.
-
The Hacker News front page, rendered by a Lean 4 program proven to render every API input correctly and redesigned every night by an LLM loop that ships without human review. Layout and accessibility are checked per release, never called proven.
-
Make one TypeScript function faster and see exactly how much of “it still does the same thing” was checked: compile, purity, differential tests, a bounded Z3 search, a benchmark, then a Lean 4 proof against an agreed spec. In the launch campaign, 3 of 130 candidate rewrites were accepted with a proof.
-
Ask a question of a spreadsheet export. A model drafts the calculation and the checks it must pass, you approve the checks, and only an answer that clears a strict TypeScript compiler, unit and property tests, and purity and time-limit gates is shown. Also a CLI and GitHub Action that certify TypeScript from any source.
-
A Claude Code skill that writes a multi-agent workflow script, runs it on Codex agents instead of Claude subagents, and shows the run as a live map. Agents edit files without asking unless the run is read-only.
-
A Claude Code mod that puts a live agent dashboard in your terminal: context and cost, every permission check, your subagents as cards or swimlanes. It only watches.
-
Train a small chatbot from scratch on Apple Silicon, from tokenizer training to a chat interface.
Why I built it: I wanted to train a chatbot from scratch on my MacBook without touching PyTorch or a cloud GPU.
model adapters
-
Random-choice adapter
A Qwen adapter for experiments with fixed-list sampling behavior.
-
Panel-reasoning adapter
The post-MATH Qwen adapter from the exploratory accuracy and completion-length comparison.
contact
I’m interested in replicating LLM experiments and building useful open-source tools. Get in touch about research ideas, corrections, or collaboration.
For bugs and code, open an issue on the repo in question.