One concrete application we've been working on: exhaustive verification of deterministic policy tables - WAF rules, DNS filter lists, routing tables.
The AI angle cuts both ways here.
AI makes it cheaper to generate policy logic, which means more policies, faster, with less review.
Formal verification of the decision function (not the config syntax) becomes the backstop - prove every input produces the correct output, not just that the rules look right.
One result that surprised us:
a DNS filter list covering 2M domains compresses to 253 bytes as a verified decision function.
Not a Bloom filter - exact, exhaustively proven against every domain. The same approach works for WAF rulesets and IP routing tables.
The AI angle cuts both ways here. AI makes it cheaper to generate policy logic, which means more policies, faster, with less review. Formal verification of the decision function (not the config syntax) becomes the backstop - prove every input produces the correct output, not just that the rules look right.
One result that surprised us: a DNS filter list covering 2M domains compresses to 253 bytes as a verified decision function.
Not a Bloom filter - exact, exhaustively proven against every domain. The same approach works for WAF rulesets and IP routing tables.
The verifier is MIT-licensed: https://github.com/ProofCodec/proofcodec-verify
Curious whether the formal verification community has looked much at policy-as-decision-function vs. policy-as-configuration.
The latter gets most of the tooling attention but the former is where correctness actually matters at runtime.