Fix #15

.gitea/issue_template/add_tool.md

@@ -7,6 +7,8 @@ assignees: ["mossbiscuits"]
 labels:
 - "new tool"
 - "enhancement"
+projects:
+- "Tool Collection"
 ---
 
 Fill in as little or as much information as you like, but more information increases my ability to add your tool effectively.

_index.md

@@ -2,6 +2,7 @@
 title = 'The Ultimate Formal Methods Toolbox'
 subtitle = 'Discover, Explore, and Contribute to the World’s Largest Collection of Formal Methods Tools'
 # date = 2023-01-01T08:00:00-07:00
+date = 2025-06-07
 # draft = false 
 +++
 

about.md

@@ -1,10 +1,10 @@
 +++
 title = 'About'
 subtitle = 'Learn more about the Formal Methods Tools project'
+date = 2025-06-07
 +++
 
-
-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
 

contribute.md

@@ -1,5 +1,6 @@
 +++
 title = 'Contribute'
+date = 2025-06-07
 +++
 
 Instructions coming soon. Please see https://gitmoss.fyi/fmtools/content/wiki/Contribute for temporary instructions.

license.md

@@ -1,6 +1,7 @@
 +++
 title = 'MIT License'
 subtitle = 'Open-Source and Free to Use'
+date = 2025-06-07
 +++
 
 MIT License

privacy.md

@@ -1,6 +1,7 @@
 +++
 title = 'Privacy'
 subtitle = "tl;dr: I won't know you were here."
+date = 2025-06-07
 +++
 
 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.

tools/mc/blast.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'BLAST'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://forge.ispras.ru/projects/blast", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://forge.ispras.ru/projects/blast/repository", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Uppsala Universitet', 'Aalborg University']
+licenses = ['Apache-2.0']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2012">}}
+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.

tools/mc/cadp.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'CADP'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://cadp.inria.fr/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://forge.ispras.ru/projects/blast/repository", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['INRIA Rocquencourt']
+licenses = ['All Rights Reserved']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+{{<closed-source>}}
+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. 

tools/mc/cgaal.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'CGAAL'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "http://ltsmin.utwente.nl/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/d702e20/CGAAL", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['University of Twente']
+licenses = ['AGPL-v3']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+CGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game structures (CGSs).

tools/mc/concuerror.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Concuerror'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "http://parapluu.github.io/Concuerror", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/parapluu/Concuerror", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Uppsala University']
+licenses = ['BSD']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+Concuerror is a stateless model checking tool for Erlang programs.

tools/mc/cpachecker.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'CPAchecker'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://cpachecker.sosy-lab.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://gitlab.com/sosy-lab/software/cpachecker/", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Ludwig-Maximilians-Universität München']
+licenses = ['Apache-2.0']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+{{<closed-source>}}
+CPAchecker is a tool for configurable software verification.

tools/mc/dscheck.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'DSCheck'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "http://ltsmin.utwente.nl/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/ocaml-multicore/dscheck", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['University of Twente']
+licenses = ['ISC']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+DSCheck is an experimental model checker for testing concurrent OCaml programs.

tools/mc/eldarica.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Eldarica'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/uuverifiers/eldarica", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Uppsala University']
+licenses = ['BSL']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+Eldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs.

tools/mc/esbmc.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'ESBMC'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://ssvlab.github.io/esbmc/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/esbmc/esbmc", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Federal University of Amazonas', 'University of Bristol', 'University of Manchester', 'University of Stellenbosch', 'University of Southampton']
+licenses = ['Apache-2.0', 'BSD 4-clause', 'MIT', 'BSD 3-clause', 'GPLv3', ]
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.

