Formula-V: Developing a Fully Verified IT System for Trusted Digital Technologies

The goal of the Formula-V project is to develop a fully formally verified system that meets the highest standards for security, privacy, and trustworthiness. Mathematical and logical proofs ensure that systems function correctly and as intended. To achieve this, Formula-V combines software and hardware verification – thus creating a robust foundation for future digital applications.

This is especially important for the Internet of Things (IoT), which connects critical devices such as autonomous vehicles or medical equipment. As these systems grow more complex, so do their vulnerabilities: attackers can extract sensitive data or manipulate system behavior. Formal verification helps mitigate these risks by identifying and eliminating vulnerabilities at the design stage.

The Barkhausen Institut (BI) leads the Formula-V project and coordinates collaboration with academic and industrial partners. BI also plays a central role in researching and advancing the formal verification methods required. By applying rigorous mathematical proofs to both software and hardware, the project aims to build a trustworthy IoT ecosystem – one where security is built in from the ground up.

Achieving formal verification across an entire system is highly complex. Formula-V explores how recent innovations can reduce this complexity and make verification more practical. One key approach is to align formal assumptions made in the software with corresponding proofs in the hardware.

A cornerstone of the project is the development of a unikernel system – a minimalist operating system tailored to a single application. By including only the most essential components, such as file systems and networking functions, this streamlined design increases both efficiency and security. The system is further hardened by integrating formal verification at every layer, ensuring reliability at the highest level.

Formula-V’s results will be applicable across a range of technologies, including IoT devices, cloud systems, and smartphones. The project ultimately aims to establish formal verification as a standard practice in modern system development – laying the groundwork for a secure and trustworthy digital future.

Project Duration: 2 December 2024 – 1 December 2028

Project Partners: Dresden University of Technology (TUD), Technische Universität Berlin, Kernkonzept GmbH, Ferrous Systems GmbH, Fraunhofer Institute for Applied and Integrated Security (AISEC)

Contact: Sebastian Ertel (Sebastian.Ertel@barkhauseninstitut.org), Verified System Design Automation