The Formal Methods Tools project is dedicated to developing, maintaining, and promoting tools that support the application of formal methods in software engineering. Our goal is to make formal verification, specification, and analysis techniques accessible and practical for both researchers and practitioners.
+
The Formal Methods Tools project is dedicated to developing, maintaining, and promoting tools that support the application of formal methods in software engineering. The goal of this website is to make formal verification, specification, and analysis techniques accessible and practical for both researchers and practitioners.
Key Objectives
Provide a comprehensive list of tools for formal methods.
[ Not Maintained Since 2012 ] BLAST (Berkeley Lazy Abstraction Software verification Tool) is a …
+ BLAST
@@ -363,7 +361,7 @@ APIs and Bindings This …
Made with ♥ using Hugo
- Built
+ Built
diff --git a/index.xml b/index.xml
index 4e2761b..d53cd99 100644
--- a/index.xml
+++ b/index.xml
@@ -13,7 +13,7 @@
https://fmtools.fyi/about/
Sat, 07 Jun 2025 00:00:00 +0000https://fmtools.fyi/about/
- <p>The Formal Methods Tools project is dedicated to developing, maintaining, and promoting tools that support the application of formal methods in software engineering. Our goal is to make formal verification, specification, and analysis techniques accessible and practical for both researchers and practitioners.</p>
<h2 id="key-objectives">Key Objectives</h2>
<ul>
<li>Provide a comprehensive list of tools for formal methods.</li>
<li>Group tools by rich metadata to support collaboration and boost tools’ strengths.</li>
<li>Foster a collaborative community for tool development and support.</li>
</ul>
<h2 id="whos-behind-this">Who’s Behind This?</h2>
<p>Howdy. My name is Landon Taylor. I sometimes go by mossBiscuits.
This is one of my hobby projects.
I have a passion for formal methods. When I started learning about verification, there was a sharp barrier to entry due partially to the sprawl of content online.
I wanted to solve this problem, so I have been chipping away at this website for a while now.</p>
+ <p>The Formal Methods Tools project is dedicated to developing, maintaining, and promoting tools that support the application of formal methods in software engineering. The goal of this website is to make formal verification, specification, and analysis techniques accessible and practical for both researchers and practitioners.</p>
<h2 id="key-objectives">Key Objectives</h2>
<ul>
<li>Provide a comprehensive list of tools for formal methods.</li>
<li>Group tools by rich metadata to support collaboration and boost tools’ strengths.</li>
<li>Foster a collaborative community for tool development and support.</li>
</ul>
<h2 id="whos-behind-this">Who’s Behind This?</h2>
<p>Howdy. My name is Landon Taylor. I sometimes go by mossBiscuits.
This is one of my hobby projects.
I have a passion for formal methods. When I started learning about verification, there was a sharp barrier to entry due partially to the sprawl of content online.
I wanted to solve this problem, so I have been chipping away at this website for a while now.</p>Alt-Ergo
@@ -29,6 +29,13 @@
https://fmtools.fyi/tools/sat-smt/bitwuzla/<p>Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays, uninterpreted functions and their combinations.</p>
+
+ BLAST
+ https://fmtools.fyi/tools/mc/blast/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/blast/
+ <p>
<div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
<span style="display:none">[</span>
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2012</span>
<span style="display:none">]</span>
</div>
BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool for C language that solves the reachability problem, i.e. whether a given program location can be reached from an entry point (main function) by a valid execution.</p>
+ Boolector
https://fmtools.fyi/tools/sat-smt/boolector/
@@ -43,6 +50,27 @@
https://fmtools.fyi/tools/sat-smt/cadical/<p>CaDiCaL is a simplified satisfiability solver.</p>
+
+ CADP
+ https://fmtools.fyi/tools/mc/cadp/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/cadp/
+ <p><div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span>
<span style="display:none">[</span>
<span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span>
<span style="display:none">] </span>
</div>
CADP (“Construction and Analysis of Distributed Processes”, formerly known as “CAESAR/ALDEBARAN Development Package”) is a toolbox for the design of asynchronous concurrent systems, such as communication protocols, distributed systems, asynchronous circuits, multiprocessor architectures, web services, etc.</p>
+
+
+ Caesar
+ https://fmtools.fyi/tools/prob/caesar/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/prob/caesar/
+ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p>
+
+
+ CGAAL
+ https://fmtools.fyi/tools/mc/cgaal/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/cgaal/
+ <p>CGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game structures (CGSs).</p>
+ Colibri
https://fmtools.fyi/tools/sat-smt/colibri/
@@ -57,6 +85,13 @@
https://fmtools.fyi/tools/prob/comics/<p>COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for discrete-time Markov Chains (DTMCs).</p>
+
+ Concuerror
+ https://fmtools.fyi/tools/mc/concuerror/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/concuerror/
+ <p>Concuerror is a stateless model checking tool for Erlang programs.</p>
+ Contribute
https://fmtools.fyi/contribute/
@@ -64,6 +99,13 @@
https://fmtools.fyi/contribute/<p>Instructions coming soon. Please see <a href="https://gitmoss.fyi/fmtools/content/wiki/Contribute" target="_blank" >https://gitmoss.fyi/fmtools/content/wiki/Contribute</a> for temporary instructions.</p>
<h2 id="quick-links">Quick Links</h2>
<ul>
<li>Request addding a tool: <a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2fadd_tool.md" target="_blank" >Submit Git Issue</a></li>
<li>Request fixing a tool: <a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md" target="_blank" >Submit Git Issue</a></li>
</ul>
+
+ CPAchecker
+ https://fmtools.fyi/tools/mc/cpachecker/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/cpachecker/
+ <p><div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span>
<span style="display:none">[</span>
<span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span>
<span style="display:none">] </span>
</div>
CPAchecker is a tool for configurable software verification.</p>
+ CryptoMiniSat
https://fmtools.fyi/tools/sat-smt/cryptominisat/
@@ -92,6 +134,13 @@
https://fmtools.fyi/tools/sat-smt/dreal/<p>
<div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
<span style="display:none">[</span>
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span>
<span style="display:none">]</span>
</div>
dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions.</p>
+
+ DSCheck
+ https://fmtools.fyi/tools/mc/dscheck/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/dscheck/
+ <p>DSCheck is an experimental model checker for testing concurrent OCaml programs.</p>
+ E
https://fmtools.fyi/tools/sat-smt/e/
@@ -99,6 +148,27 @@
https://fmtools.fyi/tools/sat-smt/e/<p>E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with equality.</p>
+
+ Eldarica
+ https://fmtools.fyi/tools/mc/eldarica/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/eldarica/
+ <p>Eldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs.</p>
+
+
+ ESBMC
+ https://fmtools.fyi/tools/mc/esbmc/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/esbmc/
+ <p>ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.</p>
+
+
+ Geyser
+ https://fmtools.fyi/tools/mc/geyser/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/geyser/
+ <p>Geyser is a simple symbolic model checker for propositional transition system systems.</p>
+ Glucose
https://fmtools.fyi/tools/sat-smt/glucose/
@@ -106,6 +176,48 @@
https://fmtools.fyi/tools/sat-smt/glucose/<p>Glucose is a SAT solver.</p>
+
+ IMITATOR
+ https://fmtools.fyi/tools/mc/imitator/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/imitator/
+ <p>IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.</p>
+
+
+ ImSpin
+ https://fmtools.fyi/tools/mc/imspin/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/imspin/
+ <p>ImSpin is a frontend for the <a href="../spin" >SPIN</a> model checker, providing an environment for users engaged in model checking tasks.</p>
+
+
+ Intrepyd
+ https://fmtools.fyi/tools/mc/intrepyd/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/intrepyd/
+ <p>
<div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
<span style="display:none">[</span>
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span>
<span style="display:none">]</span>
</div>
Intrepyd is a python module that provides a simulator and a model checker in form of a rich API, to allow the rapid prototyping of formal methods algorithms for the rigorous analysis of circuits, specifications, models.</p>
+
+
+ JANI
+ https://fmtools.fyi/tools/mod/jani/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mod/jani/
+ <p>The JANI specification defines the jani-model model interchange format and the jani-interaction tool interaction and automation protocol.</p>
+
+
+ Kind 2
+ https://fmtools.fyi/tools/mc/kind2/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/kind2/
+ <p>Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems.</p>
+
+
+ LEAN
+ https://fmtools.fyi/tools/sat-smt/lean/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/sat-smt/lean/
+ <p>cvc5 is an automatic theorem prover for SMT problems.</p>
+ Lingeling
https://fmtools.fyi/tools/sat-smt/lingeling/
@@ -113,12 +225,47 @@
https://fmtools.fyi/tools/sat-smt/lingeling/<p>Lingeling is a SAT solver.</p>
+
+ LTSA
+ https://fmtools.fyi/tools/mc/ltsa/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/ltsa/
+ <p>
<div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
<span style="display:none">[</span>
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2018</span>
<span style="display:none">]</span>
</div>
LTSA is a verification tool for concurrent systems. It mechanically checks that the specification of a concurrent system satisfies the properties required of its behaviour. In addition, LTSA supports specification animation to facilitate interactive exploration of system behaviour.</p>
+
+
+ LTSmin
+ https://fmtools.fyi/tools/mc/ltsmin/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/ltsmin/
+ <p>LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the toolset was extended to a a full (LTL/CTL/μ-calculus) model checker, while maintaining its language-independent characteristics.</p>
+ MathSAT
https://fmtools.fyi/tools/sat-smt/mathsat/
Sat, 07 Jun 2025 00:00:00 +0000https://fmtools.fyi/tools/sat-smt/mathsat/
- <p><div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span>
<span style="display:none">[</span>
<span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span>
<span style="display:none">] </span>
</div>
MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p>
+ <p><div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span>
<span style="display:none">[</span>
<span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span>
<span style="display:none">] </span>
</div>
MathSAT is an SMT solver supporting a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, and arrays) and functionalities (including e.g. computation of Craig interpolants, extraction of unsatisfiable cores, generation of models and proofs, and the ability of working incrementally).</p>
+
+
+ mcltl-rs
+ https://fmtools.fyi/tools/mc/mcltlrs/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/mcltlrs/
+ <div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
<span style="display:none">[</span>
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span>
<span style="display:none">]</span>
</div>
<p>mcltl-rs is an experimental model checker for LTL written in Rust.</p>
+
+
+ mCRL2
+ https://fmtools.fyi/tools/mc/mcrl2/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/mcrl2/
+ <p>mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols.</p>
+
+
+ Mercury
+ https://fmtools.fyi/tools/mc/mercury/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/mercury/
+ <p>
<div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
<span style="display:none">[</span>
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span>
<span style="display:none">]</span>
</div>
Mercury is a Model Checker developed for multicore, multiprocessors machine with shared memory.</p>MiniSat
@@ -134,6 +281,34 @@
https://fmtools.fyi/license/<p>MIT License</p>
<p>Copyright (c) 2025 Landon Taylor.</p>
<p>Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the “Software”), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:</p>
+
+ Momba
+ https://fmtools.fyi/tools/mod/momba/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mod/momba/
+ <p>Momba is a Python framework for dealing with quantitative models centered around the <a href="../jani" >JANI-model</a> interchange format.</p>
+
+
+ MUNTA
+ https://fmtools.fyi/tools/mc/munta/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/munta/
+ <p>
<div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
<span style="display:none">[</span>
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2020</span>
<span style="display:none">]</span>
</div>
MUNTA is a model checker for the popular realtime systems modeling formalism of Timed Automata</p>
+
+
+ NuSMV
+ https://fmtools.fyi/tools/mc/nusmv/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/nusmv/
+ <p>NuSMV is a symbolic model checker.</p>
+
+
+ NuXMV
+ https://fmtools.fyi/tools/mc/nuxmv/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/nuxmv/
+ <p><div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span>
<span style="display:none">[</span>
<span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span>
<span style="display:none">] </span>
</div>
nuXmv is a symbolic model checker for the analysis of synchronous finite-state and infinite-state systems.</p>
+ OpenSMT
https://fmtools.fyi/tools/sat-smt/opensmt/
@@ -148,6 +323,13 @@
https://fmtools.fyi/tools/sat-smt/parafrost/<p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li>
<li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li>
<li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li>
<li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li>
</ul>
+
+ Pnmc
+ https://fmtools.fyi/tools/mc/pnmc/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/pnmc/
+ <p>Pnmc is a symbolic model checker for Petri nets.</p>
+ PRISM
https://fmtools.fyi/tools/prob/prism/
@@ -162,6 +344,13 @@
https://fmtools.fyi/privacy/<p>This website does not collect or track any personal data from visitors. No cookies, personalized analytics, or tracking scripts are used. No ads are shown on this website, and there is no money to be made from this project.</p>
<p>If you choose to contribute content (including emails, issues, and pull requests), any information you voluntarily provide may be stored as part of the website’s content and source code. Only the data you explicitly submit will be saved, and data is not sold by the website’s owner. Due to the public nature of its disclosure, this information is not considered private and may be used by the general public as allowed by respective laws and policies. Your privacy is respected, and no unnecessary data is collected or shared.</p>
+
+ pyPL
+ https://fmtools.fyi/tools/mc/pypl/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/pypl/
+ <p>pyPL is a naive model generator, model checker and theorem prover.</p>
+ Q3B
https://fmtools.fyi/tools/sat-smt/q3b/
@@ -176,6 +365,20 @@
https://fmtools.fyi/tools/sat-smt/riss/<p>
<div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
<span style="display:none">[</span>
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2017</span>
<span style="display:none">]</span>
</div>
Riss is a SAT solving tool collection.</p>
+
+ Roméo
+ https://fmtools.fyi/tools/mc/romeo/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/romeo/
+ <p>Romeo allows the modelling of complex systems using extensions of time Petri nets.</p>
+
+
+ Rumur
+ https://fmtools.fyi/tools/mc/rumur/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/rumur/
+ <p>Rumur is a model checker.</p>
+ Sally
https://fmtools.fyi/tools/mc/sally/
@@ -183,6 +386,13 @@
https://fmtools.fyi/tools/mc/sally/<p>Sally is a model checker for infinite state systems described as transition systems.</p>
+
+ SM(P/)T
+ https://fmtools.fyi/tools/mc/smpt/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/smpt/
+ <p>SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).</p>
+ SMT-RAT
https://fmtools.fyi/tools/sat-smt/smt-rat/
@@ -197,6 +407,20 @@
https://fmtools.fyi/tools/sat-smt/smtinterpol/<p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li>
</ul>
+
+ SpaceEx
+ https://fmtools.fyi/tools/mc/spaceex/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/spaceex/
+ <p>The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification in continuous and hybrid systems.</p>
+
+
+ Spin
+ https://fmtools.fyi/tools/mc/spin/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/spin/
+ <p>Spin is a model checker for multi-threaded software.</p>
+ STAMINA
https://fmtools.fyi/tools/prob/stamina/
@@ -204,6 +428,13 @@
https://fmtools.fyi/tools/prob/stamina/<p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p>
+
+ stateright
+ https://fmtools.fyi/tools/mc/stateright/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/stateright/
+ <p><code>stateright</code> is a Rust library for model checking systems, with an emphasis on distributed systems.</p>
+ Storm
https://fmtools.fyi/tools/prob/storm/
@@ -218,6 +449,34 @@
https://fmtools.fyi/tools/sat-smt/stp/<p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li>
</ul>
+
+ TAPAAL
+ https://fmtools.fyi/tools/mc/tapaal/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/tapaal/
+ <p>TAPAAL is a tool for verification of timed-arc petri nets</p>
+
+
+ TimeSolver
+ https://fmtools.fyi/tools/mc/timesolver/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/timesolver/
+ <p>
<div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
<span style="display:none">[</span>
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2019</span>
<span style="display:none">]</span>
</div>
TimeSolver is a Model Checker for timed automata that uses pes (predicate equation systems).</p>
+
+
+ TLA+
+ https://fmtools.fyi/tools/mod/tlaplus/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mod/tlaplus/
+ <p>TLA+ is a high-level language for modeling programs and systems–especially concurrent and distributed ones.</p>
+
+
+ Uppaal
+ https://fmtools.fyi/tools/mc/uppaal/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/uppaal/
+ <p><div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span>
<span style="display:none">[</span>
<span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span>
<span style="display:none">] </span>
</div>
Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).</p>
+ Vampire
https://fmtools.fyi/tools/sat-smt/vampire/
diff --git a/inputs/heyvl/index.html b/inputs/heyvl/index.html
new file mode 100644
index 0000000..d2f86e4
--- /dev/null
+++ b/inputs/heyvl/index.html
@@ -0,0 +1,131 @@
+
+
+
+
+
+
+
+
+HeyVL | Formal Methods Tools
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 🚧 This site is a work in progress. Don’t be shy to submit an issue or pull request 🚧
+
+
Romeo allows the modelling of complex systems using extensions of time Petri nets.
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/licenses/gpl/index.xml b/licenses/gpl/index.xml
new file mode 100644
index 0000000..039afb5
--- /dev/null
+++ b/licenses/gpl/index.xml
@@ -0,0 +1,19 @@
+
+
+
+ GPL on Formal Methods Tools
+ https://fmtools.fyi/licenses/gpl/
+ Recent content in GPL on Formal Methods Tools
+ Hugo
+ en-us
+ Sat, 07 Jun 2025 00:00:00 +0000
+
+
+ Roméo
+ https://fmtools.fyi/tools/mc/romeo/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/romeo/
+ <p>Romeo allows the modelling of complex systems using extensions of time Petri nets.</p>
+
+
+
diff --git a/licenses/gplv2/index.html b/licenses/gplv2/index.html
index 171804d..80881c8 100644
--- a/licenses/gplv2/index.html
+++ b/licenses/gplv2/index.html
@@ -139,6 +139,23 @@ APIs and Bindings This tool is available through the following …
+
TLA+ is a high-level language for modeling programs and systems–especially concurrent and …
+
+
+
diff --git a/licenses/gplv2/index.xml b/licenses/gplv2/index.xml
index 007e6bb..2907cd5 100644
--- a/licenses/gplv2/index.xml
+++ b/licenses/gplv2/index.xml
@@ -36,5 +36,19 @@
https://fmtools.fyi/tools/mc/sally/<p>Sally is a model checker for infinite state systems described as transition systems.</p>
+
+ TAPAAL
+ https://fmtools.fyi/tools/mc/tapaal/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/tapaal/
+ <p>TAPAAL is a tool for verification of timed-arc petri nets</p>
+
+
+ TLA+
+ https://fmtools.fyi/tools/mod/tlaplus/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mod/tlaplus/
+ <p>TLA+ is a high-level language for modeling programs and systems–especially concurrent and distributed ones.</p>
+
diff --git a/licenses/gplv3/index.html b/licenses/gplv3/index.html
index 193450f..c46c5a4 100644
--- a/licenses/gplv3/index.html
+++ b/licenses/gplv3/index.html
@@ -107,6 +107,22 @@
[ Closed-Source Tool ] Uppaal is an integrated tool environment for modeling, validation and …
+
+
+
diff --git a/maintenance/actively-maintained/index.xml b/maintenance/actively-maintained/index.xml
index c3797ab..3fda198 100644
--- a/maintenance/actively-maintained/index.xml
+++ b/maintenance/actively-maintained/index.xml
@@ -29,6 +29,27 @@
https://fmtools.fyi/tools/sat-smt/cadical/<p>CaDiCaL is a simplified satisfiability solver.</p>
+
+ CADP
+ https://fmtools.fyi/tools/mc/cadp/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/cadp/
+ <p><div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span>
<span style="display:none">[</span>
<span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span>
<span style="display:none">] </span>
</div>
CADP (“Construction and Analysis of Distributed Processes”, formerly known as “CAESAR/ALDEBARAN Development Package”) is a toolbox for the design of asynchronous concurrent systems, such as communication protocols, distributed systems, asynchronous circuits, multiprocessor architectures, web services, etc.</p>
+
+
+ Caesar
+ https://fmtools.fyi/tools/prob/caesar/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/prob/caesar/
+ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p>
+
+
+ CGAAL
+ https://fmtools.fyi/tools/mc/cgaal/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/cgaal/
+ <p>CGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game structures (CGSs).</p>
+ Colibri
https://fmtools.fyi/tools/sat-smt/colibri/
@@ -36,6 +57,20 @@
https://fmtools.fyi/tools/sat-smt/colibri/<p>Colibri is an SMT solver.</p>
+
+ Concuerror
+ https://fmtools.fyi/tools/mc/concuerror/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/concuerror/
+ <p>Concuerror is a stateless model checking tool for Erlang programs.</p>
+
+
+ CPAchecker
+ https://fmtools.fyi/tools/mc/cpachecker/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/cpachecker/
+ <p><div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span>
<span style="display:none">[</span>
<span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span>
<span style="display:none">] </span>
</div>
CPAchecker is a tool for configurable software verification.</p>
+ CryptoMiniSat
https://fmtools.fyi/tools/sat-smt/cryptominisat/
@@ -50,6 +85,13 @@
https://fmtools.fyi/tools/sat-smt/cvc5/<p>cvc5 is an automatic theorem prover for SMT problems.</p>
+
+ DSCheck
+ https://fmtools.fyi/tools/mc/dscheck/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/dscheck/
+ <p>DSCheck is an experimental model checker for testing concurrent OCaml programs.</p>
+ E
https://fmtools.fyi/tools/sat-smt/e/
@@ -57,6 +99,27 @@
https://fmtools.fyi/tools/sat-smt/e/<p>E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with equality.</p>
+
+ Eldarica
+ https://fmtools.fyi/tools/mc/eldarica/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/eldarica/
+ <p>Eldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs.</p>
+
+
+ ESBMC
+ https://fmtools.fyi/tools/mc/esbmc/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/esbmc/
+ <p>ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.</p>
+
+
+ Geyser
+ https://fmtools.fyi/tools/mc/geyser/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/geyser/
+ <p>Geyser is a simple symbolic model checker for propositional transition system systems.</p>
+ Glucose
https://fmtools.fyi/tools/sat-smt/glucose/
@@ -64,6 +127,41 @@
https://fmtools.fyi/tools/sat-smt/glucose/<p>Glucose is a SAT solver.</p>
+
+ IMITATOR
+ https://fmtools.fyi/tools/mc/imitator/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/imitator/
+ <p>IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.</p>
+
+
+ ImSpin
+ https://fmtools.fyi/tools/mc/imspin/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/imspin/
+ <p>ImSpin is a frontend for the <a href="../spin" >SPIN</a> model checker, providing an environment for users engaged in model checking tasks.</p>
+
+
+ JANI
+ https://fmtools.fyi/tools/mod/jani/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mod/jani/
+ <p>The JANI specification defines the jani-model model interchange format and the jani-interaction tool interaction and automation protocol.</p>
+
+
+ Kind 2
+ https://fmtools.fyi/tools/mc/kind2/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/kind2/
+ <p>Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems.</p>
+
+
+ LEAN
+ https://fmtools.fyi/tools/sat-smt/lean/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/sat-smt/lean/
+ <p>cvc5 is an automatic theorem prover for SMT problems.</p>
+ Lingeling
https://fmtools.fyi/tools/sat-smt/lingeling/
@@ -71,12 +169,47 @@
https://fmtools.fyi/tools/sat-smt/lingeling/<p>Lingeling is a SAT solver.</p>
+
+ LTSmin
+ https://fmtools.fyi/tools/mc/ltsmin/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/ltsmin/
+ <p>LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the toolset was extended to a a full (LTL/CTL/μ-calculus) model checker, while maintaining its language-independent characteristics.</p>
+ MathSAT
https://fmtools.fyi/tools/sat-smt/mathsat/
Sat, 07 Jun 2025 00:00:00 +0000https://fmtools.fyi/tools/sat-smt/mathsat/
- <p><div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span>
<span style="display:none">[</span>
<span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span>
<span style="display:none">] </span>
</div>
MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p>
+ <p><div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span>
<span style="display:none">[</span>
<span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span>
<span style="display:none">] </span>
</div>
MathSAT is an SMT solver supporting a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, and arrays) and functionalities (including e.g. computation of Craig interpolants, extraction of unsatisfiable cores, generation of models and proofs, and the ability of working incrementally).</p>
+
+
+ mCRL2
+ https://fmtools.fyi/tools/mc/mcrl2/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/mcrl2/
+ <p>mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols.</p>
+
+
+ Momba
+ https://fmtools.fyi/tools/mod/momba/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mod/momba/
+ <p>Momba is a Python framework for dealing with quantitative models centered around the <a href="../jani" >JANI-model</a> interchange format.</p>
+
+
+ NuSMV
+ https://fmtools.fyi/tools/mc/nusmv/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/nusmv/
+ <p>NuSMV is a symbolic model checker.</p>
+
+
+ NuXMV
+ https://fmtools.fyi/tools/mc/nuxmv/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/nuxmv/
+ <p><div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span>
<span style="display:none">[</span>
<span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span>
<span style="display:none">] </span>
</div>
nuXmv is a symbolic model checker for the analysis of synchronous finite-state and infinite-state systems.</p>OpenSMT
@@ -92,6 +225,13 @@
https://fmtools.fyi/tools/sat-smt/parafrost/<p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li>
<li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li>
<li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li>
<li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li>
</ul>
+
+ Pnmc
+ https://fmtools.fyi/tools/mc/pnmc/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/pnmc/
+ <p>Pnmc is a symbolic model checker for Petri nets.</p>
+ PRISM
https://fmtools.fyi/tools/prob/prism/
@@ -99,6 +239,27 @@
https://fmtools.fyi/tools/prob/prism/<p>PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.</p>
+
+ pyPL
+ https://fmtools.fyi/tools/mc/pypl/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/pypl/
+ <p>pyPL is a naive model generator, model checker and theorem prover.</p>
+
+
+ Roméo
+ https://fmtools.fyi/tools/mc/romeo/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/romeo/
+ <p>Romeo allows the modelling of complex systems using extensions of time Petri nets.</p>
+
+
+ Rumur
+ https://fmtools.fyi/tools/mc/rumur/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/rumur/
+ <p>Rumur is a model checker.</p>
+ Sally
https://fmtools.fyi/tools/mc/sally/
@@ -106,6 +267,13 @@
https://fmtools.fyi/tools/mc/sally/<p>Sally is a model checker for infinite state systems described as transition systems.</p>
+
+ SM(P/)T
+ https://fmtools.fyi/tools/mc/smpt/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/smpt/
+ <p>SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).</p>
+ SMT-RAT
https://fmtools.fyi/tools/sat-smt/smt-rat/
@@ -120,6 +288,20 @@
https://fmtools.fyi/tools/sat-smt/smtinterpol/<p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li>
</ul>
+
+ SpaceEx
+ https://fmtools.fyi/tools/mc/spaceex/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/spaceex/
+ <p>The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification in continuous and hybrid systems.</p>
+
+
+ Spin
+ https://fmtools.fyi/tools/mc/spin/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/spin/
+ <p>Spin is a model checker for multi-threaded software.</p>
+ STAMINA
https://fmtools.fyi/tools/prob/stamina/
@@ -127,6 +309,13 @@
https://fmtools.fyi/tools/prob/stamina/<p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p>
+
+ stateright
+ https://fmtools.fyi/tools/mc/stateright/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/stateright/
+ <p><code>stateright</code> is a Rust library for model checking systems, with an emphasis on distributed systems.</p>
+ Storm
https://fmtools.fyi/tools/prob/storm/
@@ -141,6 +330,27 @@
https://fmtools.fyi/tools/sat-smt/stp/<p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li>
</ul>
+
+ TAPAAL
+ https://fmtools.fyi/tools/mc/tapaal/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/tapaal/
+ <p>TAPAAL is a tool for verification of timed-arc petri nets</p>
+
+
+ TLA+
+ https://fmtools.fyi/tools/mod/tlaplus/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mod/tlaplus/
+ <p>TLA+ is a high-level language for modeling programs and systems–especially concurrent and distributed ones.</p>
+
+
+ Uppaal
+ https://fmtools.fyi/tools/mc/uppaal/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/mc/uppaal/
+ <p><div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span>
<span style="display:none">[</span>
<span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span>
<span style="display:none">] </span>
</div>
Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).</p>
+ Vampire
https://fmtools.fyi/tools/sat-smt/vampire/
diff --git a/maintenance/not-maintained/index.html b/maintenance/not-maintained/index.html
index 0779ae5..27da502 100644
--- a/maintenance/not-maintained/index.html
+++ b/maintenance/not-maintained/index.html
@@ -107,6 +107,14 @@
+
+BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool for C language that solves the reachability problem, i.e. whether a given program location can be reached from an entry point (main function) by a valid execution.
+
+
+
+
+
+
+
+CADP (“Construction and Analysis of Distributed Processes”, formerly known as “CAESAR/ALDEBARAN Development Package”) is a toolbox for the design of asynchronous concurrent systems, such as communication protocols, distributed systems, asynchronous circuits, multiprocessor architectures, web services, etc.
+
+
+
+
+
+
+
IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.
+Intrepyd is a python module that provides a simulator and a model checker in form of a rich API, to allow the rapid prototyping of formal methods algorithms for the rigorous analysis of circuits, specifications, models.
+
+
+
+
+
+
+
+LTSA is a verification tool for concurrent systems. It mechanically checks that the specification of a concurrent system satisfies the properties required of its behaviour. In addition, LTSA supports specification animation to facilitate interactive exploration of system behaviour.
+
+
+
+
+
+
+
LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the toolset was extended to a a full (LTL/CTL/μ-calculus) model checker, while maintaining its language-independent characteristics.
mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols.
The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification in continuous and hybrid systems.
+Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).
+
+
+
+
+
+
+
This page lists all of the modeling tools and Languages on this site in alphabetical order.
+Click a tool name in the first column to view tool details.
+Click a colorful item in the second column to view all the tools for which that term applies.
+Item colors mean nothing and are intended to make it easy to skim the page.
+Colors are generated by hashing each term’s name and converting it to RGB color values.
diff --git a/tools/prob/index.xml b/tools/prob/index.xml
index de20a39..e1c6ef7 100644
--- a/tools/prob/index.xml
+++ b/tools/prob/index.xml
@@ -8,6 +8,13 @@
en-usSat, 07 Jun 2025 00:00:00 +0000
+
+ Caesar
+ https://fmtools.fyi/tools/prob/caesar/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ https://fmtools.fyi/tools/prob/caesar/
+ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p>
+ COMICS
https://fmtools.fyi/tools/prob/comics/
diff --git a/tools/sat-smt/index.html b/tools/sat-smt/index.html
index 21b3519..dff5a1e 100644
--- a/tools/sat-smt/index.html
+++ b/tools/sat-smt/index.html
@@ -187,6 +187,10 @@ Click a colorful">
+
+
+
+
@@ -1644,6 +1648,133 @@ Colors are generated by hashing each term’s name and converting it to RGB
+
cvc5 is an automatic theorem prover for SMT problems.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/tools/sat-smt/mathsat/index.html b/tools/sat-smt/mathsat/index.html
index 6f4d9c4..92516db 100644
--- a/tools/sat-smt/mathsat/index.html
+++ b/tools/sat-smt/mathsat/index.html
@@ -19,7 +19,7 @@
Closed-Source Tool
]
-MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get">
+MathSAT is an SMT solver supporting a wide range of theories (including e.g. equality and uninterpreted">
@@ -319,7 +319,7 @@ MiniSat is a minimalistic, open-source SAT solver, developed to help researchers
Closed-Source Tool]
-MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.
+MathSAT is an SMT solver supporting a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, and arrays) and functionalities (including e.g. computation of Craig interpolants, extraction of unsatisfiable cores, generation of models and proofs, and the ability of working incrementally).