The problem is most languages we use are not very safe, and which means if you have one unverified part in code, you can&#x27;t prove code correct. I read a paper recently which tried to do modular verification of C by adding runtime contracts are boundaries[1]. Theory wise its sound, but it&#x27;s really slow. You may even have to rewrite code certain ways to make it perform better.<p>[1] <a href="https:&#x2F;&#x2F;lirias.kuleuven.be&#x2F;bitstream&#x2F;123456789&#x2F;471365&#x2F;3&#x2F;sound-verification.pdf" rel="nofollow">https:&#x2F;&#x2F;lirias.kuleuven.be&#x2F;bitstream&#x2F;123456789&#x2F;471365&#x2F;3&#x2F;soun...</a>