Proof-Carrying Code

The term for a type of program or module that carries a verifiable specification of its behavior as it is migrated between contexts.

This page is linked from: Andrew Appel