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