Dresden, July 15, 2025 – Our digital infrastructure is the backbone of modern society – but it’s increasingly under threat. To protect sensitive data and critical systems, Germany’s Agentur für Innovation in der Cybersicherheit GmbH (Cyberagentur) has launched the EVIT research program (Ecosystem Formally Verifiable IT – Provable Cybersecurity, EVIT). Kernkonzept joins the Formula-V research group to help build IT systems that can be mathematically proven to be secure. With its expertise in secure operating systems, Kernkonzept brings key building blocks for a future where trust in technology is based not on promises, but on proof.
The EVIT project aims to rethink cybersecurity from the ground up – through mathematically proven correctness of both hardware and software. This is the only way to be sure that a given IT system is completely free of security-critical errors and vulnerabilities. Kernkonzept contributes its expertise as IT security specialist, with a particular focus on operating systems and microkernel-based virtualization.
A formally verified IT ecosystem would bring immense benefits for cybersecurity, but to this day it does not yet exist. That is why Agentur für Innovation in der Cybersicherheit GmbH (Cyberagentur), a federal agency founded to foster cyber innovation and enhance IT security in the areas of interior and exterior security, has launched the EVIT research program: to bring trustworthy IT into widespread use by further developing formal methods.
EVIT consists of five projects with different focal points. The one that targets trustworthy IT hardware and software infrastructure in a holistic approach is called Formula-V. For the next four years, Kernkonzept will work as part of the Formula-V research group, which is headed by Barkhausen Institut. The research group aims to enable true security by design by developing a trustworthy, formally verifiable IT hardware and software infrastructure. The foundation of this work will be the L4Re Secure Separation Kernel VS 1.0.1 developed by Kernkonzept, which is accredited by BSI for use up to German GEHEIM/NATO SECRET and Common Criteria certified as EAL4+.
“Formula-V is a significant move towards strengthening German and European cybersecurity. Developing methods for bug-free software will hopefully lead to a future with a much more resilient IT infrastructure”, says Dr. Hendrik Tews, Head of Formal Methods, who is leading the project for Kernkonzept. “Constructing solid operating systems such as the L4Re Operating System Framework, using a theoretical and mathematical foundation, is an important next step – and we are well-prepared for this with our background in theoretical computer science and formal methods.”
Kernkonzept joins forces with Barkhausen Institut, TU Dresden, Fraunhofer AISEC, Ferrous Systems and TU Berlin to advance technology for building secure hardware, software, and overall, more trustworthy systems. Central to this effort is mathematical proof of the correctness of hardware and software against a formal model. By improving both the development tools and the techniques used for formal proofs, the consortium aims to make significant contributions to the ecosystem.
Together, they are building a fully verified IoT hardware and software stack, based on the RISC-V hardware architecture and the Rust programming language, with all components formally proven with the Rocq theorem prover. Several working groups will enhance the ecosystems for security mechanisms and methods for software development.
“Trustworthiness in the digital world must no longer be a matter of belief. With Formula-V, we rely on mathematically sound foundations to build secure systems from the ground up – transparent, verifiable, and resilient. Only then can we achieve true digital sovereignty”, says Prof. Dr. Gerhard Fettweis, scientific director and founding father of the Barkhausen Institut.
With the official launch of the EVIT project, the entire research program was transferred to the Dresden project office, which is headed by Dr. Christoph Hof. Dresden, Germany’s hub for operating systems and microelectronics, thus also becomes the center of the new ecosystem of verifiably secure IT.
Kernkonzept was founded more than 10 years ago as a spin-off from TU Dresden’s Faculty of Computer Sciences and still has its headquarters in Dresden. Their strategic decision to build the L4Re Microkernel system according to the Principle of Least Authority, thus completely following the paradigm of Security by Design, laid the groundwork that now enables the company to contribute their expertise.
“By building a trustworthy IT through formal verification for both hardware and software, we will lift Germany’s and Europe’s IT sovereignty to a new level, especially for security-critical systems”, says Dr. Michael Hohmuth, founder and CEO of Kernkonzept.
