Formal methods of software verification: modern approaches and challenges

Abstract

The study examines the problem of increasing software reliability using formal verification methods, which are becoming increasingly common in modern software systems engineering. Unlike traditional testing, which detects only a portion of errors, formal methods rely on mathematical models and logical reasoning, enabling more comprehensive and reliable verification of software systems. The relevance of the topic is driven by the growing complexity of software and the strict requirements for its correctness in critical areas such as aviation, healthcare, energy, and cybersecurity. The paper systematizes the key directions of formal verification. It demonstrates that formal specifications provide a precise mathematical definition of software requirements, eliminating ambiguities inherent in natural language. Model checking makes it possible to automatically explore all possible system states, revealing hidden defects in the behavior of multi-threaded and distributed programs. Formal proof of correctness is based on logical systems and axiomatic methods, guaranteeing the highest level of confidence that the program meets its specification. Symbolic execution enables analysis of all execution paths and automatic generation of test data. At the same time, a number of challenges that hinder the widespread adoption of formal methods in practice are identified. These include the scalability problem, which limits the efficiency of analyzing large systems; the need for highly qualified specialists with a strong mathematical background; the complexity of formalizing requirements; and the difficulties of integrating these methods into modern development methodologies such as Agile and DevOps. Future prospects are associated with the integration of artificial intelligence technologies to automate the creation of specifications and the construction of proofs, the development of hybrid methods combining formal verification with testing, and the
active use of these approaches in cybersecurity, blockchain technologies, and autonomous transport systems. Of particular importance is the integration of formal methods into programming environments and continuous integration systems, which increases their accessibility for industry. Thus, formal verification methods remain a powerful tool for improving software system reliability. Despite the existing challenges, they hold significant potential for further development and for gradually evolving from an academic discipline into an essential component of industrial software development.