17 September 2026
Restoring type class support in Liquid Haskell
An internship experience report on reenabling type class support in Liquid Haskell
formal-methods
10 September 2026
Are we formal proofs yet? On formal proofs of programs with coding agents
An experiment in constraining coding agent output with formal proofs
11 June 2026
Writing static checks to an unsuspecting library with Liquid Haskell
A self-contained example showcasing formal verification using Liquid Haskell
11 September 2025
Qualified Imports and Alias Resolution in Liquid Haskell
The story of how I implemented qualified aliases in Liquid Haskell
20 March 2025
A hundred pull requests for Liquid Haskell
An overview of the improvements in the latest Liquid Haskell release
6 February 2025
The refactoring of a Haskell codebase
An experience report of a somewhat large refactoring of Liquid Haskell
30 May 2024
Liquid Haskell through the compilers
An experience report on plugin upgrades
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.
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.
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
28 November 2019
How to make your papers run: Executable formal semantics for your language
How to use the Makam metalanguage to implement an executable formal semantics for a simple language.