Sponsors

The SMT workshop is sponsored by AdaCore, Ethereum Foundation, Informal Systems, and Runtime Verification.

AdaCore

SPARK is a software development technology specifically designed for engineering high-reliability applications.

RecordFlux is a tool for formal message specification and generation of verifiable binary parsers and message generators.

Informal Systems

Apalache is an alternative to TLC for checking TLA+ specifications. While TLC is an explicit-state model checker, Apalache is a symbolic model checker. It checks safety for bounded executions and inductive invariants for unbounded executions, assuming that all data structures are finite. The tool leverages the SMT solver Z3, from Microsoft Research.

There are some tutorials on how to use it. The Entry-level Tutorial assumes no prior knowledge of TLA+ or PlusCal. More tutorials are available on the Tutorials Page.

Apalache is still experimental, so be prepared to use the command-line and to help us discover bugs. TLA+ enthusiasts may find this model checker efficient, for example, when their spec contains many constraints over integers. The first version of Apalache was developed by Igor Konnov, Jure Kukovec and Thanh Hai Tran at TU Wien and Inria Nancy. Apalache is actively developed at Informal Systems by Shon Feder, Igor Konnov, Jure Kukovec, Gabriela Mafra, Rodrigo Otoni, and Thomas Pani.

Informal Systems is using Apalache to check blockchain protocols and test them with the tool Modelator.

Runtime Verification

Runtime Verification uses SMT technologies for symbolic model checking of programs. We use the K Framework to give Matching Logic semantics to programming languages, and to symbolically execute them against a specification and prove their correctness. Matching Logic is a first-order formalism, and the inference system for First Order Logic is sound for it, meaning that many SMT solvers can be used with very little effort to decide unsatisfiability of Matching Logic formulae. The K Framework also uses SMT checkers for sort inference on K definitions themselves. Instead of writing a sort inference algorithm ourselves, we encode the sort inference problem as a set of constraints and have SMT checkers provide us with solutions.

Matching logic also has set variables, which makes it touch the second-order domain a bit (the set variables are free in formulae, so universally quantified at the top) and least-fixed points, so it also captures the LFP extension of FOL and separation logic. We are also using SMT solvers to automatically reason about recursive patterns, including separation-logic-style recursive heap patterns, in a collaboration with the formal systems lab at UIUC.

Our primary domain is in cryptocurrency, where be build formal semantics of the VMs used for executing smart contracts (like KEVM), then work to mechanically verify the correctness of the smart contracts. We also use other tools that utilize SMT checkers under the hood, such as the Solidity SMT Checker, to verify smart contract correctness.