Research-oriented software developer working across AI systems, GPU computing, formal methods, and scientific tooling.
I build experimental systems with an emphasis on explicit scope, reproducible evaluation, and technical documentation.
- contextdiet — quality checks for coding-agent context across AGENTS.md, CLAUDE.md, skills, and MCP configuration.
- ToposAI — experimental neuro-symbolic research library with a finite categorical/topos core and PyTorch research components.
- cuda-cic — experimental CUDA batch type-checking work for Lean 4/CIC proof terms.
- proof-perf-lab — performance experiments paired with explicit correctness checks and reproducible reporting.
- coherence-lab — certificate-producing normalization and equivalence for selected categorical coherence fragments.
- lean-proof-navigator — Mathlib declaration search, dependency exploration, and formalization navigation.
- Claims need provenance. Benchmarks should state hardware, commands, datasets, and comparison conditions.
- Optimization needs correctness. A speedup is useful only when behavior is preserved and checked.
- Research prototypes need scope. Experimental components should be documented as prototypes rather than production-complete systems.
- Reproducibility beats headline numbers. Raw evidence and repeatable procedures matter more than promotional wording.
- efficient AI inference and GPU execution
- formal reasoning and proof-assistant tooling
- graph and categorical structure
- reproducible performance engineering
- scientific software and research automation