Non-proven correct code doesn’t even have specs you can test the code against. So comparing non-proven code without a formal spec with code that has a formal sp

Non-proven correct code doesn’t even have specs you can test the code against. So comparing non-proven code without a formal spec with code that has a formal spec and an end-to-end proof chain from spec to machine code, and then saying they are equally likely to be buggy is frankly ridiculous.