Inspirel banner

Formal Assistant

Formal Assistant is a modular and flexible deduction and proof system, built on top of functionality offered by Wolfram, that can support various activities related to formal methods, modeling and software verification.

Formal Assistant offers several layers of functionality, that can be used separately, freely mixed in an engineering document, or as foundations for higher-level processes:

Formal Assistant offers many levels of verbosity and supports parallel execution of generated proofs on multiple computing kernels, if the target platforms allows it.

Formal Assistant is implemented as a Mathematica notebook. As such, it is portable and works on any system supporting Mathematica.

Video materials

Formal Assistant YouTube playlist

YouTube playlist presenting the Formal Assistant.

Licensing and Download

Formal Assistant is a free software, distributed under the GPL v. 3.0 license or other, if requested.
See the notebook content for detailed terms of use and compatibility notes.




Source package: Mathematica notebook file containing the implementation of Formal Assistant with integrated documentation and extensive set of examples.


Need more information about Formal Assistant? Do not hesitate to ask.