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
NaCl

Relevant book: Mechanizing Proof