> Proving programs correct end-to-end (i.e. code to high-level properties) - as this company and others purport to do - is so difficult that humans have only been able to do it for very small programs (~10KLOC) and even then, in very specialised cases, where the programs have been written in an extra-simple way (often at the cost of performance, because performance often requires more complicated algorithms).

This is not true. It has been done. I’ve seen it done for an entire OS too. Humans are very capable of doing this. The issue is this is seldom done practically speaking because the effort is not worth the benefit when the program becomes too complex.

For simple programs and small domains it’s worth it. For example type checking. Type checking proves one aspect of your program (the types) is fully correct.

> This is not true. It has been done. I’ve seen it done for an entire OS too

That might be what pron's talking about. seL4 is only 10-20K lines of code as far as I remember. Maybe you have another OS in mind, though.