# Cloudflare blog post about using racket + rosette

**URL:** <https://racket.discourse.group/t/cloudflare-blog-post-about-using-racket-rosette/3336>\
**Category:** General\
**Tags:** rosette\
**Created:** [November 18, 2024, 12:28am UTC](https://racket.discourse.group/t/cloudflare-blog-post-about-using-racket-rosette/3336 "2024-11-18T00:28:46Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![jbclements](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/jbclements/32/11_2.png) [@jbclements](https://racket.discourse.group/u/jbclements)\
**Post date:** [November 18, 2024, 12:28am UTC](https://racket.discourse.group/t/cloudflare-blog-post-about-using-racket-rosette/3336/1 "2024-11-18T00:28:46Z")

</div>

This post

> **[How we prevent conflicts in authoritative DNS configuration using formal...](https://blog.cloudflare.com/topaz-policy-engine-design/)**
>
> We describe how Cloudflare uses a custom Lisp-like programming language and formal verifier (written in Racket and Rosette) to prevent logical contradictions in our authoritative DNS nameserver’s behavior.

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!

---

<div class="post-metadata">

**Author:** ![notjack](https://avatars.discourse-cdn.com/v4/letter/n/e47774/32.png) [@notjack](https://racket.discourse.group/u/notjack)\
**Post date:** [November 18, 2024, 11:07pm UTC](https://racket.discourse.group/t/cloudflare-blog-post-about-using-racket-rosette/3336/2 "2024-11-18T23:07:29Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![cadence](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/cadence/32/998_2.png) [@cadence](https://racket.discourse.group/u/cadence)\
**Post date:** [November 20, 2024, 2:53am UTC](https://racket.discourse.group/t/cloudflare-blog-post-about-using-racket-rosette/3336/3 "2024-11-20T02:53:14Z")

</div>

> Critically, _all_ Topaz programs are encoded as YAML

Why reinvent the wheel when we already have the wonderful [yaml-exp](https://racket.discourse.group/t/yaml-exp-write-s-expressions-in-yaml/2398)...