This paper discusses a methodology for the (informal) verification of processor-supported protection mechanisms of high-level language architectures (e.g., INTEL iAPX 432). The methodology takes an abstract model representation of the real hardware architecture and proceeds to show that protection constraints for the model are complete and correct. Completeness and correctness are satisfied by showing consistency with a general protection model, the Access Matrix model. A methodology for proving this consistency is provided, with worked examples of the protection-relevant instructions of a Burroughs architecture.