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.