fmtools/content
1
0
Fork 0
Code Issues 31 Pull Requests Actions Packages Releases Wiki Activity

Compare commits

base: fmtools:0cb4f7ed821f9f342dd2f63198bf4923a1e0161f
Branches Tags
fmtools:main
...
compare: fmtools:main
Branches Tags
fmtools:main

12 Commits
0cb4f7ed82 ... main

Author SHA1 Message Date
Landon Taylor
0d0f7a7cda Fix #29 2025-08-22 13:50:11 -06:00
Landon Taylor
15ac900894 Close #28 2025-08-22 13:44:11 -06:00
Landon Taylor
3a9f16c0cc Close #26 2025-08-22 13:42:01 -06:00
Landon Taylor
867b966f74 Close #24 2025-08-22 13:39:37 -06:00
Landon Taylor
d63b97d62b Close #23 2025-08-22 13:24:48 -06:00
Landon Taylor
65e02d39e1 Close #22 2025-08-22 13:09:52 -06:00
Landon Taylor
52735b97c6 Close #20 2025-08-22 13:00:04 -06:00
Landon Taylor
8e760b44e3 Close #19 2025-08-22 12:42:35 -06:00
Landon Taylor
2c1587a006 Close #18 2025-08-21 18:02:34 -06:00
Landon Taylor
1b28b1b8b4 fix new tool generator and add rcoq for #18 2025-08-21 17:38:12 -06:00
Landon Taylor
1b3dfad81e Fix listeners 2025-08-21 17:34:44 -06:00
Landon Taylor
3e9b8f84b3 Add new tool generator 2025-08-21 17:24:52 -06:00
88 changed files with 1710 additions and 33 deletions
Expand all files Collapse all files

1
_index.md
View File

@@ -21,4 +21,3 @@ Taxonomy Data
{{<button href="/contribute">}}
Contribute
{{</button>}}

434
new-tool.md
View File

