GPU systems engineer focused on LLM inference, CUDA kernels and compilers. Based in Vancouver.

Email · LinkedIn

I'm building FindTensor, an experimental compiler and runtime for LLM inference in Rust, C++ and Python. Previously, I worked with Tor Aamodt at UBC on GPU architecture simulation.

• SOL-ExecBench B200 kernels: CUDA C++, CuTe DSL and Triton kernels, with source packages and local B200 validation reports. Local scores are estimates, not confirmed leaderboard results.
• KernelIndex: A GPU performance index that compares matching workloads and links results to their source, environment and benchmark protocol. Imported results are labeled reported until independently reproduced by the index.
• Command A+ vLLM benchmarks: A serving study on two H100s, covering prefill, decode, KV-cache capacity, CUDA graphs and tuning, with raw logs and a report.
• H100 serving estimator: Estimates GPU-seconds per request from 91 published Command A+ runs, with held-out evaluation. Its accuracy and interval coverage depend on the workload; a simpler baseline wins on the unseen serving configuration.
• SmolLM2 CPU conformance: Separate full-sequence and incremental KV-cache implementations checked against Transformers across 48 numerical cases. A correctness study for one model revision on CPU.
• Tensor parallel reference: A CPU decoder block across 1, 2 and 4 worker processes, with numerical checks, exact wire accounting and 96 fault-injection cases.

CAIRN is an experimental systems language for CPU and NVIDIA GPU programs, designed to be written by AI agents. It compiles to C++20 and CUDA. The checker tracks ownership, task leases, effects and permitted parallel access patterns, with diagnostics that identify conflicts and suggest repairs. The repository includes the compiler, runtime, agent tools and benchmarks. Its Lean models cover specific rules; the compiler itself is not formally verified.

• The Work a Verifier Needs: Certified output-head decisions and speculative-verification experiments on Qwen3.5-4B in SGLang on GH200. Includes a low-precision head with selective re-scoring and fallback to the stock kernel, Lean proofs for decision logic, and serving measurements across concurrency levels.
• StateCut: Exact-reference attention certificates and persistent decoder-state writes, with scoped Lean proofs and GH200 experiments. Pretrained attention acceleration and equivalence to a deployed backend remain open.
• Contracted moment kernels: Moment summaries for certifying attention outputs, combining real-arithmetic proofs, exact-rational checks and CUDA experiments. The measured full pipeline remains slower than fused dense attention.
• Witness-CL: Online executable memory for SQL agents, using delayed corroboration and replayable memory transitions. The implementation and development studies are public; the intended confirmatory efficacy claim is not established.
• SQ learning and dimension complexity: A manuscript on the separation between distribution-independent statistical-query learning and dimension complexity, with reproducible experiments and supporting Lean lemmas. The complete paper is not formalized.
• Memory return in quantum machines: A manuscript on repeated quantum transformations and memory reuse, with written proofs, exact finite checks, certified figure data and a partial Lean formalization. It has not yet been peer reviewed.
• Lean formalizations: Formal models and proof development for Erdős problems in Lean 4 and mathlib. The workspace includes unfinished conjecture statements.

• FlashInfer: My SM120 dispatch diagnostics and configuration API were incorporated upstream. My fix for unrouted expert IDs in SM12x fused MoE was merged. I also reported and reproduced an FP8 KV calibration bug that was fixed upstream. Further attention, GEMM, sampling and MoE work is in open PRs.
• NVIDIA CCCL / CUB: Merged execution-environment support for DeviceMergeSort, DeviceMerge and DeviceMemcpy. Further CUB and Thrust changes are under review.
• SGLang: Open PRs for snapshot-free GDN verification, speculative planning from host-known lengths and other serving fixes.
• GPU MODE and torchcomms: Open PRs for QR benchmark input and stream checks and building and shipping the uniflow Python extension.
• Triton: A proposed SM120 FP8 dot rewrite using block-scaled MMA, closed without merge.
• Accel-Sim: A merged Ubuntu 24.04 / CUDA 13.1 container update, an open GPU application compatibility PR, and a GPGPU-Sim CUDA 13 proposal closed without merge.