So one trick is to work on DSLs with restricted semantics that are good enough for your domain. That makes proofs plus other formal techniques, and hence security guarantees, much much easier.
But if you insist on Turing complete languages, as I explained above, you can e.g. build abstract interpreters or data flow analyses that are able to prove really sophisticated things. I have implemented a C abstract interpreter for an industrial client that among many other things detected whether you were making potential out of bounds accesses to arrays, or potentially using uninitialized pointers. Of course it erred on the safe side. But it was really precise (few false positives). Not a walk in the park as it relies on Galois connections. See the seminal Cousot & Cousot 1977 paper [1].
https://www.youtube.com/watch?v=SVRiktFlWxI#t=2h9m38s
Software could be proven correct, but we abandoned that, just gave up on it, itβs too hard. But we can test it. We can use science, and we can write tests that demonstrate that the software is not failing. We treat software like a science, not like mathematics.
β Robert Martin