An overview of the improvements in the latest Liquid Haskell release

An experience report of a somewhat large refactoring of Liquid Haskell

An experience report on plugin upgrades

A revamp of the mechanism for introducing assumptions

Embark with the High Assurance Software Group for a guided tour through the stages of a smart-contract audit, secret weapon included.

Announcement of smtlib-backends, a Haskell library providing a generic interface for interacting with SMT solvers using SMT-LIB

On a previous post, we explained how to write tests for stateful systems using traces — sequences of stateful actions — that can be combined and modified to write complex test cases easily and transparently. This post elaborates on the combinators used to generate new traces from…

New features to understand old verification failures

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.

How to automatically inject attacks and faults in safety tests using random traces.

On the relevance of Liquid Haskell in programming languages

How to use the Makam metalanguage to implement an executable formal semantics for a simple language.