A software bug is defined as an error, flaw, or fault in a system that causes it to produce an incorrect or unexpected result, or to behave in unintended ways. Traditionally, verification is a task of bugs’ detection. The main traditional question is whether a system correctly implements the expected behavior, described in its specification. In this paper, we deal rather with a different question, which is: are we sure that our specification is even sound? In order to effectively answer the question, we limit ourselves to the case of analysis of definition of Graphical User Interface (GUI) of information systems, where the frontend (GUI) in many cases may be defined as a “walk” between different screens. For this kind of systems, we present a methodology for partial capturing of a GUI specification using a graphical presentation, which is a formal model of such a system at the abstraction level of its GUI. The model is subsequently saved as a program graph (Kripke structure). That graph is then translated into ProMeLA and can be checked against LTL properties. We define a set of properties specifying sanity checks of the specifications. The LTL properties (commandments) are aimed to cover standard verification notions such as consistency, absence of ambiguity, etc. We develop a tool helping the user to model a GUI specification and execute the sanity checks, which are done using standard verification machinery. The contribution presents a fresh use of temporal logics in this context. Other approaches that tackle the same problem (for example, based on UML diagrams) have not been used yet for formal verification of software specifications.