This piece of work is dedicated to the use of formal methods in designing ERP systems in MSBS Navision environment capabilities research. Theoretical principles of formal and informal specifications and implementation peculiarities are analyzed re various specifications. UML and Z specification languages were chosen for comparison. Also MSBS Navision C/SIDE ERP system design environment is analyzed. A part of “Fixed assets” domain functionality is specified in different languages. Their clarity, precision, and implementation are compared. Formal methods (same as informal ones) have their advantages and disadvantages. UML specification is fundamentally based on graphic representation. It’s clearer, more readable, but its compatibility can’t be unambiguously verified. Z specification language has a mathematical basis. The compatibility of Z specification can be precisely verified. However, Z specification is difficult to read and learn. It’s impossible to validate the specification unambiguously neither using UML, nor Z. UML language is highly applicable for specification and design of ERP systems, because you can specify object-oriented system models using this language, and C/AL programming language is partially object-oriented. Z language specification is only useful for describing particular, sophisticated parts of the system. Z language can also be used for detailing UML specifications.