This paper discusses the formal requirements for implementing virtual machine systems on third-generation computer architectures. It begins with a definition of a virtual machine, emphasizing efficiency, isolation, and identical behavior. A model of third-generation computer systems is developed, including a processor with supervisor and user modes, memory protection, and a trap facility. The paper then applies formal techniques to derive necessary and sufficient conditions for an architecture to support virtual machines. The main theorem states that a virtual machine system can be constructed if and only if certain properties of the real machine's instruction set hold. The conditions are simple and can be used to evaluate existing hardware or guide the design of new machines. The paper also covers related concepts like hybrid virtual machines and recursive virtualization, providing their specific requirements. Finally, it discusses the simplifications in the model, possible extensions, and the utility of the formal approach.This paper discusses the formal requirements for implementing virtual machine systems on third-generation computer architectures. It begins with a definition of a virtual machine, emphasizing efficiency, isolation, and identical behavior. A model of third-generation computer systems is developed, including a processor with supervisor and user modes, memory protection, and a trap facility. The paper then applies formal techniques to derive necessary and sufficient conditions for an architecture to support virtual machines. The main theorem states that a virtual machine system can be constructed if and only if certain properties of the real machine's instruction set hold. The conditions are simple and can be used to evaluate existing hardware or guide the design of new machines. The paper also covers related concepts like hybrid virtual machines and recursive virtualization, providing their specific requirements. Finally, it discusses the simplifications in the model, possible extensions, and the utility of the formal approach.