@@ -1,12 +1,436 @@
+++
title = 'Contribute'
date = 2025-06-07
title = 'New Tool Page Generator'
subtitle = "Creates nicely formatted markdown for a new tool, so you don't have to"
date = 2025-08-21
+++
This page is useful to generate copy-and-paste source code in Markdown for a new tool.
**Publications:** Coming soon.
## Quick Links
Reset the form with **Double Click** on reset button for safety.
- Request addding a tool: [Submit Git Issue](https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2fadd_tool.md)
- Request fixing a tool: [Submit Git Issue](https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md)
{{<rawhtml>}}
<script>
function arr(str) {
return str.split(',').map(s => s.trim()).filter(Boolean);
}
function bool(val) {
return val ? 'false' : 'true';
}
function generateMarkdown() {
const title = document.getElementById('title').value;
const subtitle = document.getElementById('subtitle').value;
const date = new Date().toISOString().slice(0, 10);
const homepage = arr(document.getElementById('homepage').value);
const sourcecode = arr(document.getElementById('sourcecode').value);
const playground = arr(document.getElementById('playground').value);
const applications = arr(document.getElementById('applications').value);
const developers = arr(document.getElementById('developers').value);
const licenses = arr(document.getElementById('licenses').value);
const inputs = arr(document.getElementById('inputs').value);
const interfaces = arr(document.getElementById('interfaces').value);
const updatedYear = parseInt(document.getElementById('updated-year').value, 10);
const currentYear = new Date().getFullYear();
let maintenance = "Actively Maintained";
let maintenance_year = "";
let description = document.getElementById('description').value;
if (updatedYear && currentYear - updatedYear > 5) {
maintenance = "Not Maintained";
maintenance_year = `updated_year = ${updatedYear}\n`;
description = `\{\{<inactive year="${updatedYear}">\}\}\n\n` + description
}
let md = `+++
title = '${title}'
subtitle = '${subtitle}'
links = [${homepage.length ? `\n\t{ title = "Homepage", url = "${homepage}", icon = 'fa-solid fa-home' },\n` : ''}${sourcecode.length ? `\t{ title = "Source Code", url = "${sourcecode}", icon = 'fa-solid fa-code' },\n` : ''}${playground.length ? `\t{ title = "Playground", url = "${playground}", icon = 'fa-solid fa-gamepad' }\n` : ''}]
applications = ${JSON.stringify(applications)}
developers = ${JSON.stringify(developers)}
licenses = ${JSON.stringify(licenses)}
inputs = ${JSON.stringify(inputs)}
interfaces = ${JSON.stringify(interfaces)}
maintenance = [${JSON.stringify(maintenance)}]
${maintenance_year}draft = false
date = ${date}
+++\n\n`;
md += description;
document.getElementById('output').textContent = md;
}
</script>
<table style="width: 100%">
<style>
input[type="text"],
input[type="url"],
input[type="date"],
textarea {
width: 100%;
box-sizing: border-box;
}
input,textarea {
margin: 0.2rem 0.2rem;
font-weight: 500;
}
table {
border-collapse: collapse;
width: 100%;
background: #eee;
color: #000;
border-radius: 0.5rem;
}
th, td {
padding: 8px;
text-align: left;
}
tr:nth-child(even) {
background: #ccc;
}
label {
color: #000;
font-weight: 600;
margin-right: 0.5rem;
}
input, textarea, select {
background: #fff;
color: #000;
border: 2px solid #888;
padding: 4px;
padding: 0.2rem 1rem;
font-size: 0.9rem;
}
button {
background: #000;
color: #ccc;
border: 2px solid white;
padding: 8px 38px;
font-size: 1rem;
font-weight: bold;
cursor: pointer;
}
button:hover {
background: #444;
}
</style>
<tr>
<td><label for="title">Title:</label></td>
<td><input type="text" id="title" required></td>
</tr>
<tr>
<td><label for="subtitle">Subtitle:</label></td>
<td><input type="text" id="subtitle"></td>
</tr>
<tr>
<td><label for="description">Description:</label></td>
<td><textarea id="description" rows="3" cols="50"></textarea></td>
</tr>
<tr>
<td><label for="homepage">Homepage URL:</label></td>
<td><input type="url" id="homepage" placeholder="https://example.com"></td>
</tr>
<tr>
<td><label for="sourcecode">Source Code URL:</label></td>
<td><input type="url" id="sourcecode" placeholder="https://github.com/example"></td>
</tr>
<tr>
<td><label for="playground">Playground URL:</label></td>
<td><input type="url" id="playground" placeholder="https://play.example.com"></td>
</tr>
<tr>
<td><label for="applications">Applications:</label></td>
<td>
<div id="applications-checkboxes">
<label><input type="checkbox" value="Theorem Prover">Theorem Prover</label> &nbsp;
<label><input type="checkbox" value="SMT Solver">SMT Solver</label> &nbsp;
<label><input type="checkbox" value="SAT Solver">SAT Solver</label>
<label><input type="checkbox" value="SAT Solver">Constraint Solver</label>
<br>
<label><input type="checkbox" value="Model Checker">Model Checker</label> &nbsp;
<label><input type="checkbox" value="Runtime Verifier">Runtime Verifier</label> &nbsp;
<label><input type="checkbox" value="Proof Assistant">Proof Assistant</label> &nbsp;
<label><input type="checkbox" value="Program Prover">Program Prover</label> &nbsp;
<label><input type="checkbox" value="Protocol Verifier">Protocol Verifier</label> &nbsp;
<br>
<label><input type="checkbox" value="Static Analyzer">Static Analyzer</label> &nbsp;
<label><input type="checkbox" value="Type Checker">Type Checker</label> &nbsp;
<label><input type="checkbox" value="Code Synthesizer">Code Synthesizer</label>
<label><input type="checkbox" value="Parameter Synthesizer">Parameter Synthesizer</label> &nbsp;
<br>
<label><input type="checkbox" value="Test Generator">Test Generator</label> &nbsp;
<label><input type="checkbox" value="Model Simulator">Model Simulator</label> &nbsp;
<label><input type="checkbox" value="Counterexample Generator">Counterexample Generator</label> &nbsp;
<br>
<label><input type="checkbox" value="Specification Language">Specification Language</label> &nbsp;
<label><input type="checkbox" value="Refinement Tool">Refinement Tool</label> &nbsp;
<label><input type="checkbox" value="Visualizer">Visualizer</label> &nbsp;
<br>
<label><input type="checkbox" value="Probabilistic Program Prover">Probabilistic Program Prover</label> &nbsp;
<label><input type="checkbox" value="Probabilistic Model Checker">Probabilistic Model Checker</label> &nbsp;
<label><input type="checkbox" value="Stochastic Simulator">Stochastic Simulator</label>
<br>
<!-- <label for="other-applications">Other:</label> -->
<input type="text" id="other-applications" placeholder="Other application">
<script>
document.getElementById('other-applications').addEventListener('input', updateApplications);
Array.from(document.querySelectorAll('#applications-checkboxes input[type="checkbox"]')).forEach(cb => {
cb.addEventListener('change', updateApplications);
});
function updateApplications() {
const otherValue = document.getElementById('other-applications').value.trim();
const checkboxes = Array.from(document.querySelectorAll('#applications-checkboxes input[type="checkbox"]:checked')).map(cb => cb.value);
const applications = otherValue ? [...checkboxes, otherValue] : checkboxes;
document.getElementById('applications').value = applications.join(', ');
}
</script> </script>
<input type="hidden" id="applications">
</div>
</td>
<script>
function getCheckedApplications() {
return Array.from(document.querySelectorAll('#applications-checkboxes input[type="checkbox"]:checked'))
.map(cb => cb.value);
}
</script>
</tr>
<tr>
<td><label for="developers">Developers:</label></td>
<td>
<input type="text" id="developers" placeholder="Devs separated by commas, e.g. Alice, Bob, Carol">
</td>
</tr>
</tr>
<tr>
<td><label for="licenses">License:</label></td>
<td>
<select id="licenses">
<optgroup label="Copyleft (GPL)">
<option value="GPL-1.0">GPL-1.0</option>
<option value="GPL-2.0">GPL-2.0</option>
<option value="GPL-3.0">GPL-3.0</option>
<option value="AGPL-3.0">AGPL-3.0</option>
</optgroup>
<optgroup label="Copyleft (LGPL)">
<option value="LGPL-2.1">LGPL-2.1</option>
<option value="LGPL-3.0">LGPL-3.0</option>
</optgroup>
<optgroup label="Copyleft (Other)">
<option value="EPL-2.0">EPL-2.0</option>
<option value="CDDL-1.0">CDDL-1.0</option>
<option value="OSL-3.0">OSL-3.0</option>
<option value="CECILL-2.1">CECILL-2.1</option>
<option value="Artistic-2.0">Artistic-2.0</option>
<option value="IPL-1.0">IPL-1.0</option>
<option value="OCamlPro Non-Commercial">OCamlPro Non-Commercial</option>
</optgroup>
<optgroup label="Permissive">
<option value="MIT">MIT</option>
<option value="Apache-1.1">Apache-1.1</option>
<option value="Apache-2.0">Apache-2.0</option>
<option value="BSD-2-Clause">BSD-2-Clause</option>
<option value="BSD-3-Clause">BSD-3-Clause</option>
<option value="ISC">ISC</option>
<option value="MPL-2.0">MPL-2.0</option>
<option value="Zlib">Zlib</option>
<option value="Unlicense">Unlicense</option>
<option value="CC0-1.0">CC0-1.0</option>
</optgroup>
<optgroup label="Proprietary / Other">
<option value="All Rights Reserved">All Rights Reserved</option>
<option value="NASA Open-Source">NASA Open-Source</option>
</optgroup>
<option value="">Select a license</option> document.getElementById('licenses').addEventListener('change', function() {
document.getElementById('licenses-hidden').value = this.value;
});
</script>
<input type="hidden" id="licenses-hidden">
</td>
</tr>
<tr>
<td><label for="inputs">Inputs:</label></td>
<td>
<div id="inputs-checkboxes">
<!-- SAT/SMT/Model Checking formats -->
<label><input type="checkbox" value="SMT-LIB">SMT-LIB</label> &nbsp;
<label><input type="checkbox" value="DIMACS CNF">DIMACS CNF</label> &nbsp;
<label><input type="checkbox" value="AIGER">AIGER</label> &nbsp;
<label><input type="checkbox" value="TPTP">TPTP</label> &nbsp;
<label><input type="checkbox" value="SyGuS">SyGuS</label> &nbsp;
<label><input type="checkbox" value="WhyML">WhyML</label> &nbsp;
<br>
<!-- Model Checking languages -->
<label><input type="checkbox" value="Promela">Promela</label> &nbsp;
<label><input type="checkbox" value="NuSMV">NuSMV</label> &nbsp;
<label><input type="checkbox" value="LTL">LTL</label> &nbsp;
<label><input type="checkbox" value="CTL">CTL</label> &nbsp;
<br>
<!-- Hardware description languages -->
<label><input type="checkbox" value="Verilog">Verilog</label> &nbsp;
<label><input type="checkbox" value="VHDL">VHDL</label> &nbsp;
<br>
<!-- Formal specification languages -->
<label><input type="checkbox" value="B">B</label> &nbsp;
<label><input type="checkbox" value="Z">Z</label> &nbsp;
<label><input type="checkbox" value="Alloy">Alloy</label> &nbsp;
<label><input type="checkbox" value="TLA+">TLA+</label> &nbsp;
<br>
<!-- Proof assistant formats -->
<label><input type="checkbox" value="Coq">Coq</label> &nbsp;
<label><input type="checkbox" value="Isabelle/HOL">Isabelle/HOL</label> &nbsp;
<label><input type="checkbox" value="HOL Light">HOL Light</label> &nbsp;
<label><input type="checkbox" value="ACL2">ACL2</label> &nbsp;
<label><input type="checkbox" value="PVS">PVS</label> &nbsp;
<br>
<!-- Rewriting and algebraic specification -->
<label><input type="checkbox" value="Maude">Maude</label> &nbsp;
<label><input type="checkbox" value="CASL">CASL</label> &nbsp;
<br>
<!-- Simulation/visualization formats -->
<label><input type="checkbox" value="SPIN">SPIN</label> &nbsp;
<label><input type="checkbox" value="DOT">DOT (Graphviz)</label> &nbsp;
<br>
<!-- Data formats -->
<label><input type="checkbox" value="JSON">JSON</label> &nbsp;
<label><input type="checkbox" value="XML">XML</label> &nbsp;
<label><input type="checkbox" value="CSV">CSV</label> &nbsp;
<br>
<input type="text" id="other-inputs" placeholder="Other input format(s), separated by commas">
<script>
document.getElementById('other-inputs').addEventListener('input', function() {
const otherValues = this.value.split(',').map(s => s.trim()).filter(Boolean);
const checkboxes = Array.from(document.querySelectorAll('#inputs-checkboxes input[type="checkbox"]:checked'))
.map(cb => cb.value);
const inputs = otherValues.length ? [...checkboxes, ...otherValues] : checkboxes;
document.getElementById('inputs').value = inputs.join(', ');
});
</script> <script>
document.getElementById('other-inputs').addEventListener('input', function() {
const otherValue = this.value.trim();
const checkboxes = Array.from(document.querySelectorAll('#inputs-checkboxes input[type="checkbox"]:checked'))
.map(cb => cb.value);
const inputs = otherValue ? [...checkboxes, otherValue] : checkboxes;
document.getElementById('inputs').value = inputs.join(', ');
});
</script>
<input type="hidden" id="inputs">
</div>
</td>
<script>
function getCheckedInputs() {
return Array.from(document.querySelectorAll('#inputs-checkboxes input[type="checkbox"]:checked'))
.map(cb => cb.value);
}
</script>
</tr>
<tr>
<td><label for="interfaces">Interfaces:</label></td>
<td>
<div id="interfaces-checkboxes">
<!-- Web interfaces -->
<label><input type="checkbox" value="Web">Web</label> &nbsp;
<label><input type="checkbox" value="REST">REST</label> &nbsp;
<label><input type="checkbox" value="gRPC">gRPC</label> &nbsp;
<label><input type="checkbox" value="API">API</label> &nbsp;
<br>
<!-- Desktop interfaces -->
<label><input type="checkbox" value="CLI">CLI (Command Line)</label> &nbsp;
<label><input type="checkbox" value="GUI">GUI (Graphical)</label> &nbsp;
<label><input type="checkbox" value="REPL">REPL</label> &nbsp;
<br>
<!-- Integration interfaces -->
<label><input type="checkbox" value="Toolset Integration">Toolset Integration</label> &nbsp;
<label><input type="checkbox" value="Library">Library</label> &nbsp;
<label><input type="checkbox" value="Plugin">Plugin</label> &nbsp;
<label><input type="checkbox" value="IDE Integration">IDE Integration</label> &nbsp;
<br>
<!-- Other interfaces -->
<!-- <label for="other-interfaces">Other:</label> -->
<input type="text" id="other-interfaces" placeholder="Other interface(s), separated by commas">
<script>
document.getElementById('other-interfaces').addEventListener('input', updateInterfaces);
Array.from(document.querySelectorAll('#interfaces-checkboxes input[type="checkbox"]')).forEach(cb => {
cb.addEventListener('change', updateInterfaces);
});
function updateInterfaces() {
const otherValues = document.getElementById('other-interfaces').value.split(',').map(s => s.trim()).filter(Boolean);
const checkboxes = Array.from(document.querySelectorAll('#interfaces-checkboxes input[type="checkbox"]:checked')).map(cb => cb.value);
const interfaces = otherValues.length ? [...checkboxes, ...otherValues] : checkboxes;
document.getElementById('interfaces').value = interfaces.join(', ');
} </script>
<input type="hidden" id="interfaces"> </div>
</td>
<script>
function getCheckedInterfaces() {
return Array.from(document.querySelectorAll('#interfaces-checkboxes input[type="checkbox"]:checked'))
.map(cb => cb.value);
}
</script>
</tr>
<tr>
<td><label for="updated-year">Last Updated:</label></td>
<td>
<input type="number" id="updated-year" min="1900" max="2099" style="width:6em;">
<script>
document.getElementById('updated-year').addEventListener('input', function() {
const year = parseInt(this.value, 10);
const currentYear = new Date().getFullYear();
let status = "Actively Maintained";
if (currentYear - year > 5) {
status = "Not Maintained";
}
});
// Update hidden input when radio changes
Array.from(document.getElementsByName('maintenance')).forEach(radio => {
radio.addEventListener('change', function() {
document.getElementById('maintenance').value = this.value;
});
});
</script>
</td>
</tr>
<tr>
<td colspan="2" style="text-align:center;">
<button type="button" onclick="generateMarkdown()">Generate Markdown</button>
<button type="button" ondblclick="resetForm()" onclick="this.style.background='rgba(255, 0, 0, 0.85)';" style="background: rgba(85, 6, 6, 1)">Reset Form</button>
<script>
function resetForm() {
document.getElementById('title').value = '';
document.getElementById('subtitle').value = '';
document.getElementById('homepage').value = '';
document.getElementById('sourcecode').value = '';
document.getElementById('playground').value = '';
document.getElementById('developers').value = '';
document.getElementById('licenses').value = '';
document.getElementById('licenses-hidden').value = '';
document.getElementById('inputs').value = '';
document.getElementById('interfaces').value = '';
document.getElementById('updated-year').value = '';
document.getElementById('description').value = '';
document.getElementById('other-applications').value = '';
document.getElementById('other-inputs').value = '';
// Uncheck all checkboxes
Array.from(document.querySelectorAll('input[type="checkbox"]')).forEach(cb => cb.checked = false);
// Clear output
document.getElementById('output').textContent = '';
}
// Accept "Enter" to trigger Generate Markdown in any field
Array.from(document.querySelectorAll('input,select,number')).forEach(el => {
el.addEventListener('keydown', function(e) {
if (e.key === 'Enter') {
e.preventDefault();
generateMarkdown();
}
});
});
</script>
</td>
</tr>
</table>
<h3>Output Markdown:</h3>
<button type="button" onclick="navigator.clipboard.writeText(document.getElementById('output').textContent)">Copy to Clipboard</button>
<pre id="output" style="background:#000; padding:1em; border:1px solid #ccc;"></pre>
{{</rawhtml>}}

