We present the concept of a unified graphical environment for expressing the semantics of control systems. The graphical control system design environment in Simulink already allows great flexibility for assertions aimed the verification and validation of the control software. We propose extensions to Simulink block diagram’s annotation capabilities to include formal control system stability, performance prop- erties and their proofs. These annotations can be created by the user or generated automatically by a third party software. In the latter case, we provide a conceptual description of a tool, that takes in a Simulink diagram of the control system as the input and feeds this information in the appropriate form to back-end solvers such as IQCβ or μ-tool. The output consists of an automatically generated proof of stability or performance, and a graphical representation of the system and the proof annotation. We finally describe how the graphical representation of the system and its properties can be translated to annotated programs in high-level languages such as Lustre or Matlab.