The abstract and conclusion of the linked paper[1] is a better entry point than the article:

> In this paper we present Topaz, a new authoritative nameserver architecture for anycast CDNs which encodes DNS objectives as declarative, modular programs called policies. Nameservers execute policies directly in response to live queries. To understand or change DNS behavior, operators simply read or modify the list of policy programs. In addition, because policies are written in a formally-verified domain-specific language (topaz-lang), Topaz can detect policy conflicts before deployment. Topaz handles ~1M DNS queries per second at a global CDN, dynamically deciding addresses for millions of names on six continents. We evaluate Topaz and show that the latency overheads it introduces are acceptable.

1: https://files.research.cloudflare.com/publication/Larisch202...

The docs for the Rosette language used to write their verified interpreter:

https://docs.racket-lang.org/rosette-guide/index.html

A talk presenting the language by the author (Emina Torlak):

https://m.youtube.com/watch?v=nOyIKCszNeI&t=3245s&pp=ygUOcmF...