1. A computer-implemented method of verifying that untrusted software supplied by a code producer is safe to execute by a code consumer, comprising the steps of: defining a safety policy that specifies safe operating conditions of the untrusted software on the code consumer; generating a safety predicate for the untrusted software that determines if execution by the code consumer of the untrusted software will violate said safety policy; generating a safety proof that proves that said safety predicate is valid; and validating the untrusted software for execution based on said safety proof and said safety predicate prior to execution of the untrusted software.