Comment by daymanstep

As LLMs make formal verification cheaper (they can generate proofs that can then be automatically checked) many of the verifiable components of software systems, such as compilers and microkernels, will be verified. I suppose the issue is that the critical bugs are rarely in compilers and microkernels, but more often in applications, such as web browsers, which are more difficult to formally verify.