Cloudflare Topaz: formal verification to prevent conflicts in DNS configuration (opens in new tab)

(blog.cloudflare.com)

7 pointsself1y ago3 comments

3 comments

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

selfOP1y ago

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

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

spdegabrielle1y ago

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

j / k navigate · click thread line to collapse

3 comments

spdegabrielle1y ago

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

selfOP1y ago

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

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

spdegabrielle1y ago

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

j / k navigate · click thread line to collapse