Inspirel banner

Formal Methods Toolkit

Formal Methods Toolkit is a set of extension packages for Mathematica, supporting software engineering activities related to modeling, verification and code generation of correct software systems. Even though not limited to any particular domain, FMT was motivated by the needs of embedded and safety-critical projects.

The major features of FMT are:

Formal Methods Toolkit relies on Mathematica as its underlying computing platform and is portable between Linux, Mac OS X and Windows. Both content-rich, interactive workflows with notebook files and batch processing with Wolfram scripting are supported.

Prior experience with Wolfram and Mathematica is not necessary to use and benefit from FMT, although some knowledge of that platform can bring significant added value with advanced modeling techniques and automation capabilities.

Example gallery

Check the gallery of example screenshots to see how FMT can help you create better software:



FMT book cover

"Formal Methods Toolkit" by Maciej Sobczak

This book is a complete FMT manual that describes its features and usage patterns.

Support independent publishing: Buy this book on Lulu.

The on-line version of this book is available as well.

Apart from this comprehensive manual, a set of example notebooks for interactive exploration is included as part of the downloadable package below.

Video materials

FMT YouTube playlist

The YouTube playlist presenting the idea to use Mathematica for formal methods.

These videos explain not only how to use FMT, but also what features of Mathematica and Wolfram were used as a basis for its implementation.

Development blog

The articles linked below document the reasoning behind new FMT features. All features listed below are part of the FMT 2.0 release.

Implementing Logic Reachability Checks

Basic Support For Ghost Variables

Supporting Quantified Statements, Part 1

Supporting Quantified Statements, Part 2

Supporting Quantified Statements, Part 3

Supporting Quantified Statements, Part 4

Supporting Quantified Statements, Part 5

Fixing Loops

Supporting Loop Invariants

Ad Hoc Ghosts and Loop Variants

Loops and Quantified Statements

Licensing and Download

Formal Methods Toolkit packages are available in two variants:



Wolfram source packages with example Mathematica notebook files and comprehensive set of unit tests.


Need more information about the FMT project? Do not hesitate to ask.