The automotive industry is grappling with an unprecedented surge in vehicle recalls, with over 21 million issued in 2024 alone[i]. This figure highlights a critical and ongoing challenge for manufacturers as they struggle to maintain quality control amidst increasingly complex vehicle technologies.

International safety standards such as ISO 26262 have been established to address these challenges.

ISO 26262: The standard for automotive functional safety

ISO 26262 is an international safety standard that defines the requirements and processes to ensure the functional safety of electrical and electronic systems in road vehicles. It aims to minimize the risks associated with system failures by implementing rigorous development and verification practices. The standard covers the entire lifecycle of automotive systems, from concept and design to production, operation, and decommissioning. Central to ISO 26262 are its Automotive Safety Integrity Levels (ASIL), which categorize risk into four levels—A through D—based on the severity, exposure, and controllability of potential hazards. These ASIL levels guide the safety measures required for different components, with higher levels demanding more stringent verification and validation processes.

The ISO 26262 certification helps the entire supply chain to have a common language for functional safety[ii].

The current trend is that every Original Equipment Manufacturer (OEM) demand that all the suppliers in the entire supply chain of automotive products adhere to the standard.

The benefits of formal methods

Verification is a cornerstone of ISO 26262, encompassing a range of activities such as peer reviews, dynamic testing, and static analysis. These activities ensure that the software behaves as expected, even in edge cases, and potential faults are detected early in development.

To support the automotive sector’s evolving needs for high-assurance software, automotive developers can significantly enhance the reliability and security of their systems by considering formal verification in their processes.

Formal verification frameworks are instrumental in assessing the correctness of hardware and software design operations by applying formal mathematical proofs. Unlike traditional methods, which focus on testing, formal verification seeks to provide mathematical assurances regarding the adherence of a system to specified safety and/or security requirements.

Even if a company has adopted memory-safe programming languages, vulnerabilities may persist in software. Testing alone is insufficient to address these vulnerabilities due to the inherent complexities of code. Formal methods offer a systematic approach to demonstrating correctness.

There are two primary ways formal methods can be leveraged across software and hardware development. First, they can be integrated directly into the developer toolchain, automating mathematical proofs during the software development lifecycle. This integration ensures that safety and security conditions are continuously verified as the software is built, tested, and deployed. Second, developers can opt for formally verified core components in their software supply chain, reducing the likelihood of incorporating vulnerable software libraries.

The SPARK language and tool suite are particularly well-suited for automotive software development, aligning with the rigorous demands of ISO 26262. By enabling static verification and formal proof of correctness, SPARK eliminates entire classes of run-time errors, such as buffer overflows and data races, which are critical concerns in safety-critical automotive applications. Unlike traditional testing approaches, which can miss rare but dangerous edge cases, SPARK’s mathematically proven guarantees provide a higher level of confidence in software reliability and compliance with ASIL-D—the highest level of automotive safety integrity. As the industry shifts towards greater software complexity, SPARK offers automotive developers a powerful tool to ensure functional safety in modern vehicles.

The SPARK technology is sound – if the source code violates an assurance property, the violation will be detected – while employing precise analysis techniques to reduce the “false alarms” that impede productivity.  The SPARK proof engine can check for program properties, including proper information flows, absence of run-time errors, and functional correctness with respect to formally specified requirements. Designed to make software safer and more secure, SPARK has fulfilled its goals and lays claim to a long and successful track record in high-integrity systems ranging from GPU firmware to air traffic control.

In an industry where software complexity continues to grow, ensuring functional safety and compliance with ISO 26262 is more critical than ever. As automotive systems become increasingly sophisticated, traditional testing methods can no longer guarantee reliability. By integrating formal verification techniques, developers can achieve higher levels of assurance, reducing the risk of costly recalls and enhancing overall vehicle safety.


[i] https://blog.bizzycar.com/automotive-recall-alert-over-21-million-vehicles-affected-year-to-date-2024-0
[ii] https://www.tuvsud.com/en-ae/resource-centre/blogs/understanding-the-iso-26262-standard—what-you-need-to-know