An early note
Here are some older notes on this general idea, and a new note.
Here is another start.
Here are some thoughts on safe storage allocation.
My rant on academic papers on proofs.
See an entirely different form of program proof here.
Other similar work on Proof Carrying Code