TAG
Formal Methods
November 8, 2024
How we prevent conflicts in authoritative DNS configuration using formal verification
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 nameservers behavior.
![[James Larisch]](https://blog.cloudflare.com/_image?href=https%3A%2F%2Fblog.cloudflare.com%2F_emdash%2Fapi%2Fmedia%2Ffile%2F01KW44C9J5HQA4MAD7AN1K285E.jpg&w=64&h=64&f=webp&fit=cover&position=center){kind=link}
![[Suleman Ahmad]](https://blog.cloudflare.com/_image?href=https%3A%2F%2Fblog.cloudflare.com%2F_emdash%2Fapi%2Fmedia%2Ffile%2F01KW44MCC5WJ427B6XCV7Z59EV.png&w=64&h=64&f=webp&fit=cover&position=center){kind=link}
![[Marwan Fayed]](https://blog.cloudflare.com/_image?href=https%3A%2F%2Fblog.cloudflare.com%2F_emdash%2Fapi%2Fmedia%2Ffile%2F01KW4975XAXEZ77Q31PP9FF3ME.jpg&w=64&h=64&f=webp&fit=cover&position=center){kind=link}
Subscribe to receive notifications of new posts
Getting Started
Public interest
Resources
Solutions
- SSE and SASE platform
- Cloudflare AI Cloud
- AI Security
- Frontend Development Platform
- Multi-Tenant Platform Development
- Web Security Platform