I build agentic AI systems, RAG pipelines, and knowledge graphs that turn messy information into something a machine can actually reason about. Currently studying Computer Science & Mathematics at the University of Virginia, and interning on the AI Engineering team at BAE Systems.
A bit about my background, education, and the tools I reach for when building AI systems.
B.A. in Computer Science and Mathematics
From AI engineering at a defense & security company to research on formal verification and reproducible research infrastructure.
At BAE Systems I work on the Intelligence & Security Sector's AI Engineering team, where I'm building an AI-powered knowledge management platform that helps engineering teams make sense of hundreds of dense technical documents — turning scattered PDFs and specs into something searchable, structured, and reasoned over.
As a Research Assistant in the Hiprel Group, I work under Professor Wenxi Wang at the intersection of neuro-symbolic AI and formal methods — essentially asking whether LLMs can be trusted to write code that's not just plausible, but provably correct. Most of this work centers on the Verus Benchmark, which pairs Rust programs with machine-checkable formal specifications.
A mix of client work, hackathon builds, and research publications spanning RAG systems, applied AI, and formal verification.
Engineered a Retrieval-Augmented Generation platform that generates company history outlines in client-specific tones. Built a Hono API with Supabase storage for document ingestion and retrieval, and optimized embedding, chunking, and retrieval pipelines with vector databases and reranking to improve coherence and style alignment.
A full-stack web app that reads a restaurant menu and tells you what's actually safe to eat — built to solve the real problem of scanning a menu in a language you don't speak, or with allergies, and having no idea what's hiding in a dish.
"VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation" — a benchmark built to test whether LLMs can write code that's formally, mathematically verified as correct, not just code that happens to pass a few test cases. This work grew directly out of my Verus proof-analysis research with the Hiprel Group.
I'm starting to write about what I'm learning building agentic AI systems, RAG pipelines, and knowledge graphs. Here's what's in the works.
Notes on designing Agent-to-Agent workflows and grounding LLM output in a Neo4j knowledge graph.
What I'm learning analyzing LLM-generated Verus proofs for correctness across algorithmic domains.
A practical intro to graph-enhanced retrieval — why flat vector search isn't always enough.
New posts publishing soon — check back or follow along on GitHub.
Always happy to talk about AI engineering, research, or interesting problems. Reach out — I'd love to hear from you.