CS + Computational Math @ Penn State (Schreyer Honors) Application Developer Intern @IBM
I mostly work on ML, optimization, and formal verification. Recently I've been building a governance layer for AI coding agents: it figures out how much a given change should be trusted and attaches a signed receipt so you can check the decision later.
| Project | ||
|---|---|---|
| ◆ | Signetry | A change-control plane for coding agents. Any agent can open a PR; Signetry decides how much authority the change earned and signs the result with an Ed25519 receipt (in-toto / SLSA). It quarantines prompt-injection text on disk, runs an independent verifier, and does deterministic SAST across 7 languages. Ships as a kernel, a GitHub Action, a GitHub App, and editor plugins. |
| ◆ | Cauzon | Root-cause analysis for data incidents on DataHub. It walks the lineage upstream, finds the actual cause, and writes it back. |
| ◆ | TracePilot | A multi-agent router that learns from its own Arize Phoenix traces and reroutes away from tools that keep failing. |
| ◆ | Transformer × QAOA | IEEE NMITCON 2025 paper. A from-scratch PyTorch transformer with QAOA-optimized attention blocks. |
| ◆ | 5G-AKA verification (honors thesis, in progress) | Formal verification of the 5G-AKA auth protocol with SAT/SMT (Z3), an NL-to-CNF pipeline, and a Tamarin baseline. |
Plenty of people are making AI agents more capable. I'm more interested in whether you can trust what they do: keep the change inside a contract, have something the model can't override check it, and be able to prove afterward what happened. Signetry is that idea built out. The QAOA and 5G-AKA work comes from the same place, just applied to optimization and protocols.
- @IBM — generative AI on watsonx, and Watson services on OpenShift for clients.
- Before that — Lockheed Martin, reinforcement learning for threat assessment (85% success rate).
- Tools I reach for — PyTorch, Qiskit/QAOA, Z3/SMT, Coq/Rocq, and Python / C / Java / TypeScript.