Proof carrying code

[Google Scholar] [Wikipedia]

Papers: necula:popl:1997

Proof carrying code is code (typically machine code, bytecode, etc.) accompanied by a proof that the code satisfies some property such as memory safety, termination, etc.

Typed assembly language