Yes, I'm very sure. 99.9999% of the code you are running is not formally proven to be correct, and was not generated by a compiler whose output was formally proven to be correct.
Just curious, how much time have you spent in (a) industry, (b) a CS classroom, or (c) both?
> Yes, I'm very sure.
You do understand that you are proving my entire point? It is still not a reason to *NOT* test or check your code implementation at all or to only rely on an LLM to check it for you.
What it really means is that software testing is extremely more important.
For running formally verified code every day, seL4 runs on the iPhone's security chip (secure enclave) in the hands of billions of users and it is a formally verified microkernel used for cryptographic operations from payments to disk encryption everyday.
This kernel is also used on medical devices, cars and in defense equipment, relied on by hundreds of millions of users.
> Just curious, how much time have you spent in (a) industry, (b) a CS classroom, or (c) both?
Lots of decades to know that no process developing safety critical system software would allow AI-generated code that isn't checked by a human or is only checked by other LLMs and using that as a substitute to writing tests.