Kry10, in collaboration with Proofcraft, aims to enable a new class of embedded and cyber-physical systems with formally verified support for updatable multicore systems based on the verified seL4 microkernel. To allow the system to run on multiple cores, a multicore configuration of seL4 is used, with a separate seL4 kernel instance per core. For software and configuration updates without downtime, the team is developing a privileged user-space component that provides a high-level API for authenticating and executing update commands. For formal verification, they will develop theorem proving frameworks to verify the correctness of multi-kernel configurations at the kernel level and the correctness of privileged components at the user level. A major challenge in verification is the parallelism between multiple kernel instances and user space threads.

The mission of Clash Formal is to enable the applicability of formal verification tools, such as proof assistants or SMT solvers, not only for functional programs, but in the same fashion for intrinsically parallel functional circuit designs.
The goal of the project is to leverage the power of functional languages for the precise description of hardware and software functionality in combination with a strong type system to capture the whole spectrum of non-functional security and safety requirements.
To this end, they leverage Clash, a functional hardware description language that borrows both its syntax and semantics from the functional programming language Haskell. It provides a familiar structural design approach to both combinational and synchronous sequential circuits. The Clash compiler transforms high-level functional hardware descriptions to low-level synthesizable VHDL, Verilog, or SystemVerilog.
The particular focus lies on the formal verification of functional hardware designs together with their hardware-to-software interfaces, a research area which still is less explored than for example pure functional program verification. Clash Formal's goal is to create a fully featured ecosystem of tightly interconnected design tools and methodologies that capture the whole spectrum of software, hardware and formal reasoning as well as their connected methodologies.

PISTIs-V addresses the lack of an integrated IT stack with provable end-to-end security for embedded/cyber-physical systems. It aims to develop a reference system with proofs of strong safety and security properties covering hardware and software and their interaction. Specifically, PISTIs-V will verify that the new LionsOS operating system (OS) operates to specification and enforces security and safety properties, including the prevention of unauthorised leaking of sensitive data and the guarantee of real-time deadlines, making use of formally verified hardware components. A core enabler of the work will be Pancake, a new systems programming language with a verified compiler.

Formula-V aims to create a fully formally verified system that meets the highest standards of security, privacy, and trustworthiness. To achieve this, the project integrates both software and hardware verification, laying a solid foundation for the digital technologies of tomorrow.

PROTECT aims to take IT security to a new level using innovative formal verification methods and to strengthen trust in digital systems in the long term. Together, the PROTECT partners are developing solutions that make the IT systems of companies and public institutions more robust against cyber attacks. In doing so, they rely on three key strengths: They pursue a bottom-up approach by combining existing methods from their partners and enabling users to select the most suitable procedures for their specific application. Their work is research-driven, with scientific partners contributing their in-depth expertise. Technically, modern tools are used, including advanced verification techniques, SAIL for ISA specifications, various RISC-V reference architectures and Rust as the implementation language.