I think the hard part of formally verifying something is not writing code. Granted it is hard and LLMs will help with that.You also need to model the user space correctly and this is a bit like causal modeling, there are many confounding factors to be taken into account and if you missed something at modeling time you'll miss bugs