Yes, those exactly are criteria that PCC was developed in mind with: "examples of safety properties that are covered in this paper are memory safety and complia

Yes, those exactly are criteria that PCC was developed in mind with: "examples of safety properties that are covered in this paper are memory safety and compliance with data access policies, resource usage bounds, and data abstraction boundaries" (from the abstract of [0]). That's what safety is, after all: that something bad does not happen. [0] George C. Necula, Peter Lee. Safe, Untrusted Agents using Proof-Carrying Code. 1998. http://www.cs.cmu.edu/afs/cs/project/pop-10/member/petel/www/publications/lncs98.pdf http://www.cs.cmu.edu/afs/cs/project/pop-10/member/petel/www...