I have to admit I used to think any level of formal verification was worthwhile.

But I recently tried having agents try starting with formal models, and then building code using that as basis. In the end to models were never detailed enough to catch the most common issues that were shaken out with getting a high level of coverage and mutation testing.

At which point, the predictive power of the formal models became somewhat vacuous.

I’m trying to be more optimistic that maybe using dependently typed languages will yield better results.