17 September 2026
Restoring type class support in Liquid Haskell
An internship experience report on reenabling type class support in Liquid Haskell
high-assurance
23 July 2026
Five years of Cardano smart-contract audits: a retrospective
A retrospective on five years and twenty-plus Cardano smart-contract audits at Tweag.
11 June 2026
Writing static checks to an unsuspecting library with Liquid Haskell
A self-contained example showcasing formal verification using Liquid Haskell
20 February 2025
From minimal skeletons to comprehensive transactions with cooked-validators
cooked-validators is a Haskell library to write offchain code and conduct testing activities over Cardano smart contracts. One of its main features is to create fully-fledged transactions from simple declarative skeletons.
22 June 2023
Assumptions for Liquid Haskell in the large
A revamp of the mechanism for introducing assumptions
11 May 2023
A journey through the auditing process of a smart contract
Embark with the High Assurance Software Group for a guided tour through the stages of a smart-contract audit, secret weapon included.
27 April 2023
Type-safe data processing pipelines
Using type-level dependency tags to verify a Haskell pipeline.
14 February 2023
smtlib-backends: faster SMT-LIB-based Haskell interface to SMT solvers
Announcement of smtlib-backends, a Haskell library providing a generic interface for interacting with SMT solvers using SMT-LIB
14 October 2022
Testing stateful systems, part two: Linear Temporal Logic
21 July 2022
A dialogue with Liquid Haskell
New features to understand old verification failures
1 July 2022
Introducing Pirouette 2: formal methods for smart contracts
The new Pirouette 2 introduces formal method techniques to the verification of smart contracts; in this post we focus particularly in how incorrectness logic helps this goal.
25 March 2022
Our first audit of Minswap and the aftermath
26 January 2022
A Case Study on Correctness and Safety Testing of Stateful Systems
How to automatically inject attacks and faults in safety tests using random traces.
19 January 2022
Why Liquid Haskell matters
On the relevance of Liquid Haskell in programming languages