Internal verification is an approach where the proof of some property of a piece of code is layered on top of that code.  Instead of having 2 artifacts -- code and proof -- we just have one, namely this composite of code and proof.  The advantage is that a lot of the time the proof can piggyback on the code, when the two share their recursive structure (which is pretty often).  Discussion of these ideas.