It reads like not much has changed, and given what the two underlying issues are, that's not surprising.

I've been considering getting into formal verification, but the learning curve and the illusions of rigor angle are keeping me away so far. It's great that an agent can now figure out a formal spec on my behalf and check the program it generates on my behalf for compliance, but that doesn't make me any better equipped to keep it all honest end to end. The hard part is gone, remains the hard part.

Anecdotally, what I've been doing with agents instead is I made more things declarative. Config, policy, etc. manifests can be linted for syntax and schema compliance, and the logic only has to be written once. The agents can then go ham emitting their silly little JSONs or whatever, the risk is a lot more bounded that way. Just gotta be mindful to not smuggle in too much logic, and not walking the configuration complexity clock too hard, and all remains well. I feel with agents this is now more scalable, but maybe I'll come to think different later.

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