Researchers develop contract-based verification tool for embedded automotive C code safety

Formal verification of safety-critical embedded systems is growing more important as automotive software grows in complexity. A team of researchers has introduced a method to verify not just what code is supposed to do, but also how it does it—catching violations of non-functional constraints that could threaten safety.

The Problem with Untrusted Code#

While tools like Frama-C and specification languages such as ACSL (ANSI/ISO C Specification Language) can formally verify the functional behavior of C code, they often miss safety issues at the module level. Code written by subcontractors, less experienced developers, or generated by large language models may pass functional checks yet still call unsafe functions, use uninitialized variables, or violate critical control and data flow rules.

A New Approach to Interface Contracts#

The researchers created a set of general rules targeting non-functional requirements in safety-critical embedded systems—requirements like restrictions on which functions can be called or how data flows between modules. Their rules focus on module interactions and interfaces rather than individual functions, operating orthogonally to widely used standards like MISRA-C.

To enforce these rules, they designed a new interface specification contract language for C modules and built a Frama-C plugin that checks whether a module adheres to its declared contract. The checker verifies properties such as which external functions are permitted and which program variables must be initialized.

Real-World Validation#

The team integrated their tools into a complete verification chain and tested it on two case studies using safety-critical C code from Scania trucks. In both cases, they extracted module contracts and function-level ACSL contracts from informal system requirements and successfully verified them through the toolchain.

The approach bridges a gap in formal verification by ensuring that safety-critical embedded software not only behaves correctly but also respects structural and interface constraints that protect system integrity.