Automated Reasoning Checks

I contributed to Automated Reasoning checks, a neurosymbolic guardrail for AI-driven workflows. It combines LLMs with formal verification to check that a model’s output complies with a policy, and large enterprises use it to prove the correctness of financial workflows. See the CAV 2026 paper for the approach.

AWS intent-driven networking

I have worked on various parts of the AWS intent-driven network control plane (AIDN), from building the intent infrastructure to working on a new routing protocol. I architected AIDN’s network compiler, which powers the control plane across AI/ML clusters as well as general datacenters. I also contributed to SIDR, a Rust link-state routing protocol for ultra-large datacenters, and led its correctness effort using model checking and property-based testing, which enabled an accelerated multi-datacenter rollout. More info available in this re:Invent presentation

Batfish

I continue contributing to Batfish, an open source tool for network configuration analysis. Batfish has broad use in the networking community, and has been adopted at AWS as well. I was the core developer for the routing simulation engine. These days mostly focused on closing vendor gaps and supporting users.

Past projects

Network Access Control

At AWS, I built a service for verifying network access control lists (ACLs) using formal methods.

AWS Reachability Analyzer

While at AWS, I briefly worked on a service that powered AWS reachability analyzer.

SDN Optimization Layer (SOL)

During my PhD at UNC, I explored the intersection of Software-Defined Networking (SDN) and global network optimization. In particular, I looked at how to efficiently write and execute SDN applications that try to perform optimal resource management (e.g., traffic engineering) in the SDN world. As a result, I ended up developing a library called SOL for expression and composition SDN resource-management applications.

Gremlin — microservice resilience testing

On an internship at IBM Research, I helped start a project for resiliency testing of microservice applications. We built an automated testing framework for stress-testing microservice applications and checking if they are resistant to failures.