Community

Communities

Repositories

ghc-typlits-proof-assist: A GHC plugin enabling the developer to rely on an external proof assistant (Agda, Rocq or Lean) to prove statements that are either impossible or too difficult to prove with the existing constraint solver of GHC.
clash-crypto: A hardware design library for cryptographic primitives written in Clash.

Talks

Ökosystem Vertrauenswürdige IT – Projekt Clash Formal
20 January 2025, Project Kickoff
Slides (EN), Slides (DE)
Formale Verifikation von Hardware
15 May 2025, Security and Innovation in Cyberspace
Slides (DE)
ghc-typelits-proof-assist: A Haskell Plugin for Type-Nat Proofs
6 June 2025, Haskell Implementors Workshop (Lightning Talk)
Slides (EN), Video (EN)
Experience Report: Translating Haskell / Clash to Coq / Agda / Liquid Haskell
6 June 2025, Haskell Implementors Workshop (Lightning Talk)
Slides (EN), Video (EN)
Synergizing Functional Programming, Proofs & Hardware Design
6 October 2025, FOMSESS Annual Workshop
Slides (EN)

Challenges

The Clash UDBC Arbiter Verification Challenge: The challenge is to formally verify that the given implementation satisfies a given list of safety and security properties for any number of clients and all potential data types.
TSL Kitchen Timer Verification: The Clash hardware implementation of the timer has been claimed to satisfy the given temporal specification by construction, but the specification cannot be verified against the synthesized or any other manually given specification yet. The challenge is to connect the specification with a Clash implementation using a verification system that is capable of verifying the design against the specified properties.

Acknowledgements

This project would be impossible without the availability of a vast range of already existing open source software and hardware projects indirectly contributing to the success of the project as well. Some of the most influential projects are: