Clash Formal - Ecosystem formally verifiable IT

Home | Projects | Clash Formal – Ecosystem formally verifiable IT

The challenge

The research program Ecosystem formally verifiable IT (EvIT) of Cyberagentur has a clear mission: the research and development of formal verification tools and methodologies that enable verification at every level of a complete hardware-to-software system stack. The challenge is to create an ecosystem, which enables the easy design of safe and secure products with reasonable development efforts and costs.

The solution

Our Clash ecosystem offers a perfect connection between hardware and program design via utilizing the shared Haskell language front-end. At the same time, it connects well with formal verification tools such as proof assistants or model checkers due to the underlying functional design principles. In this project, we leverage these connections to make them applicable and approachable at every level of an IT hardware-to-software stack.

The deliverables

Clash 2.0 will first time enable developers to use formal verification tools naturally and directly integrated with their workflow. We will showcase the new features on an advanced IT application with strong safety and security requirements. Furthermore, documentation and training material will be offered to guide developers in working with the new features and tools.

Find out more at the official project page:

clash-formal.org

Our clients

Why QBayLogic?

QBayLogic stands out for its ability to harness the power of both software and digital hardware design. Our Clash software-to-hardware compiler, based on the Haskell programming language, is a prime example of our innovative approach.

This unique expertise made us the ideal fit for Cyberagentur’s ambitious EvIT project.