Abstract: In this paper, a kind of type safety policy is introduced, which is used to assure code safety The logic representation, formal description, and proof method of the policy are discussed in detail A and theorem prover HBTSTP based on the policy is also presented at the end of the paper The core idea of the policy is that any valid memory address has an attached type, and a symbol expression is used to trace the change of the whole memory state For instructions that need to read or write memory, HBTSTP is called to check whether the destination is type safe if it is type safe, then the read or write operation is memory safe