Clash Formal is part of the Ecosystem formally verifiable IT (EvIT), a research mission for the integration of formal verification capabilities across all levels of the hardware / software stacks being present in basically all IT devices we use today. To this end, the Clash Formal project aims at leveraging the power of functional languages for the precise description of hardware and software functionality in combination with their type systems for capturing non-functional security and safety requirements.

The project builds upon the existing ecosystems for the functional programming language Haskell and the functional hardware description language Clash, which share the same language frontend and type system. On that behalf:

"We aim 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."

We particularly focus on the formal verification of functional hardware designs together with their hardware-to-software interfaces. A research area which is still less explored than for example pure Haskell program verification. The goal is a fully featured ecosystem of tightly interconnected design tools and methodologies which captures the whole spectrum of software, hardware and formal reasoning as well as their connected methodologies.

Does this sound exactly like what you are looking for? Then have a closer look at our more detailed Project Overview, where you can learn more about the particular project’s goals, our research and development progress, and some of the project challenges.

Open-source Community

Haskell and Clash already benefit from an active community, to which Clash Formal will also connect and contribute.

Project Alliance

The project is part of the Ecosystem formally verifiable IT (EvIT), a research mission of Cyberagentur. It is maintained by QBayLogic.