Hacker News Reader

This was running user-facing, in production? Do you have any experience with scaling Z3? I'm thinking large problems running on many machines, contra many small problems on many processes.

For some reason, I always imagined that SMT was used to verify stuff before putting it into production, but this opens up a whole new world of ideas for me.

View on HN

It wasn't running as any sort of persistent service, if that's what you mean. It just ran during deployments to check output of old & new firewall generation methods for equivalence.

Something like what you describe was implemented in an Azure system called SecGuru, which is sort of a generalized version of firewall comparison to check security rule enforcement. Here is the whitepaper: https://www.microsoft.com/en-us/research/wp-content/uploads/...

Reply on news.ycombinator.com