research

Certificates that prove autonomous systems safe, and proofs a computer can check.

I build certificates that prove a controlled system stays safe or reaches its goal, and I make those proofs checkable by a computer.

A barrier function certifies safety; a control Lyapunov function certifies that a goal can be reached. Sum-of-squares (SOS) programming finds such certificates automatically as polynomials, but a single polynomial rarely covers all the states you care about. My work chains certificates into hierarchies that hand a system from one to the next, reuses one certificate for obstacles that move, and turns the solver's floating-point output into exact proofs that Lean 4 can check.

Three synthesis methods produce SOS certificates in floating point; exact repair turns them into rational certificates that Lean 4 checks. floating point exact ℚ Successive barriersstay safe Repulsive barriersavoid moving obstacles Successive CLFsreach the goal SOS programssolved numerically Exact repairrational arithmetic Lean 4machine-checked Three synthesis methods produce SOS certificates in floating point; exact repair turns them into rational certificates that Lean 4 checks. floating point exact ℚ Successivebarriers Repulsivebarriers SuccessiveCLFs SOS programssolved numerically Exact repairrational arithmetic Lean 4machine-checked
How the projects fit together. Each synthesis method produces SOS certificates in floating point (hollow dots); exact repair turns them into rational certificates (solid dots) that a proof assistant verifies. Select a box to open that project.

Successive barriers

HSCC 2025, with Sriram Sankaranarayanan

A polynomial barrier found by SOS certifies only a small safe region. Successive barriers add certificates level by level, and each new one only has to hold outside the region already certified. The union is a controlled invariant set far larger than any single certificate, and every level is still a tractable SOS program.

Build the hierarchy yourself

Repulsive barriers

CDC 2026 (to appear), with Georgios Fainekos, Bardh Hoxha, Hideki Okamoto and Sriram Sankaranarayanan

Moving obstacles usually force certificates that depend on time. Car-like dynamics don't change when you shift them in space, so we synthesize barriers once around an obstacle at the origin and re-anchor them to the obstacle's sampled position at run time, with a margin for how far it can move between samples.

Drag the obstacle into the car's path

Successive control Lyapunov functions

Part of my dissertation

Reaching a goal through clutter rarely admits one polynomial control Lyapunov function. Successive CLFs chain local certificates: each one only has to bring the system into the region of a lower level, and the last one brings it home, with at most one switch per level.

Watch the hand-offs
Floating point

Exact SOS certificates

Part of my dissertation, with Sriram Sankaranarayanan

SOS solvers return certificates that are almost right: the polynomial identity is off by tiny residues and the matrices are only numerically positive semidefinite. We round to rationals, repair the residue exactly, and confirm positive semidefiniteness in exact arithmetic, producing certificates that Lean 4 can check.

Run the repair on a real Gram matrix