Open Source Tools for System Correctness
Automata: Automata (opens in new tab) is a .NET library that provides algorithms for composing and analyzing regular expressions, automata, and transducers. In addition to classical word automata, it also includes algorithms for analysis of tree automata and tree transducers. The library covers algorithms over finite alphabets as well as their symbolic counterparts. Predicates can be supported by an SMT solver as a plugin.
Corral Program Verifier: Corral (opens in new tab) is a whole-program analysis tool for Boogie (opens in new tab) programs. Corral uses goal-directed symbolic search techniques to find assertion violations. It leverages the automated theorem prover Z3. Corral, by default, does a bounded search up to a recursion depth and fixed number of context switches. Corral also supports the Duality (opens in new tab) extension for constructing inductive proofs of correctness of programs.
Ivy: IVy (opens in new tab) is a tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Lean Theorem Prover: Lean (opens in new tab) is an open source theorem prover and programming language. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.
P/P#: P/P# (opens in new tab) are languages for asynchronous event-driven programming that allow the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P/P# unifies modeling and programming into one activity for the programmer. Not only can a P/P# program be compiled into executable code, but it can also be validated using systematic testing.
Project Everest: Everest (opens in new tab) is the combination of the following projects, that together are used to prove correct/secure and generate a C library that efficiently implements TLS 1.3
- F* (opens in new tab), a verification-oriented dialect of ML
- HACL* (opens in new tab), a verified library of cryptographic primitives written in F*
- KreMLin (opens in new tab), a compiler from a subset of F* to C
- miTLS (opens in new tab), an implementation of the TLS protocol, written in F*
- Vale (opens in new tab), a domain-specific language designed to implement verified cryptographic primitives in assembly
TLA+: TLA+ (opens in new tab) is based on the idea that the best way to describe things formally is with simple mathematics, and that a specification language should contain as little as possible beyond what is needed to write simple mathematics precisely. TLA+ is especially well suited for writing high-level specifications of concurrent and distributed systems.
Network Verification: Firewall Checker (opens in new tab) is a firewall analysis library using the Z3 SMT Solver from Microsoft Research. Includes console applications to check the equivalence of two firewalls, or analyze the action of a firewall on a single packet. It was developed for use inside Microsoft Azure to analyze changes to Windows Firewall generation logic. It is one part of much larger effort to verify aspects of data center configuration and behavior.
Verisol: VeriSol (opens in new tab) (Verifier for Solidity) is a prototype formal verification and analysis system for smart contracts developed in the popular Solidity (opens in new tab) programming language. It is based on translating programs in Solidity language to programs in Boogie (opens in new tab) intermediate verification language, and then leveraging the verification toolchain for Boogie programs.
Z3 Theorem Prover: Z3 (opens in new tab) is an automated theorem prover in the satisfiability-modulo-theories (SMT) family, under research/development for over a decade at Microsoft Research and widely deployed in the industry for a wide range of uses, from program verification to product configuration.