Talks

How Cloudflare Uses Racket and Rosette to Verify DNS Changes
RacketCon, October 2025 | Keynote

Programming language-focused presentation on Topaz, Cloudflare's system for figuring out what IP to return when it receives a DNS query. We execute small Lisp-like programs on the hot-path, and verify the programs using a Racket/Rosette verifier.

---

Topaz: Declarative and Verifiable Authoritative DNS at CDN-Scale
SIGCOMM, August 2024

Academic presentation on Topaz, Cloudflare's system for figuring out what IP to return when it receives a DNS query. We execute small programs on the hot-path, and we formally verify these programs.

---

No Root Store Left Behind
HotNets, November 2023

Turns out browsers like Firefox are really strict when it comes to TLS root certificates. Everyone tries to copy Firefox, but they can't do so completely. This paper suggests a way for them to do so completely.

---

Hammurabi: A Framework for Pluggable, Logic-Based X.509 Certificate Validation Policies
CCS, November 2022

Have you ever wondered what would happen if TLS clients validated X.509 certificates using Prolog?

---

CRLite: A Scalable System for Pushing All TLS Revocations to All Browsers
Oakland (IEEE Security and Privacy), May 2017

No system provides complete coverage of all revoked TLS certificates. Until now. Featuring bloom filters, everyone's favorite compressed data structure with false positives (that we eliminate).

---