Cloudflare Topaz: formal verification to prevent conflicts in DNS configuration

[self]

https://blog.cloudflare.com/topaz-policy-engine-design/

[spdegabrielle]

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)”

[self]

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

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

[spdegabrielle]

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