I don't think issues like syntax and schema compliance are the level of problems where verification comes into play

In this case it's more that the underlying declarative systems function as they should across any possible states or configurations

You mentioned policy and the policy language Cedar uses Lean formal verification in this way, not to verify that the specific policies users create are sound but to ensure that the declarative policy engine itself cannot produce any invalid or unwanted configurations