FM Playground

---

A web-based platform for formal methods tools, providing an easy-to-use interface for model checking, formal verification, and synthesis. Currently, Limboole, Z3, nuXmv, Alloy, dafny, and Spectra are integrated into the platform. Due to the modular architecture, more tools can be added easily.

Overview and Examples

We started a small overview of the features of the FM Playground and how to use it. The video playlist is available on YouTube

For more updates, examples, and tutorials, please visit the formal-methods.net website.

Development

Requirements

• Python >= 3.10.0
• Node >= 20.0.0
• PostgreSQL >= 15.0 (optional) - use sqlite3 for development
• Docker >= 20.10.0 (optional)
• Docker Compose >= 1.27.0 (optional)

Installation

• [TODO]

Development Server

For local development, you can use the following script to start the development server:

• Unix-based systems (Linux, macOS): ./start_dev.sh
• Windows: start_dev.ps1 It will ask you which services you want to start (frontend, backend, tools). You can select multiple services by separating them with commas.

NOTE: In windows, you might experience issues with the script execution policy.

Docker

• [TODO]

Docker Compose

• Copy the .env.example file to .env and update the environment variables as needed:

cp .env.example .env

• Run the following command:

docker compose up -d

Contributing

TODO: Create a contributing guide

License

This project is licensed under the MIT License.

Third-Party Licenses

• Limboole - https://github.com/maximaximal/limboole/blob/master/LICENSE
• Z3 - https://github.com/Z3Prover/z3/blob/master/LICENSE.txt
• nuXmv - https://nuxmv.fbk.eu/downloads/LICENSE.txt
• Alloy - https://github.com/AlloyTools/org.alloytools.alloy/blob/master/LICENSE
• Dafny - https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt
• Spectra - https://github.com/SpectraSynthesizer/spectra-synt/blob/master/LICENSE