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

George Necula
Peter Lee
Lightweight Static Capabilities

Relevant book: Mechanizing Proof