Now that I think of it, instead of checking specifically firewall (or something else) validation, we could try to make the config generation part as declarative as possible. Then we could prove soundness of the mapping translator (by hand or with a proof checker) rather than prove it for every component.
In most cases there are just a few primitives (option X requires option Y to be set to Z, option X is mutually exclusive with Y). These should not be overly hard to convert to a long pattern match.