We use the proof of the safety predicate, written out in an appropriate language (to be described in the next section), as the proof that the code obeys the safety policy. This is justified formally by the safety theorem, stated below:
Since the abstract machine gets stuck when there is any violation of an
or 
safety check, this theorem provides an absolute
guarantee that a certified program will not have such violations, as long
as its execution is started in a state that satisfies the precondition.
The proof of the Safety Theorem is beyond the scope of this paper, but can be found in a separate technical report [16].