18
tools/mc/abc.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'ABC'
subtitle = 'Sequential Logic Verifier'
links = [
{ title = "Homepage", url = "http://www.eecs.berkeley.edu/~alanmi/abc/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/berkeley-abc/abc", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover","Model Checker"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
System for Sequential Logic Synthesis and Formal Verification

16
tools/mc/avr.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'AVR'
subtitle = 'Reachability Analysis'
links = [ { title = "Source Code", url = "https://github.com/aman-goel/avr", icon = 'fa-solid fa-code' },
]
applications = ["Model Checker"]
developers = []
licenses = ["GPL-3.0"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Reads a state transition system and performs property checking

2
tools/mc/concuerror.md
View File

@@ -10,7 +10,7 @@ links = [
]
applications = ['Model Checker']
developers = ['Uppsala University']
licenses = ['BSD']
licenses = ['BSD-2-Clause']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']

16
tools/mc/fast-downward-pdr.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'Fast Downward PDR'
subtitle = 'Reachability Analyzer'
links = [ { title = "Source Code", url = "https://github.com/Tiim/fast-downward-pdr", icon = 'fa-solid fa-code' },
]
applications = ["Model Checker"]
developers = []
licenses = ["GPL-3.0"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Implementation of the Property-Directed Reachability algorithm in the Fast Downward planning system.

16
tools/mc/fbpdr.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'fbPDR'
subtitle = 'Reachability Analyzer'
links = [ { title = "Source Code", url = "https://github.com/tobiasseufert/fbPDR", icon = 'fa-solid fa-code' },
]
applications = ["Model Checker"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Forward / backward PDR/IC3 implementation.

19
tools/mc/fuseic3.md Normal file
View File

@@ -0,0 +1,19 @@
+++
title = 'FuseIC3'
subtitle = 'Reachability Analyzer'
links = [ { title = "Source Code", url = "https://github.com/rohitdureja/FuseIC3", icon = 'fa-solid fa-code' },
]
applications = ["Model Checker"]
developers = []
licenses = ["GPL-3.0"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2017
draft = false
date = 2025-08-22
+++
{{<inactive year="2017">}}
FuseIC3 is a SAT-based algorithm for checking a set of models. It extends IC3 to minimize time spent in exploring the common state space between related models.

27
tools/mc/geyser.md
View File

@@ -1,21 +1,16 @@
+++
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-solid fa-code' },
# { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
subtitle = 'Reachability Analysis'
links = [ { title = "Source Code", url = "https://github.com/JakubSarnik/geyser", icon = 'fa-solid fa-code' },
]
applications = ['Model Checker']
# developers = ['Eindhoven University of Technology']
licenses = ['MIT']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']
techniques = ['PDR', 'CAR']
# publications = ['']
applications = ["Model Checker"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Geyser is a simple symbolic model checker for propositional transition system systems.
Simple implementation of PDR and CAR model checking algorithms

2
tools/mc/intrepyd.md
View File

@@ -10,7 +10,7 @@ links = [
]
applications = ['Model Checker']
# developers = ['']
licenses = ['BSD']
licenses = ['BSD-3-Clause']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Not Maintained']

2
tools/mc/ltsmin.md
View File

@@ -10,7 +10,7 @@ links = [
]
applications = ['Model Checker']
developers = ['University of Twente']
licenses = ['BSD']
licenses = ['BSD-3-Clause']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']

16
tools/mc/pdrc.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'PDRC'
subtitle = 'Reachability Analyzer'
links = [ { title = "Source Code", url = "https://github.com/Gy-Hu/PDRC", icon = 'fa-solid fa-code' },
]
applications = ["Model Checker"]
developers = []
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Reproduce of "HVC2017: A Supervisory Control Algorithm Based on Property-Directed Reachability"

19
tools/mc/pdrlia.md Normal file
View File

@@ -0,0 +1,19 @@
+++
title = ' PDR-LIA'
subtitle = 'Reachability Analyzer'
links = [ { title = "Source Code", url = "https://github.com/akaydesai/PDR-LIA", icon = 'fa-solid fa-code' },
]
applications = ["Model Checker"]
developers = []
licenses = ["CRAPL"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2018
draft = false
date = 2025-08-22
+++
{{<inactive year="2018">}}
Implementation of Property Directed Reachability for linear integer arithmetic

2
tools/mc/pnmc.md
View File

@@ -10,7 +10,7 @@ links = [
]
applications = ['Model Checker']
# developers = ['University of Twente']
licenses = ['BSD']
licenses = ['BSD-2-Clause']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']

16
tools/mc/reach.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'Reach'
subtitle = 'Reachability Analyzer'
links = [ { title = "Source Code", url = "https://github.com/go-air/reach", icon = 'fa-solid fa-code' },
]
applications = ["Model Checker"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Reach is a symbolic finite state reachability checker. One could also say that Reach is a safety model checker.

16
tools/mc/ric3.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'rIC3'
subtitle = 'Hardware Model Checker'
links = [ { title = "Source Code", url = "https://github.com/gipsyh/rIC3", icon = 'fa-solid fa-code' },
]
applications = ["Model Checker"]
developers = []
licenses = ["GPL-3.0"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Hardware Formal Verification Tool

19
tools/mc/simplepdr.md Normal file
View File

@@ -0,0 +1,19 @@
+++
title = 'SimplePDR'
subtitle = 'Reachability Analyzer'
links = [ { title = "Source Code", url = "https://github.com/rohitdureja/SimplePDR", icon = 'fa-solid fa-code' },
]
applications = ["Model Checker"]
developers = []
licenses = ["GPL-3.0"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2016
draft = false
date = 2025-08-22
+++
{{<inactive year="2016">}}
A reference implementation of property directed reachability for boolean transition systems.

2
tools/mc/tapaal.md
View File

@@ -10,7 +10,7 @@ links = [
]
applications = ['Model Checker']
developers = ['Aalborg University']
licenses = ['Open Source 3.0', 'BSD', 'GPLv2']
licenses = ['GPL-2.0']
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']

19
tools/mc/z3ic3pdr.md Normal file
View File

@@ -0,0 +1,19 @@
+++
title = 'Z3-IC3-PDR'
subtitle = 'Reachability Analyzer'
links = [ { title = "Source Code", url = "https://github.com/pddenhar/Z3-IC3-PDR", icon = 'fa-solid fa-code' },
]
applications = ["Model Checker"]
developers = []
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2016
draft = false
date = 2025-08-22
+++
{{<inactive year="2016">}}
Implementation of the IC3 / Property Directed Reachability algorithm using the the Z3 SMT solver.

2
tools/mod/tlaplus.md
View File

@@ -10,7 +10,7 @@ links = [
]
applications = ['Modeling Language']
developers = [' Leslie Lamport']
licenses = ['Open Source 3.0', 'BSD', 'GPLv2']
licenses = []
# inputs = ['Sally']
# interfaces = ['CLI']
maintenance = ['Actively Maintained']

10
tools/nn/_index.md Normal file
View File

@@ -0,0 +1,10 @@
+++
title = "Neural Net Verification Tools"
layout = "section"
+++
This page lists all of the Neural Net Verification 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.

18
tools/nn/dnnf.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'DNNF'
subtitle = 'Deep Neural Network Falsification'
links = [
{ title = "Homepage", url = "https://dnnf.readthedocs.io/en/latest/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/dlshriver/dnnf", icon = 'fa-solid fa-code' },
]
applications = ["Neural Net Verifier"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
DNNF is a tool for applying falsification methods such as adversarial attacks to the checking of DNN correctness problems.

18
tools/nn/dnnv.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'DNNV'
subtitle = 'Deep Neural Network Verifier'
links = [
{ title = "Homepage", url = "https://docs.dnnv.org/en/stable/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/dlshriver/dnnv", icon = 'fa-solid fa-code' },
]
applications = ["Neural Net Verifier"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
A framework for verification and analysis of deep neural networks.

16
tools/nn/fmdnn.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'FMDNN'
subtitle = 'Deep Neural Network Verifier'
links = [ { title = "Source Code", url = "https://github.com/abj-paul/FMDNN", icon = 'fa-solid fa-code' },
]
applications = ["Neural Net Verifier"]
developers = []
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Formal Method based DNN verification

16
tools/nn/incremental-dnn-verification.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'Incremental Neural Network Verifiers'
subtitle = 'Deep Neural Network Verifier'
links = [ { title = "Source Code", url = "https://github.com/uiuc-arc/Incremental-DNN-Verification", icon = 'fa-solid fa-code' },
]
applications = ["Neural Net Verifier"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Incremental Verifiers for Neural Networks

16
tools/nn/ivan.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'IVAN'
subtitle = 'Deep Neural Network Verifier'
links = [ { title = "Source Code", url = "https://github.com/uiuc-focal-lab/IVAN", icon = 'fa-solid fa-code' },
]
applications = ["Neural Net Verifier"]
developers = []
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Incremental Verification of DNNs

16
tools/nn/verapak.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'VeRAPAk'
subtitle = 'Deep Neural Network Verifier'
links = [ { title = "Source Code", url = "https://github.com/formal-verification-research/VERAPAK", icon = 'fa-solid fa-code' },
]
applications = ["Neural Net Verifier"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
VeRAPAk is an algorithmic framework for optimizing formal verification techniques for deep neural networks when it is used for verifying the local adversarial robustness property of classification problems.

16
tools/nn/verifydnn.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'verifyDNN'
subtitle = 'Deep Neural Network Verifier'
links = [ { title = "Source Code", url = "https://github.com/hunglequoc2001/verifyDNN", icon = 'fa-solid fa-code' },
]
applications = ["Neural Net Verifier"]
developers = []
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Early Implementation of DNN verification algorithms

16
tools/nn/verifying-dnn.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'Verifying-DNN'
subtitle = 'Deep Neural Network Verifier'
links = [ { title = "Source Code", url = "https://github.com/ShivamThukral/Verifying-DNN", icon = 'fa-solid fa-code' },
]
applications = ["Neural Net Verifier"]
developers = []
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
SMT Solvers to verify DNN

16
tools/nn/verigauge.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'VeriGauge'
subtitle = 'Deep Neural Network Verifier'
links = [ { title = "Source Code", url = "https://github.com/AI-secure/VeriGauge", icon = 'fa-solid fa-code' },
]
applications = ["Neural Net Verifier"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
A united toolbox for running major robustness verification approaches for DNNs.

16
tools/nn/veristable.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'VeriStable'
subtitle = 'Deep Neural Network Verifier'
links = [ { title = "Source Code", url = "https://github.com/veristable/veristable", icon = 'fa-solid fa-code' },
]
applications = ["Neural Net Verifier"]
developers = []
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Harnessing Neuron Stability to Improve DNN Verification

10
tools/program-synth/_index.md Normal file
View File

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

16
tools/program-synth/codegen2.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'CodeGen2'
subtitle = 'Program Synthesis'
links = [ { title = "Source Code", url = "https://github.com/salesforce/CodeGen2", icon = 'fa-solid fa-code' },
]
applications = ["Program Synthesizer"]
developers = []
licenses = ["Apache-2.0"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
CodeGen2 models for program synthesis

18
tools/program-synth/fiat.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'Fiat'
subtitle = 'Program Synthesis'
links = [
{ title = "Homepage", url = "http://plv.csail.mit.edu/fiat/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/mit-plv/fiat", icon = 'fa-solid fa-code' },
]
applications = ["Program Synthesizer"]
developers = ["MIT"]
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Mostly Automated Synthesis of Correct-by-Construction Programs

16
tools/program-synth/lakeroad.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'Lakeroad'
subtitle = 'Program Synthesis'
links = [ { title = "Source Code", url = "https://github.com/gussmith23/lakeroad", icon = 'fa-solid fa-code' },
]
applications = ["Program Synthesizer"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
FPGA synthesis tool powered by program synthesis

21
tools/program-synth/minisynth.md Normal file
View File

@@ -0,0 +1,21 @@
+++
title = 'minsynth'
subtitle = 'Program Synthesis'
links = [
{ title = "Homepage", url = "https://www.cs.cornell.edu/~asampson/blog/minisynth.html", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/sampsyo/minisynth", icon = 'fa-solid fa-code' },
]
applications = ["Program Synthesizer"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2019
draft = false
date = 2025-08-22
+++
{{<inactive year="2019">}}
program synthesis is possible

19
tools/program-synth/neuralkanren.md Normal file
View File

@@ -0,0 +1,19 @@
+++
title = 'neuralkanren'
subtitle = 'Program Synthesis'
links = [ { title = "Source Code", url = "https://github.com/xuexue/neuralkanren", icon = 'fa-solid fa-code' },
]
applications = ["Program Synthesizer"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2018
draft = false
date = 2025-08-22
+++
{{<inactive year="2018">}}
Neural Guided Constraint Logic Programming for Program Synthesis

18
tools/program-synth/prose.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'PROSE'
subtitle = 'Program Synthesis'
links = [
{ title = "Homepage", url = "https://www.microsoft.com/en-us/research/group/prose/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/microsoft/prose", icon = 'fa-solid fa-code' },
]
applications = ["Program Synthesizer"]
developers = ["Microsoft Research"]
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Microsoft Program Synthesis using Examples SDK is a framework of technologies for the automatic generation of programs from input-output examples. This repo includes samples and sample data for the Microsoft Program Synthesis using Example SDK.

16
tools/program-synth/rbsyn.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'RbSyn'
subtitle = 'Program Synthesis'
links = [ { title = "Source Code", url = "https://github.com/ku-progsys/rbsyn", icon = 'fa-solid fa-code' },
]
applications = ["Program Synthesizer"]
developers = []
licenses = ["BSD-3-Clause"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Program synthesis for Ruby

18
tools/program-synth/tree-diffusion.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'Tree Diffusion'
subtitle = 'Program Synthesis'
links = [
{ title = "Homepage", url = "https://tree-diffusion.github.io/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/revalo/tree-diffusion", icon = 'fa-solid fa-code' },
]
applications = ["Program Synthesizer"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Diffusion on syntax trees for program synthesis

18
tools/programs/gillian.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'Gillian'
subtitle = 'Program Prover'
links = [
{ title = "Homepage", url = "https://gillianplatform.github.io/sphinx/index.html", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/GillianPlatform/Gillian", icon = 'fa-solid fa-code' },
]
applications = ["Program Prover"]
developers = []
licenses = ["BSD-3-Clause"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Gillian is a multi-language analysis platform supporting, e.g., verification and symbolic testing. Gillian has currently been instantiated to C, JavaScript, and Rust.

10
tools/proof-assist/_index.md Normal file
View File

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

18
tools/proof-assist/andromeda.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'Andromeda'
subtitle = 'Proof Assistant'
links = [
{ title = "Homepage", url = "https://www.andromeda-prover.org/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/Andromedans/andromeda", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = []
licenses = ["BSD-3-Clause"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Andromeda 2 is a proof checker for user-definable dependently-typed theories.

18
tools/proof-assist/arend.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'Arend'
subtitle = 'Proof Assistant'
links = [
{ title = "Homepage", url = "https://arend-lang.github.io/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/JetBrains/Arend", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = ["JetBrains"]
licenses = ["Apache-2.0"]
inputs = []
interfaces = ["CLI","Library"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Arend is a theorem prover and a programming language based on Homotopy Type Theory.

19
tools/proof-assist/arvo.md Normal file
View File

@@ -0,0 +1,19 @@
+++
title = 'Arvo'
subtitle = 'Proof Assistant'
links = [ { title = "Source Code", url = "https://github.com/uwplse/arvo", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = ["PLSE lab"]
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2015
draft = false
date = 2025-08-22
+++
{{<inactive year="2015">}}
Arvo is a proof assistant from the PLSE lab.

18
tools/proof-assist/aya.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'Aya Prover'
subtitle = 'Proof Assistant'
links = [
{ title = "Homepage", url = "https://www.aya-prover.org/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/aya-prover/aya-dev", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI","IDE Integration"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
A proof assistant designed for formalizing math and type-directed programming.

19
tools/proof-assist/blazeit.md Normal file
View File

@@ -0,0 +1,19 @@
+++
title = 'BlazeIt'
subtitle = 'Proof Assistant'
links = [ { title = "Source Code", url = "https://github.com/pjreddie/blazeit", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = []
licenses = ["Yolo"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2015
draft = false
date = 2025-08-22
+++
{{<inactive year="2015">}}
A proof assistant.

16
tools/proof-assist/cur.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'cur'
subtitle = 'Proof Assistant'
links = [ { title = "Source Code", url = "https://github.com/wilbowma/cur", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover","Specification Language"]
developers = []
licenses = ["BSD-2-Clause"]
inputs = ["Cur"]
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
A language with static dependent-types and dynamic types, type annotations and parentheses, theorem proving and meta-programming.

16
tools/proof-assist/holbert.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'Holbert'
subtitle = 'Proof Assistant'
links = [ { title = "Source Code", url = "https://github.com/liamoc/holbert", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = []
licenses = ["BSD-3-Clause"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Holbert is an interactive theorem prover, or proof assistant, based on higher order logic and natural deduction. Furthermore, Holbert is graphical.

18
tools/proof-assist/knuckledragger.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'knuckledragger'
subtitle = 'Proof Assistant'
links = [
{ title = "Homepage", url = "https://www.philipzucker.com/knuckledragger/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/philzook58/knuckledragger", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Knuckledragger is an attempt at creating a down to earth, highly automated interactive proof assistant in python. The goal is to support applications like software/hardware verification, calculus, equational reasoning, and numerical bounds.

16
tools/proof-assist/lambdapi.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'Lambdapi'
subtitle = 'Proof Assistant'
links = [ { title = "Source Code", url = "https://github.com/Deducteam/lambdapi", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = []
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Proof assistant based on the λΠ-calculus modulo rewriting

16
tools/proof-assist/lisa.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'LISA'
subtitle = 'Proof Assistant'
links = [ { title = "Source Code", url = "https://github.com/epfl-lara/lisa", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = []
licenses = ["Apache-2.0"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
LISA is a proof assistant based on first-order logic sequent calculus and set theory.

16
tools/proof-assist/narya.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'Narya'
subtitle = 'Proof Assistant'
links = [ { title = "Source Code", url = "https://github.com/gwaithimirdain/narya", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = []
licenses = ["GPL-3.0"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Narya: A proof assistant for higher-dimensional type theory

18
tools/proof-assist/qrhl-tool.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'Qrhl-tool'
subtitle = 'Proof Assistant'
links = [
{ title = "Homepage", url = "https://dominique-unruh.github.io/qrhl-tool/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/dominique-unruh/qrhl-tool", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Qrhl-tool is an interactive theorem prover for qRHL (quantum relational Hoare logic), specifically for quantum and post-quantum security proofs.

18
tools/proof-assist/sasylf.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'SASyLF'
subtitle = 'Proof Assistant'
links = [
{ title = "Homepage", url = "https://www.cs.cmu.edu/~aldrich/SASyLF/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/boyland/sasylf", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = []
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
SASyLF (pronounced "Sassy Elf") is an LF-based proof assistant specialized to checking theorems about programming languages and logics.

10
tools/runtime/_index.md Normal file
View File

@@ -0,0 +1,10 @@
+++
title = "Runtime Verifiers"
layout = "section"
+++
This page lists all of the Runtime Verifiers 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.

16
tools/runtime/contractlarva.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'contractLarva'
subtitle = 'Runtime Verifier'
links = [ { title = "Source Code", url = "https://github.com/gordonpace/contractLarva", icon = 'fa-solid fa-code' },
]
applications = ["Runtime Verifier"]
developers = []
licenses = ["Apache-2.0"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
contractLarva is a runtime verification tool for Solidity contracts. For more details about the tool check out the user manual in the docs folder.

18
tools/runtime/copilot.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'Copilot'
subtitle = 'Runtime Verifier'
links = [
{ title = "Homepage", url = "https://copilot-language.github.io/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/Copilot-Language/copilot", icon = 'fa-solid fa-code' },
]
applications = ["Runtime Verifier"]
developers = []
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Copilot is a runtime verification framework for hard real-time systems.

18
tools/runtime/detecter.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'detectEr'
subtitle = 'Runtime Verifier'
links = [
{ title = "Homepage", url = "https://duncanatt.github.io/detecter/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/duncanatt/detecter", icon = 'fa-solid fa-code' },
]
applications = ["Runtime Verifier"]
developers = []
licenses = ["GPL-3.0"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
A runtime verification tool for monitoring asynchronous component systems.

16
tools/runtime/easyrte.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'easy-rte'
subtitle = 'Runtime Verifier'
links = [ { title = "Source Code", url = "https://github.com/PRETgroup/easy-rte", icon = 'fa-solid fa-code' },
]
applications = ["Runtime Verifier"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Toolchain to automatically generate and verify HW or SW runtime enforcers from text-based framework

15
tools/runtime/hlola.md Normal file
View File

@@ -0,0 +1,15 @@
+++
title = 'hlola'
subtitle = 'Runtime Verifier'
links = [ { title = "Source Code", url = "https://github.com/imdea-software/hlola", icon = 'fa-solid fa-code' },
]
applications = ["Runtime Verifier"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++

19
tools/runtime/ivoryrtverification.md Normal file
View File

@@ -0,0 +1,19 @@
+++
title = 'ivory-rtverification'
subtitle = 'Runtime Verifier'
links = [ { title = "Source Code", url = "https://github.com/GaloisInc/ivory-rtverification", icon = 'fa-solid fa-code' },
]
applications = ["Runtime Verifier"]
developers = []
licenses = ["BSD-3-Clause"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2014
draft = false
date = 2025-08-22
+++
{{<inactive year="2014">}}
Runtime verification for C code via a GCC plugin architecture.

19
tools/runtime/javamop.md Normal file
View File

@@ -0,0 +1,19 @@
+++
title = 'JavaMOP'
subtitle = 'Runtime Verifier'
links = [ { title = "Source Code", url = "https://github.com/runtimeverification/javamop", icon = 'fa-solid fa-code' },
]
applications = ["Runtime Verifier"]
developers = []
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2019
draft = false
date = 2025-08-22
+++
{{<inactive year="2019">}}
Runtime verification system for Java, using AspectJ for instrumentation.

16
tools/runtime/mesa.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'MESA'
subtitle = 'Runtime Verifier'
links = [ { title = "Source Code", url = "https://github.com/NASA-SW-VnV/mesa", icon = 'fa-solid fa-code' },
]
applications = ["Runtime Verifier"]
developers = []
licenses = ["NASA Open Source"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
MESA is a framework that provides runtime verification of distributed systems in a nonintrusive manner.

16
tools/runtime/paranoidscientist.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'Paranoid Scientist'
subtitle = 'Runtime Verifier'
links = [ { title = "Source Code", url = "https://github.com/mwshinn/paranoidscientist", icon = 'fa-solid fa-code' },
]
applications = ["Runtime Verifier"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["Library"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Runtime software verification and automated testing for scientific software in Python

19
tools/runtime/qea.md Normal file
View File

@@ -0,0 +1,19 @@
+++
title = 'QEA'
subtitle = 'Runtime Verifier'
links = [ { title = "Source Code", url = "https://github.com/selig/qea", icon = 'fa-solid fa-code' },
]
applications = ["Runtime Verifier","Specification Language"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2019
draft = false
date = 2025-08-22
+++
{{<inactive year="2019">}}
Quantified Event Automata (QEA) is a specification formalism developed for runtime monitoring. This project is a reimplementation and extension of QEA monitoring techniques (explored in Giles Reger’s PhD work) by Master’s student Helena Cuenca.

19
tools/runtime/r2u2.md Normal file
View File

@@ -0,0 +1,19 @@
+++
title = 'R2U2'
subtitle = 'Runtime Verifier'
links = [
{ title = "Homepage", url = "https://r2u2.temporallogic.org/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/R2U2/r2u2", icon = 'fa-solid fa-code' },
{ title = "Playground", url = "https://r2u2.temporallogic.org/playground/", icon = 'fa-solid fa-gamepad' }
]
applications = ["Runtime Verifier"]
developers = ["Iowa State University"]
licenses = ["MIT", "Apache-2.0"]
inputs = []
interfaces = ["Web","CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
The Realizable Responsive Unobtrusive Unit is an online runtime monitor framework.

16
tools/runtime/rosmonitoring.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'ROSMonitoring'
subtitle = 'Runtime Verifier'
links = [ { title = "Source Code", url = "https://github.com/autonomy-and-verification-uol/ROSMonitoring", icon = 'fa-solid fa-code' },
]
applications = ["Runtime Verifier"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
ROSMonitoring is a framework developed for verifying at runtime the messages exchanged in a ROS system.

19
tools/runtime/rosrv.md Normal file
View File

@@ -0,0 +1,19 @@
+++
title = 'ROSRV'
subtitle = 'Runtime Verifier'
links = [ { title = "Source Code", url = "https://github.com/cansuerdogan/ROSRV", icon = 'fa-solid fa-code' },
]
applications = ["Runtime Verifier"]
developers = []
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2014
draft = false
date = 2025-08-22
+++
{{<inactive year="2014">}}
ROSRV is a runtime verification framework for the Robot Operating System (ROS).

21
tools/runtime/rvhyper.md Normal file
View File

@@ -0,0 +1,21 @@
+++
title = 'RVHyper'
subtitle = 'Runtime Verifier'
links = [
{ title = "Homepage", url = "https://www.react.uni-saarland.de/tools/rvhyper/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/reactive-systems/rvhyper", icon = 'fa-solid fa-code' },
]
applications = ["Runtime Verifier"]
developers = []
licenses = ["GPL-3.0"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2019
draft = false
date = 2025-08-22
+++
{{<inactive year="2019">}}
RVHyper - A Runtime Verification Tool for Temporal Hyperproperties.

18
tools/sat-smt/agda.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'Agda 2'
subtitle = ''
links = [
{ title = "Homepage", url = "https://wiki.portal.chalmers.se/agda/pmwiki.php", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/agda/agda", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover","Specification Language"]
developers = []
licenses = ["MIT"]
inputs = ["Agda"]
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-21
+++
Agda is a dependently typed programming language / interactive theorem prover.

18
tools/sat-smt/chyp.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'Chyp'
subtitle = 'Interactive Theroem Prover'
links = [
{ title = "Homepage", url = "https://github.com/akissinger/chyp", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/akissinger/chyp", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = ["University of Oxford"]
licenses = ["Apache-2.0"]
inputs = ["Chyp"]
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-21
+++
Chyp (pronounced "chip") is an interactive theorem prover for symmetric monoidal categories (SMCs), a.k.a. process theories.

2
tools/sat-smt/cvc4.md
View File

@@ -10,7 +10,7 @@ links = [
]
applications = ['SMT Solver', 'Theorem Prover']
developers = ['Stanford University', 'University of Iowa']
licenses = ['BSD']
licenses = ['BSD-3-Clause']
inputs = ['SMTLIB2']
interfaces = ['CLI', 'Online']
maintenance = ['Not Maintained']

2
tools/sat-smt/cvc5.md
View File

@@ -10,7 +10,7 @@ links = [
]
applications = ['SMT Solver', 'Theorem Prover']
developers = ['Stanford University', 'University of Iowa']
licenses = ['BSD']
licenses = ['BSD-3-Clause']
inputs = ['SMTLIB2']
interfaces = ['CLI', 'Online']
maintenance = ['Actively Maintained']

21
tools/sat-smt/hilbert.md Normal file
View File

@@ -0,0 +1,21 @@
+++
title = 'Hilbert'
subtitle = 'Interactive Theorem Prover'
links = [
{ title = "Homepage", url = "https://github.com/liamoc/hilbert", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/liamoc/hilbert", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = ["ConsenSys"]
licenses = ["Apache-2.0"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2014
draft = false
date = 2025-08-21
+++
{{<inactive year="2014">}}
Hilbert is a theorem prover designed for people who don't want to learn a theorem prover, specifically students studying formal treatments of programming languages.

18
tools/sat-smt/isabelle.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'Isabelle'
subtitle = 'Interactive Theorem Prover'
links = [
{ title = "Homepage", url = "https://isabelle.in.tum.de/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://isabelle-dev.sketis.net/source/isabelle", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = ["University of Cambridge","Technische Universitat Munchen"]
licenses = ["BSD-2-Clause"]
inputs = ["Isabelle"]
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-21
+++
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus.

18
tools/sat-smt/megalodon.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'Megalodon'
subtitle = 'Interactive Theorem Prover'
links = [
{ title = "Homepage", url = "https://github.com/ai4reason/Megalodon", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/ai4reason/Megalodon", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = []
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-21
+++
Megalodon is an open source interactive theorem prover and proof checker.

21
tools/sat-smt/otter.md Normal file
View File

@@ -0,0 +1,21 @@
+++
title = 'Otter'
subtitle = 'Theorem Prover'
links = [
{ title = "Homepage", url = "https://www.cs.unm.edu/~mccune/otter/", icon = 'fa-solid fa-home' },
]
applications = ["Theorem Prover"]
developers = []
licenses = []
inputs = []
interfaces = []
maintenance = ["Not Maintained"]
updated_year = 2015
draft = false
date = 2025-08-22
+++
{{<inactive>}}
Otter/Mace2 are no longer being actively developed, and maintenance and support minimal.
We recommend using Otter/Mace2's successor Prover9/Mace4 instead.

17
tools/sat-smt/prover9.md Normal file
View File

@@ -0,0 +1,17 @@
+++
title = 'Prover9'
subtitle = 'Theorem Prover'
links = [
{ title = "Homepage", url = "https://www.cs.unm.edu/~mccune/prover9/", icon = 'fa-solid fa-home' },
]
applications = ["Theorem Prover"]
developers = []
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-21
+++
Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover.

18
tools/sat-smt/pvs.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'PVS'
subtitle = 'Interactive Theorem Prover'
links = [
{ title = "Homepage", url = "https://pvs.csl.sri.com/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "github.com/SRI-CSL/PVS", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = ["SRI International"]
licenses = ["GPL-2.0"]
inputs = ["PVS"]
interfaces = ["CLI","GUI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-21
+++
PVS is a mechanized environment for formal specification and verification. PVS consists of a specification language, a large number of predefined theories, a type checker, an interactive theorem prover that supports the use of several decision procedures and a symbolic model checker, various utilities including a code generator and a random tester, documentation, formalized libraries, and examples that illustrate different methods of using the system in several application areas.

20
tools/sat-smt/rocq.md Normal file
View File

@@ -0,0 +1,20 @@
+++
title = 'Rocq'
subtitle = 'Interactive Theorem Prover'
links = [
{ title = "Homepage", url = "https://rocq-prover.org/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/rocq-prover/rocq", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = ["Rocq Team"]
licenses = ["LGPL-2.1"]
inputs = ["Rocq"]
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-21
+++
A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics, computer science and more.
The Rocq Prover was formerly known as the Coq Proof Assistant.

19
tools/sat-smt/setheo.md Normal file
View File

@@ -0,0 +1,19 @@
+++
title = 'SETHEO'
subtitle = 'Theorem Prover'
links = [ { title = "Source Code", url = "https://github.com/theoremprover-museum/SETHEO", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = []
licenses = []
inputs = []
interfaces = ["CLI"]
maintenance = ["Not Maintained"]
updated_year = 2017
draft = false
date = 2025-08-22
+++
{{<inactive year="2017">}}
SETHEO is a theorem prover for first-order logic based on some variant of the connection method.

2
tools/sat-smt/vampire.md
View File

@@ -10,7 +10,7 @@ links = [
]
applications = ['Theorem Prover']
developers = ['TU Wien']
licenses = ['BSD']
licenses = ['BSD-3-Clause']
# inputs = ['']
interfaces = ['CLI']
maintenance = ['Actively Maintained']

2
tools/sat-smt/verit.md
View File

@@ -13,7 +13,7 @@ links = [
applications = ['SMT Solver']
developers = ['LORIA', 'ULiege']
licenses = ['BSD']
licenses = ['BSD-2-Clause']
inputs = ['SMTLIB2', 'DIMACS']
interfaces = ['CLI']
maintenance = ['Actively Maintained']

18
tools/sat-smt/wytp.md Normal file
View File

@@ -0,0 +1,18 @@
+++
title = 'Whiley Theorem Prover'
subtitle = 'Interactive Theorem Prover'
links = [
{ title = "Homepage", url = "https://github.com/Whiley/WhileyTheoremProver", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/Whiley/WhileyTheoremProver", icon = 'fa-solid fa-code' },
]
applications = ["Theorem Prover"]
developers = ["ConsenSys"]
licenses = ["Apache-2.0"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-21
+++
The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.

2
tools/sat-smt/zipperposition.md
View File

@@ -10,7 +10,7 @@ links = [
]
applications = ['Theorem Prover']
developers = ['TU Wien']
licenses = ['BSD']
licenses = ['BSD-2-Clause']
# inputs = ['']
interfaces = ['CLI']
maintenance = ['Actively Maintained']

10
tools/static-analysis/_index.md Normal file
View File

@@ -0,0 +1,10 @@
+++
title = "Static Anaylsis Tools"
layout = "section"
+++
This page lists all of the Static Anaylsis 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.

16
tools/static-analysis/cobra.md Normal file
View File

@@ -0,0 +1,16 @@
+++
title = 'Cobra'
subtitle = 'Static Code Analyzer'
links = [ { title = "Source Code", url = "https://github.com/nimble-code/Cobra", icon = 'fa-solid fa-code' },
]
applications = ["Static Analyzer"]
developers = []
licenses = ["MIT"]
inputs = []
interfaces = ["CLI"]
maintenance = ["Actively Maintained"]
draft = false
date = 2025-08-22
+++
Cobra is a fast code analyzer that can be used to interactively probe and query up to millions of lines of code.