About Us Products Articles News Contact Support

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:

Level 0 - which is Wolfram computation engine itself,
Level 1 - that deals with the general notion of deduction with custom transformation rules,
Level 2 - providing high-level verification operations for validation and satisfiability checks with support for custom theorems, basic set operations, predicates and quantified expressions,
Level 3 - offering complete system/software modeling environment inspired by Event-B.

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

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.

Package:	Purpose:
FormalAssistant-1.0.nb	Source package: Mathematica notebook file containing the implementation of Formal Assistant with integrated documentation and extensive set of examples.

Questions?

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