The software-based programmable logic controller is an industrial computer widely used to implement safety–critical systems in digital I&C of nuclear power plants. As the complexity of future systems increases and demands for flexibility in control and monitor growing, the scale and role of software are becoming more significant, leading to concerns about software reliability. Formal methods are essential for ensuring software reliability in safety–critical domains. In recent years, formal methods have made substantial advancements, resulting in many sophisticated techniques. However, there is a lack of practical guidelines and a systematic solution in the nuclear domain. In this paper, we propose a comprehensive framework that integrates recent technological advancements in formal methods across all aspects of software development, encompassing definition, design, implementation, verification, and operation. Our aim is to establish a complete formal verification technology stack. Additionally, we also present the progress and future plans for a developing prototype software development toolchain that combines model-driven and formal approaches based on this framework.