Current

I own profiling and scale-out for VerInf, which develops proofs of language-model inference that mutually distrustful parties can check on their own hardware. The profiler, weight split, caches, bridge integration, and subsequent constraint repairs are merged upstream (pull requests 21–25). Archived Maverick proofs lack complete model binding; draft pull request 31 proposes a repair, with its GPU gate, new enrollment, and re-proof still outstanding. Weight splitting has passed proof-byte equivalence and independent Rust verification on one GPU; multi-device execution remains in progress. The experimental weight bridge's intended privacy protection and its profiler cost model remain unfinished. I work on this as a MARS V fellow, mentored by James Petrie (FLI).

Proof Broker routes Lean 4 and Rocq goals to untrusted solvers and LLMs, checking evidence before kernel-verified closure. R4 closed 19/19 targeted VerInf obligations; R5 consolidated spec v1.1. R6, an audited live-model evaluation on 15 VerInf obligations, is closed: all 80 certificate-feasible slots returned a verified witness, and proofs covered 6 of 15 obligations (48 of 88 slots), unchanged across eight draws and two more than the deterministic baseline. Posing goals and turning certificates into proofs, not finding them, was the constraint. The evaluation ran under two post-collection amendments, both published with it.

Mathematics preprint proving a square-root cop bound for actual stopping-rule degree-reduction towers over bases satisfying fixed multistage expansion and accessibility hypotheses. Port placement and synchronized guarding remove the cloud-order factor. The follow-up gives an explicit whole-tower lower-transfer proof and an exact criterion for guarding adjacent-cloud unions. The remaining full-ball Hall requirement still blocks the proposed shrinking-base route to Meyniel's conjecture.

Mathematics preprint determining the bounded annealed critical window for growing-radius domination in random regular graphs — its universal scaling function and a scalar coupon-root asymptotic expansion. A bounded literature pass closed 5 September 2026, with the Duckworth–Mans attribution corrected and the relative overlap estimate completed. Typical existence in the growing-radius window remains open. A separate timed cloud-guarding paper now resolves the cloud-order loss in the conditional multistage pursuit transfer.

Mathematics preprint on path-tube persistence, exhaustive static coverage, conditional sampling thresholds, and information loss in d-regular tree-balls. Audit corrections landed 5 September 2026: the root-degree statement corrected, admissible-root coverage clarified with a counterexample to residual domination.

Reinforcement-learning agent under active development on top of arcana, a Rust rules engine built as the substrate for it; expected late 2026.

Compute is available at DTU for the duration of my enrollment; paused because it is not a current priority rather than for want of hardware.

Under review at JAMIA (Journal of the American Medical Informatics Association), after moving from JAMA Network Open. Calculator deployed at levineuwirth.github.io/icd_embeddings.

v1.1.0 shipped with prebuilt binaries; 4476 tests across 120 suites since. Rust core and embedded Lua VM, split into a long-lived instance and thin TUI and GPU frontends that attach over a typed protocol and edit CRDT-backed buffers concurrently. An audit on 5 September 2026 put it a few dozen small changes short of a daily driver on both frontends.

A Python-successor language designed adversarially: statically inferred without annotations, no GIL, no MRO. Spec, reference machine, language server, and debugger exist, .levo files run, and 1061 tests across 182 suites hold the line — but with no I/O and no standard library it is still a conformance machine, not a runtime.

Wayland-targeted productivity and research shell, in daily use as my main environment, with project resume as the hero verb. Recent work adds a reading-library surface — paper records filled from OpenAlex, PDFs opened in place — and a live window over the daemon's state.

FOSS music-notation platform: a deterministic, CRDT-based score model whose LaTeX specification suite is the source of truth. Spec and editor tracks advancing in parallel.