Commit to marriage with TLA+ pt.2
The second part of the conspect of the “Intoduction to TLA+” course by Leslie Lamport.
Blogs
Do not die hard with TLA+ pt.1
The first part of the conspect of the “Intoduction to TLA+” course by Leslie Lamport.
Small and Big Step Semantics
This blog outlines small-step and big-step semantics, their differences, and applications in analyzing computer programs.
LTL and CTL Applications for Smart Contracts Security
In this blog we explore linear temporal logic as well as computation tree logic, and how we could use them to verify smart-contracts.
Why use formal specification
This blog explores the benefits of formal specification in the context of program verification.