Research engineering portfolio

Proofs, benchmarks, and systems with evidence close to the claim.

I am a mathematics undergraduate at the University of Washington. I build proof-oriented software, reproducible benchmark harnesses, certificate-shaped runtime tools, and data systems where the public claim can be checked against source, runs, and artifacts.

View projects GitHub

About

I turn mathematical ideas into software that can be checked.

My strongest projects sit between proof, algorithm design, and pragmatic engineering. I care about exact input formats, failure modes, reproducible commands, and clear boundaries around what has and has not been verified.

Current work includes Lean 4 formalization, normal forms over Euclidean and PID-like settings, sparse matrix benchmarking, certificate-oriented runtime monitoring, and data workflows where assumptions need to stay visible.

Lean 4 / mathlib Rust Python C++ Formal verification HPC benchmarking Algorithm design Reproducibility

Selected Projects

Six builds with traceable evidence paths.

Each project card says what exists, what it proves or measures, and where the current claim boundary stops.

HPC benchmark harness

SparseBench

A C++ CPU sparse-matrix benchmark harness that reads Matrix Market inputs, converts coordinate data into CSR, runs serial and OpenMP SpMV, and writes CSV timing, throughput, and checksum fields.

The public case study is deliberately scoped: Hyak job 34825519 covers a 96-core mem2x run, and job 34852262 covers a 32-core Eigen comparison.

C++ OpenMP Hyak SuiteSparse
Read the case study

Model evaluation pipeline

FlashDistill

A local Python/uv data factory for pre-Hyak math distillation experiments, keeping generation, normalization, verification, SFT packing, cost logs, reports, and data manifests in one CLI-driven workflow.

It stops at reproducible local gates and a Hyak handoff runbook. It produces JSONL artifacts and manifest hashes; it does not claim submitted GPU training runs.

Python uv LLM evals Schemas
Local artifact / public release pending

Agent safety infrastructure

Proof-Carrying Monitor

A Rust workspace with Lean 4 specifications around a certificate-oriented runtime monitor. The gRPC schemas model decisions that carry either an allow certificate or a deny witness, plus policy-diff evidence for review.

Lean-side soundness work and FFI integration remain conservative; the executable path currently relies on Rust checker machinery and protobuf contracts.

Rust Lean 4 gRPC Security
Open GitHub

Civic data analysis

Seattle Transit Restoration

A Python analysis repo for schedule-based Seattle transit restoration work using King County Metro GTFS, archived Transitland GTFS, NOAA weather data, and ACS demographics.

The optimization claim is static-data connectivity analysis: routing modules, candidate generation, and MIP optimization. GTFS-RT scripts exist, but they are not the basis of the restoration result claims here.

Python Data analysis Civic tech
Open GitHub

Image tooling

agentic-color

A FastAPI + React/Vite MVP for image color variants. The backend accepts an upload and returns a schema-backed ImageAnalysis object with three StyleVariant presets.

The useful part is editability: each variant has explicit tone and color parameters plus a preview card. The analyzer still uses MVP/mock variants, so it is not described as a production ML grader.

Python Computer vision Image editing
Open GitHub

IoT case study

All-in-One Air Quality Monitor

A compact indoor monitor built with ESP32-C3, SEN55, onboard OLED, ESPHome firmware, and Home Assistant integration for PM, temperature, humidity, VOC, and NOx trend data.

The case study records the parts list, wiring table, firmware YAML, display behavior, and the black-screen debugging path that found the board's actual I2C pins.

ESP32 ESPHome Sensors
Read the case study

More Work

Smaller builds, forks, and workbenches.

These artifacts are narrower than the selected projects: useful for showing tools I have built around, studied through, or used as reference contexts.

matrixcalc Gaussian-elimination solver with partial pivoting, rectangular-system handling, and tests for unique, inconsistent, and infinite-solution cases. Matrix-Cam CLI prototype that turns a live webcam feed into density-mapped ASCII output in a green terminal style. Celestial-Chase R data-storytelling around near-Earth comet orbital elements and meteorite landing records. mathlib4 fork Lean/mathlib workbench for theorem-proving experiments, local reference checks, and learning from upstream library structure. lean-normal-forms Lean 4 normal-form workbench with a completed HNF layer, Smith-form specification boundaries, and ongoing PID bridge work. leanprover/cslib Canonical Lean Computer Science Library context for formalizing CS theories, APIs, and certified-software building blocks.

Writing

Recent notes and case studies.

I use these posts to record the decision trail: what I tried, what evidence counted, what failed, and which claims should stay out of scope.

Apr 26, 2026 - Systems Building a Reproducible Sparse Matrix Benchmark on Hyak How tiny Matrix Market fixtures grew into Hyak Slurm gates, SuiteSparse manifests, 96-core scaling evidence, and a scoped Eigen comparison. Dec 06, 2025 - DIY Building an All-in-One Air Quality Monitor for roughly $30 A practical ESP32-C3 + SEN55 build: wiring, ESPHome YAML, Home Assistant integration, and the I2C-pin mistake that kept the display black.