AssemblyLanguage or ByteCode, that comes along with the implicit property or explicit annotations, that it is e.g. type-safe.

See e.g. http://citeseer.ist.psu.edu/bernard99securityproperty.html

Not to be confused with ProofCarryingCode

See also TypedAssemblyLanguage