Several times I have begun to record ideas about formal proofs for code. Just now (2005) I gathered these ideas into this directory. The ideas have never come together and stuff here may be inconsistent.
An early note
Here are some older notes on this general idea, and a new note.
Here is another start.
Capability Complience of Raw Code
Keykos Kernel thoughts
Here are some thoughts on safe storage allocation.
more thoughts on system proofs
My rant on academic papers on proofs.
See an entirely different form of program proof here.
Obstacle to HOL
Pipe dream (so far)
more wandering, and more
Other similar work on Proof Carrying Code
Lightweight Static Capabilities
Relevant book: Mechanizing Proof