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, we 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.

Our particular focus lies on the formal verification of functional hardware designs together with their hardware-to-software interfaces, a. A research area which still is less explored than for example pure functional program verification. Our 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.

The 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 build on these connections to make them applicable and approachable at every level of an IT hardware-to-software stack.

Clash Formal is operated by QBayLogic B.V.