Cloudflare blog post about using racket + rosette

General
1

This post

describes using racket + rosette for formal verification of cloudflare configurations. This work was also published at SIGCOMM 2024:

Larisch, James, Timothy Alberdingk Thijm, Suleman Ahmad, Peter Wu, Tom Arnfeld, and Marwan Fayed. "Topaz: Declarative and Verifiable Authoritative DNS at CDN-Scale." In Proceedings of the ACM SIGCOMM 2024 Conference, pp. 891-903. 2024.

The paper mentions both Racket and Rosette by name. I think this is pretty amazing, and an incredible tribute to Tim Alberdingk-Thijm who apparently did the work as an intern at cloudflare, to Emina Torlak for building Rosette, and to the Racket community (that's you) for making an incredible product!

Many thanks to Chris Lawson, a student at Cal Poly, for bringing this to my attention!

11 Likes
2

Oh damn, that's a very good use case to point to when people ask who uses Racket in production.

1 Like
3

Critically, all Topaz programs are encoded as YAML

Why reinvent the wheel when we already have the wonderful yaml-exp...