I wonder if AI systems like ChatGPT will be helpful in this area. Something that’s able to track all requirements of a system and understands the code enough to validate it against the requirements.
If LLM systems are going to give us a virtual army of programmers, I think formally proving more systems software (device drivers, browser engines, etc.) would be a great use of their time.
[1]: https://www.microsoft.com/en-us/research/blog/project-everes...
Basically, if you don't allow GPT to iteratively write, execute, criticise and then correct its code, you won't get good results.
It itself is not verified, and its results are so inaccurate that you need to verify them anyway.