Work · CV · Website · Email · GPG · ORCID
I work on technical AI assurance, establishing verifiable claims about what a model actually did, when the operator, the evaluator, or the model itself may not be trusted. This spans cryptography, systems, evaluations, and mathematics, precisely the shape of my background. I'm a MARS V fellow with the Cambridge AI Safety Hub, mentored by James Petrie (FLI), and a graduate student in computer science and engineering at DTU; previously CS and mathematics at Brown.
I am open to full-time research and research-engineering positions worldwide.
Verifiable LLM inference (MARS V, ongoing) — zero-knowledge proofs for cryptographic verification of claims about LLM training, inference, and deployment. My contributions are merged upstream into JamesPetrie/VerInf: a dry-run profiler with a manifest contract, cost model, execution DAG, and partition scorecard, plus cost-model corrections matching the paper's analysis (merged PRs). Currently porting the verifier from single-chip to multi-GPU and working on mathematical techniques for further optimization. Technical write-up expected Q4 2026, for review and publication.
Frontier-model evaluation and red-teaming — reasoning evaluation, red-teaming, RL environments, and evaluation research under contract. What I can discuss publicly is limited.
proof-broker — brokers proof goals from Lean 4 and Rocq through a shared IR to SMT solvers, ATPs, and LLM provers, then verifies returned certificates and lifts proof terms back to the home system. The verifier is strictly fail-closed: it refutes the negated goal, checking for smuggled axioms rather than trusting prover output.
icd_embeddings — order-invariant ICD-10-CM embeddings for 30-day readmission and post-discharge mortality, trained on the Nationwide Readmissions Database. Our manuscript is under review at JAMIA.
Systems and performance: pmacs (Rust-cored, Lua-scripted editor), kyber-simd-profiling (SIMD post-quantum cryptography, cross-ISA), LeVCS (federated version control with signed authority chains), the Weenix kernel, and a TCP/IP stack written from scratch. Mathematics: two graph-theory preprints, on tree-ball geometry and growing-radius domination. Research engineering: neuropose, 3D kinematics in Liqi Shu's lab at Brown Neurology.
Rust, Python, C/C++, OCaml, Haskell, Go. Cryptography, distributed systems and HPC, formal methods, ML evaluation.
I have worked with many other tools in the past to various extents, and the above list is certainly not exhaustive.
Most of my development is being moved to my Forgejo instance, mirrored here. Current is what I'm actually working on this month, while Vita is the most formal record.