Software

This page describes my past and present open source academic software projects.

Mellea

I currently lead development of Mellea. Mellea is an inference-time stack for building LLM-powered agentic software. Mellea is designed to support development of robust agents and to enable model/software co-design.

Amazon CodeWhisperer

CodeWhisperer is an AI code generator developed by a large team at AWS (of which I was a member). One of Amazon's first AI products to enter General Availability, CodeWhisperer was highlighted in two letters to shareholders as proof of Amazon's leadership in the AI space.

KeYmaera X

I am a primary developer of KeYmaera X, a theorem prover for hybrid systems. Hybrid systems are a type of dynamical system with both continuous dynamics (differential equations) and discrete dynamics (imperative programs). These systems are often used to model systems in which the specification of a piece of softwawre is intimately related to a continuous phenomenon; for example, KeYmaera X has been used to verify models of self-driving cars, aircraft collision avoidance protocols, and surgical robots.

KeYmaera X website | GitHub repo |

IBM Verifiably Safe Reinforcement Learning Framework

A framework for applying formal methods to end-to-end reinforcement learning systems.

VSRL Github repo

Teaching tools

A Type System for String Analysis

I developed a type system that helps reduce errors in security-critical input validation logic as a type system extension in Cyrus Omar's Ace programming language. The source code is available on GitHub and the type system is described in two award winning papers (see Publications). I also made some small contributions to Ace itself.

An OpenCL Type Checker

I wrote a type checker for v. 1.0.29 of the OpenCL specification in Python. My original plan was to use this library extend Ace with support for high-level GPU programming constructs, but I've since moved on to other projects. The source code is available on GitHub.

Formal Proofs

Civics / Fun / Random