Automating the verification of correct behaviour in complex systems.

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.

Using type-level dependency tags to verify a Haskell pipeline.

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.

What Happened On the morning of the 22nd of March, 2022, we were notified about the existence of an unknown critical vulnerability on one of Minswap’s contracts. Everyone here on the audit team was dismayed, since we had conducted an audit for Minswap not long before. We found…

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

On the relevance of Liquid Haskell in programming languages