tools/mc/geyser.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Geyser'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/JakubSarnik/geyser", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['Eindhoven University of Technology']
+licenses = ['MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+techniques = ['PDR', 'CAR']
+# publications = ['']
++++
+
+Geyser is a simple symbolic model checker for propositional transition system systems.

tools/mc/imitator.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'IMITATOR'
+subtitle = 'Parameter Synthesis'
+links = [
+    { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/imitator-model-checker/imitator", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Parameter Synthesizer']
+developers = ['Universite Sorbonne Paris Nord']
+licenses = ['GPLv3']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more. 

tools/mc/imspin.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'ImSpin'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/MrDiver/ImSpin", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['Eindhoven University of Technology']
+licenses = ['MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['PDR', 'CAR']
+# publications = ['']
++++
+
+ImSpin is a frontend for the [SPIN](../spin) model checker, providing an environment for users engaged in model checking tasks.

tools/mc/intrepyd.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Intrepyd'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/formalmethods/intrepid", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['']
+licenses = ['BSD']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2021">}}
+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.

tools/mc/ivy.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'IVy'
+subtitle = 'Protocol Verifier'
+links = [
+    { title = "Homepage", url = "https://kenmcmil.github.io/ivy/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/kenmcmil/ivy", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Protocol Verifier']
+developers = ['Microsoft Research']
+licenses = ['MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2023">}}
+IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques.

tools/mc/kind2.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Kind 2'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://kind2-mc.github.io/kind2/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/kind2-mc/kind2", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['University of Iowa']
+licenses = ['Apache-2.0']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems.

tools/mc/ltsa.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'LTSA'
+subtitle = 'Labelled Transition System Analyser'
+links = [
+    { title = "Homepage", url = "https://www.doc.ic.ac.uk/ltsa/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['University of Twente']
+# licenses = ['BSD']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2018">}}
+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. 

tools/mc/ltsmin.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'LTSmin'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "http://ltsmin.utwente.nl/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/utwente-fmt/ltsmin", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['University of Twente']
+licenses = ['BSD']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+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.

tools/mc/mcltlrs.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'mcltl-rs'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://nuxmv.fbk.eu/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/NotBad4U/mcltl-rs", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['Fondazione Bruno Kessler']
+# licenses = ['All Rights Reserved']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2020">}}
+<!-- {{<closed-source>}} -->
+mcltl-rs is an experimental model checker for LTL written in Rust.

tools/mc/mcrl2.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'mCRL2'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/mCRL2org/mCRL2", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Eindhoven University of Technology']
+licenses = ['BSL']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+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.

tools/mc/mercury.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Mercury'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/rtsaad/mercury", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['LAAS-CNRS', 'Vertics']
+licenses = ['MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2020">}}
+Mercury is a Model Checker developed for multicore, multiprocessors machine with shared memory.

tools/mc/munta.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'MUNTA'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/wimmers/munta", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['']
+licenses = ['MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2020">}}
+MUNTA is a model checker for the popular realtime systems modeling formalism of Timed Automata

tools/mc/nusmv.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'NuSMV'
+subtitle = 'Symbolic Model Checker'
+links = [
+    { title = "Homepage", url = "https://nusmv.fbk.eu/index.html", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Fondazione Bruno Kessler']
+licenses = ['LGPL']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2018">}} -->
+NuSMV is a symbolic model checker.

tools/mc/nuxmv.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'NuXMV'
+subtitle = 'Symbolic Model Checker'
+links = [
+    { title = "Homepage", url = "https://nuxmv.fbk.eu/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Fondazione Bruno Kessler']
+licenses = ['All Rights Reserved']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2018">}} -->
+{{<closed-source>}}
+nuXmv is a symbolic model checker for the analysis of synchronous finite-state and infinite-state systems.

tools/mc/pnmc.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Pnmc'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "http://ltsmin.utwente.nl/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['University of Twente']
+licenses = ['BSD']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+Pnmc is a symbolic model checker for Petri nets.

tools/mc/pypl.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'pyPL'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/nclarius/pyPL", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker', 'Model Generator', 'Theorem Prover']
+developers = ['Matthew Fernandez']
+licenses = ['Unilicense']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+pyPL is a naive model generator, model checker and theorem prover.

tools/mc/romeo.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Roméo'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://romeo.ls2n.fr/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['University of Nantes']
+licenses = ['GPL']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2018">}} -->
+<!-- {{<closed-source>}} -->
+Romeo allows the modelling of complex systems using extensions of time Petri nets.

tools/mc/rumur.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Rumur'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/Smattr/rumur", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Matthew Fernandez']
+licenses = ['Unilicense']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+Rumur is a model checker.

tools/mc/sally.md

@@ -2,7 +2,7 @@
 date = 2025-06-07
 draft = false
 title = 'Sally'
-subtitle = 'Probabilistic Model Checker'
+subtitle = 'Model Checker'
 links = [
     { title = "Homepage", url = "http://sri-csl.github.io/sally/", icon = 'fa-solid fa-home' },
     { title = "Source Code", url = "https://github.com/SRI-CSL/sally", icon = 'fa-brands fa-github'  },

tools/mc/smpt.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'SM(P/)T'
+subtitle = 'Satisfiability Modulo Petri Net'
+links = [
+    # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/nicolasAmat/SMPT", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['LAAS-CNRS']
+licenses = ['GPLv3']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).

tools/mc/spaceex.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'SpaceEx'
+subtitle = 'Hybrid Systems'
+links = [
+    { title = "Homepage", url = "http://spaceex.imag.fr/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://forge.ispras.ru/projects/blast/repository", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Hybrid Systems']
+developers = ['Verimag']
+licenses = ['GPLv3']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+<!-- {{<closed-source>}} -->
+The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification in continuous and hybrid systems.

tools/mc/spin.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Spin'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://spinroot.com/spin/whatispin.html", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/nimble-code/Spin", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Bell Labs']
+licenses = ['All Rights Reserved']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['PDR', 'CAR']
+# publications = ['']
++++
+
+Spin is a model checker for multi-threaded software.

tools/mc/stateright.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'stateright'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://docs.rs/stateright/latest/stateright/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/stateright/stateright", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Jonathan Nadal']
+licenses = ['MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+<!-- {{<closed-source>}} -->
+`stateright` is a Rust library for model checking systems, with an emphasis on distributed systems.

tools/mc/tapaal.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'TAPAAL'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://www.tapaal.net/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/TAPAAL/", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Aalborg University']
+licenses = ['Open Source 3.0', 'BSD', 'GPLv2']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+<!-- {{<closed-source>}} -->
+TAPAAL is a tool for verification of timed-arc petri nets

tools/mc/timesolver.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'TimeSolver'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://nuxmv.fbk.eu/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/jkeiren/TimeSolver", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['Fondazione Bruno Kessler']
+# licenses = ['All Rights Reserved']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2019">}}
+TimeSolver is a Model Checker for timed automata that uses pes (predicate equation systems).

tools/mc/uppaal.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Uppaal'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://uppaal.org/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/imitator-model-checker/imitator", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Uppsala Universitet', 'Aalborg University']
+licenses = ['All Rights Reserved']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<closed-source>}}
+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.).

tools/mod/_index.md

@@ -0,0 +1,10 @@
++++
+title = "Modeling (Tools and Languages)"
+layout = "section"
++++
+
+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.

tools/mod/jani.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'JANI'
+subtitle = 'Quantitative Modeling Specification'
+links = [
+    { title = "Homepage", url = "https://momba.dev/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/koehlma/momba", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Modeling Language']
+developers = ['University of Twente', 'RWTH Aachen', 'ISCAS', 'Universidad Nacional de Cordoba']
+licenses = ['Apache-2.0', 'MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+<!-- {{<closed-source>}} -->
+The JANI specification defines the jani-model model interchange format and the jani-interaction tool interaction and automation protocol.

tools/mod/momba.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Momba'
+subtitle = 'Quantitative Modeling Framework'
+links = [
+    { title = "Homepage", url = "https://momba.dev/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/koehlma/momba", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Modeling Framework']
+developers = ['Saarland University']
+licenses = ['Apache-2.0', 'MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+<!-- {{<closed-source>}} -->
+Momba is a Python framework for dealing with quantitative models centered around the [JANI-model](../jani) interchange format.

tools/mod/tlaplus.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'TLA+'
+subtitle = 'Modeling Language'
+links = [
+    { title = "Homepage", url = "https://lamport.azurewebsites.net/tla/tla.html", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/TAPAAL/", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Modeling Language']
+developers = [' Leslie Lamport']
+licenses = ['Open Source 3.0', 'BSD', 'GPLv2']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+<!-- {{<closed-source>}} -->
+TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones.

tools/prob/caesar.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Caesar'
+subtitle = 'Probabilistic Program Prover'
+links = [
+    { title = "Homepage", url = "https://www.caesarverifier.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/moves-rwth/caesar", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Program Prover']
+developers = ['RWTH Aachen']
+licenses = ['MIT']
+inputs = ['HeyVL']
+interfaces = ['CLI', 'VSCode']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Hensel2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+Caesar is a deductive verifier for probabilistic programs.

tools/prob/comics.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'COMICS'
+subtitle = 'DTMC Counterexample Generator'
+links = [
+    { title = "Homepage", url = "https://ths.rwth-aachen.de/research/tools/comics/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/moves-rwth/storm", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Counterexample Generator']
+developers = ['RWTH Aachen']
+# licenses = ['GPLv3']
+# inputs = ['PRISM', 'JANI', 'PNML', 'GreatSPN', 'Galileo', 'MRMC']
+# interfaces = ['CLI', 'C++', 'Python']
+# maintenance = ['Unknown']
+# techniques = ['CDCL']
+# publications = ['Hensel2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for discrete-time Markov Chains (DTMCs).

tools/prob/dftgui.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'DFT Visualization'
+subtitle = 'Visualization for Dynamic Fault Trees'
+links = [
+    { title = "Homepage", url = "https://moves-rwth.github.io/dft-gui/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/moves-rwth/dft-gui", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Visualizer']
+developers = ['RWTH Aachen']
+# licenses = ['MIT']
+# inputs = ['HeyVL']
+interfaces = ['GUI', 'Online']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['Hensel2022']
++++
+
+{{<inactive year="2021">}}
+PRINSYS is a tool for invariant generation for probabilistic programs.

tools/prob/prinsys.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'PRINSYS'
+subtitle = 'PRobabilistic INvariant SYnthesiS'
+links = [
+    { title = "Homepage", url = "https://www-i2.informatik.rwth-aachen.de/prinsys/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/moves-rwth/caesar", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Invariant Synthesizer']
+developers = ['RWTH Aachen']
+# licenses = ['MIT']
+# inputs = ['HeyVL']
+interfaces = ['GUI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['Hensel2022']
++++
+
+{{<inactive year="2012">}}
+PRINSYS is a tool for invariant generation for probabilistic programs.

tools/prob/prophesy.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Prophesy'
+subtitle = 'Parameter Synthesis'
+links = [
+    # { title = "Homepage", url = "https://www-i2.informatik.rwth-aachen.de/prinsys/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/moves-rwth/prophesy", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Parameter Synthesizer']
+developers = ['RWTH Aachen']
+licenses = ['GPLv3']
+# inputs = ['HeyVL']
+# interfaces = ['GUI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['Hensel2022']
++++
+
+{{<inactive year="2019">}}
+Prophesy is a tool set for parameter synthesis of parametric Markov models.

tools/programs/_index.md

@@ -0,0 +1,10 @@
++++
+title = "Program Proof Tools"
+layout = "section"
++++
+
+This page lists all of the program proof tools 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.

tools/programs/aeneas.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Aeneas'
+subtitle = 'Rust Verifier'
+links = [
+    { title = "Homepage", url = "https://aeneasverif.github.io/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/AeneasVerif/aeneas", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Program Prover', 'Rust Verifier']
+developers = ['Microsoft Research', 'Inria']
+licenses = ['Apache-2.0']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+Aeneas (pronunced [Ay-nay-as]) is a verification toolchain for Rust programs.

tools/programs/creusot.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Creusot'
+subtitle = 'Rust Verifier'
+links = [
+    # { title = "Homepage", url = "https://dafny.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/creusot-rs/creusot", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Program Prover', 'Rust Verifier']
+# developers = ['Amazon Web Services']
+licenses = ['LGPLv2.1']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+Creusot is a deductive verifier for Rust code.

tools/programs/dafny.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Dafny'
+subtitle = 'Program Proofs'
+links = [
+    { title = "Homepage", url = "https://dafny.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/dafny-lang/dafny", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Program Prover']
+developers = ['Amazon Web Services']
+licenses = ['MIT']
+inputs = ['Dafny']
+interfaces = ['CLI', 'VSCode']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+Dafny is a verification-aware programming language that has native support for recording specifications and is equipped with a static program verifier.

tools/programs/kani.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Kani'
+subtitle = 'Rust Verifier'
+links = [
+    { title = "Homepage", url = "https://model-checking.github.io/kani/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/model-checking/kani", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker', 'Rust Verifier']
+# developers = ['Microsoft Research', 'Inria']
+licenses = ['Apache-2.0', 'MIT']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+The Kani Rust Verifier is a bit-precise model checker for Rust.

tools/programs/loom.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Loom'
+subtitle = 'Rust Verifier'
+links = [
+    # { title = "Homepage", url = "https://www.pm.inf.ethz.ch/research/prusti.html", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/tokio-rs/loom", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Rust Verifier']
+developers = ['Tokio']
+licenses = ['MIT']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2024">}} -->
+Loom is a testing tool for concurrent Rust code. 

tools/programs/miri.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Miri'
+subtitle = 'Rust Verifier'
+links = [
+    # { title = "Homepage", url = "https://model-checking.github.io/kani/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/rust-lang/miri", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Rust Verifier']
+# developers = ['Microsoft Research', 'Inria']
+licenses = ['Apache-2.0', 'MIT']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+Miri is an Undefined Behavior detection tool for Rust.

tools/programs/prusti.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Prusti'
+subtitle = 'Rust Verifier'
+links = [
+    { title = "Homepage", url = "https://www.pm.inf.ethz.ch/research/prusti.html", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/viperproject/prusti-dev", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Rust Verifier']
+# developers = ['Microsoft Research', 'Inria']
+licenses = ['Mozilla-2.0']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+{{<inactive year="2024">}}
+Prusti is a prototype verifier for Rust that makes it possible to formally prove absence of bugs and correctness of code contracts.

tools/programs/shuttle.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Loom'
+subtitle = 'Rust Verifier'
+links = [
+    # { title = "Homepage", url = "https://www.pm.inf.ethz.ch/research/prusti.html", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/awslabs/shuttle", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Rust Verifier']
+developers = ['Amazon Web Services']
+licenses = ['MIT']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2024">}} -->
+Shuttle is a library for testing concurrent Rust code.

tools/programs/verus.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Verus'
+subtitle = 'Rust Verifier'
+links = [
+    # { title = "Homepage", url = "https://www.pm.inf.ethz.ch/research/prusti.html", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/verus-lang/verus", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Rust Verifier']
+# developers = ['Microsoft Research', 'Inria']
+licenses = ['MIT']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2024">}} -->
+Verus is a tool for verifying the correctness of code written in Rust.

tools/sat-smt/cadical.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'CaDiCaL'
+subtitle = 'SAT Solver'
+links = [
+    # { title = "Homepage", url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/arminbiere/cadical", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SAT Solver']
+developers = ['University of Freiburg']
+licenses = ['MIT']
+# inputs = ['']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+CaDiCaL is a simplified satisfiability solver.

tools/sat-smt/e.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'E'
+subtitle = 'Theorem Prover'
+links = [
+    { title = "Homepage", url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/eprover/eprover", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Theorem Prover']
+developers = ['DHBW Stuttgart']
+licenses = ['GPLv2']
+# inputs = ['']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with equality.

tools/sat-smt/lean.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'LEAN'
+subtitle = 'Programming Language & Theorem Prover'
+links = [
+    { title = "Homepage", url = "https://lean-lang.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/leanprover/lean4", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Theorem Prover', 'Modeling Language']
+developers = ['Lean FRO']
+licenses = ['Apache-2.0']
+# inputs = ['SMTLIB2']
+# interfaces = ['CLI', 'Online']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+cvc5 is an automatic theorem prover for SMT problems.

tools/sat-smt/mathsat.md

@@ -19,4 +19,4 @@ maintenance = ['Actively Maintained']
 +++
 
 {{<closed-source>}}
-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).

tools/sat-smt/vampire.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Vampire'
+subtitle = 'Theorem Prover'
+links = [
+    { title = "Homepage", url = "https://vprover.github.io/index.html", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/vprover/vampire", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Theorem Prover']
+developers = ['TU Wien']
+licenses = ['BSD']
+# inputs = ['']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+Vampire is a theorem prover.

tools/sat-smt/zipperposition.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Zipperposition'
+subtitle = 'Theorem Prover'
+links = [
+    { title = "Homepage", url = "https://sneeuwballen.github.io/zipperposition/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/sneeuwballen/zipperposition", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Theorem Prover']
+developers = ['TU Wien']
+licenses = ['BSD']
+# inputs = ['']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+Zipperposition is an automated theorem prover for first-order logic with equality and theories.