High Assurance Software
Automating the verification of correct behaviour in complex systems.
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
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…
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
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…
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.