Aspect-oriented specifications and formal reasoning are often advocated for the design of complex, distributed systems. Commonly used design notations seem to lack the reasoning control of formal languages. OUN is an object-oriented language with facilities for aspect-oriented specifications through multiple viewpoints and for reasoning control. However, to be of practical use the language needs tool support. In this paper, we propose a formalization of aspects of the observable behavior of objects, using the PVS proof system. The formalism is extended with constructs to provide reasoning support for OUN specifications.