Cloudflare Topaz: formal verification to prevent conflicts in DNS configuration

Racket! https://racket-lang.org/

“Whenever an engineer changes one of these programs, we run all the programs through our custom model checker (written in Racket + Rosette)”

Video: https://www.youtube.com/watch?v=hW7RjXVx7_Q

Paper: https://research.cloudflare.com/publications/Larisch2024/

“we formally verify the programs — written in a custom Lisp-like programming language — that our nameserver executes when it receives a DNS query” nice