Project Kickoff

The project started with the official EvIT Kickoff at the National Academy of Sciences Leopoldina in Germany (January 20, 2025). Together with Cyberagentur and four other groups of leading experts in the field we have made it our mission to enable formal verification at every level of the IT hardware-to-software stack. Our shared goal is the creation a new ecosystem of tools and methodologies that not only leverages the applicability of formal verification to new and existing system designs, but similarly facilitates a network and community of formal verification experts and users.

QBayLogic will support this mission with their unique expertise in hardware and hardware-to-software interface design based on Clash, a compiler that turns the well-known functional language Haskell into hardware descriptions / circuit designs. Haskell and Clash are particularly suited for formal verification due to the purely functional principles and the advanced type system the language is based on.

Our newly created Clash Formal Research and Development Team is looking forward to tackle the exciting challenges of the project over the next 4 years.

Our Mission

“We will bring your hardware development experience to the next level: not only can you use your favorite functional hardware description language Clash to create hardware designs, but at the same time you can utilize the power of its functional language design to easily connect with formal verification tools such as proof assistants or SMT solvers.”