A generalized algorithm for the verification of functional models and the rules for the verification of diagrams related by levels of detail were developed in this paper. The algorithm is based on the analysis of a tree which describes the decompose relations in functional diagrams. At each step of the algorithm, a pair consisting of a parent diagram and a functional diagram is selected, and the correlation of the arrows and their roles is checked for both. The formalization of the verification rules was based on the set-theoretic representation of functional diagrams in the form of labeled oriented graphs. The rules make it possible to map the position and roles of the arrows associated with the detailed function block of the parent diagram to the arrows of the child diagram. The following rules for each of the possible arrow roles were established: “input”, “output”, “control”, “mechanism”. The use of the logic programming language PROLOG was proposed for the implementation of the algorithm. A knowledge base structure comprised of 3 interrelated predicates to describe the tree of diagrams, nodes and edges of the graphs was suggested. A query to check the verification rules was formed, and methods of binding variables and fixing roles were considered. The analysis and verification of a fragment of a functional model for the production of vinyl acetate from ethylene was conducted as an example. The functional diagrams for the processes “Condensate separation” and “Vinyl acetate isolation” connected by a decompose relation were developed, their set-theoretic models were constructed, and the use of rules for the verification of each type of arrow were considered.