Kry10 hat sich in Zusammenarbeit mit Proofcraft zum Ziel gesetzt, eine neue Klasse von eingebetteten und cyber-physikalischen Systemen zu ermöglichen, mit formal verifizierter Unterstützung für aktualisierbare Multicore-Systeme, die auf dem verifizierten seL4-Mikrokernel basieren. Damit das System auf mehreren Rechenkernen läuft, wird eine Multikernel-Konfiguration von seL4 verwendet, mit einer separaten seL4-Kernel-Instanz pro Kern. Für Software- und Konfigurationsaktualisierungen ohne Ausfallzeiten entwickelt das Team eine privilegierte User-Space-Komponente, die eine hochrangige API für die Authentifizierung und Ausführung von Aktualisierungsbefehlen bereitstellt. Zur formalen Verifikation werden sie Theorembeweis-Frameworks entwickeln, um die Korrektheit von Multikernel-Konfigurationen auf Kernel-Ebene und die Korrektheit von privilegierten Komponenten auf User-Ebene zu überprüfen. Eine große Herausforderung bei der Verifikation ist die Parallelität zwischen mehreren Kernel-Instanzen und User-Space-Threads.

Clash Formal will die Anwendbarkeit formaler Verifikationswerkzeuge wie Beweisassistenten oder SMT-Löser nicht nur für funktionale Programme, sondern in gleicher Weise auch für intrinsisch parallele funktionale Schaltungsdesigns ermöglichen.
 Ziel des Projekts ist es, die Leistungsfähigkeit funktionaler Sprachen für die präzise Beschreibung von Hardware- und Softwarefunktionalität in Kombination mit einem starken Typsystem zu nutzen, um das gesamte Spektrum nicht-funktionaler Sicherheitsanforderungen abzudecken.
 Zu diesem Zweck nutzen sie Clash, eine funktionale Hardwarebeschreibungssprache, deren Syntax und Semantik der funktionalen Programmiersprache Haskell entlehnt sind. Sie bietet einen vertrauten strukturellen Designansatz für kombinatorische und synchrone sequentielle Schaltungen. Der Clash-Compiler wandelt funktionale high-level Hardwarebeschreibungen in synthetisierbare low-level Sprachen, wie VHDL, Verilog oder SystemVerilog um.
 Ihr besonderer Schwerpunkt liegt auf der formalen Verifikation funktionaler Hardware-Designs  gemeinsam mit den Hardware-Software-Schnittstellen. Ihr Ziel ist es, ein voll ausgestattetes Ökosystem aus eng miteinander verbundenen Designtools und Methodiken zu schaffen, das das gesamte Spektrum von Software, Hardware und formalem Beweisen sowie die damit verbundenen Methodiken abdeckt.

PISTIs-V addressiert den Mangel eines integrierten IT-Stacks mit nachweisbarer Ende-zu-Ende-Sicherheit für eingebettete/cyber-physische Systeme. Ziel ist die Entwicklung eines Referenzsystems mit Nachweisen für starke Sicherheits- und Schutzmerkmale, die Hardware und Software sowie deren Interaktion abdecken. Insbesondere wird PISTIs-V überprüfen, ob das neue Betriebssystem LionsOS die Spezifikationen erfüllt und Sicherheits- und Schutzmerkmale garantiert. Dazu zählen unter anderem die Verhinderung der unbefugten Weitergabe sensibler Daten und die Gewährleistung von Echtzeit-Fristen unter Verwendung formal verifizierter Hardwarekomponenten. Einen wertvollen Beitrag wird auch die Entwicklung von Pancake leisten, eine neue Systemprogrammiersprache mit einem verifizierten Compiler.

Formula-V hat sich zum Ziel gesetzt, ein vollständig formal verifiziertes System zu schaffen, das den höchsten Standards in Bezug auf Sicherheit, Datenschutz und Vertrauenswürdigkeit entspricht. Um dies zu erreichen, integriert das Projekt sowohl Software- als auch Hardware-Verifikation und legt damit ein solides Fundament für die digitalen Technologien von morgen.

PROTECT möchte mit innovativen Methoden der formalen Verifikation die IT-Sicherheit auf ein neues Niveau heben und das Vertrauen in digitale Systeme nachhaltig stärken. Gemeinsam erarbeiten die PROTECT-Partner Lösungen, die IT-Systeme von Unternehmen und öffentlichen Einrichtungen robuster gegenüber Cyberangriffen machen. Dabei setzen sie auf drei zentrale Stärken: Sie verfolgen einen Bottom-up-Ansatz, indem sie bestehende Methoden der Partner kombinieren und den Anwendern ermöglichen, die am besten geeigneten Verfahren für ihren konkreten Anwendungsfall auszuwählen. Sie arbeiten forschungsgetrieben, wobei die wissenschaftlichen Partner ihr tiefes Fachwissen einbringen. Technisch kommen dabei moderne Werkzeuge zum Einsatz, darunter fortgeschrittene Verifikationstechniken, SAIL für ISA-Spezifikationen, verschiedene RISC-V-Referenzarchitekturen und Rust als Implementierungssprache