Fix #29

Close #28
Close #26
2025-08-22 13:50:11 -06:00 · 2025-08-22 13:44:11 -06:00 · 2025-08-22 13:42:01 -06:00 · 2025-08-22 13:39:37 -06:00 · 2025-08-22 13:24:48 -06:00 · 2025-08-22 13:09:52 -06:00
167 changed files with 1996 additions and 109 deletions
--- a/_index.md
+++ b/_index.md
@@ -21,4 +21,3 @@ Taxonomy Data
 {{<button href="/contribute">}}
 Contribute
 {{</button>}} 
-
--- a/new-tool.md
+++ b/new-tool.md
@@ -0,0 +1,436 @@
+++
+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.
+
+Reset the form with **Double Click** on reset button for safety.
+
+{{<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>}}
--- a/tools/mc/abc.md
+++ b/tools/mc/abc.md
@@ -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
--- a/tools/mc/avr.md
+++ b/tools/mc/avr.md
@@ -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 
--- a/tools/mc/blast.md
+++ b/tools/mc/blast.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://forge.ispras.ru/projects/blast/repository", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/cadp.md
+++ b/tools/mc/cadp.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://forge.ispras.ru/projects/blast/repository", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/cgaal.md
+++ b/tools/mc/cgaal.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/d702e20/CGAAL", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/concuerror.md
+++ b/tools/mc/concuerror.md
@@ -5,12 +5,12 @@ 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 = "Source Code", url = "https://github.com/parapluu/Concuerror", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
 developers = ['Uppsala University']
-licenses = ['BSD']
+licenses = ['BSD-2-Clause']
 # inputs = ['Sally']
 # interfaces = ['CLI']
 maintenance = ['Actively Maintained']
--- a/tools/mc/cpachecker.md
+++ b/tools/mc/cpachecker.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://gitlab.com/sosy-lab/software/cpachecker/", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/dscheck.md
+++ b/tools/mc/dscheck.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/ocaml-multicore/dscheck", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/eldarica.md
+++ b/tools/mc/eldarica.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/uuverifiers/eldarica", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/esbmc.md
+++ b/tools/mc/esbmc.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/esbmc/esbmc", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/fast-downward-pdr.md
+++ b/tools/mc/fast-downward-pdr.md
@@ -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. 
--- a/tools/mc/fbpdr.md
+++ b/tools/mc/fbpdr.md
@@ -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.
--- a/tools/mc/fuseic3.md
+++ b/tools/mc/fuseic3.md
@@ -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.
--- a/tools/mc/geyser.md
+++ b/tools/mc/geyser.md
@@ -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-brands fa-github'  },
-    # { 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 
--- a/tools/mc/imitator.md
+++ b/tools/mc/imitator.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/imitator-model-checker/imitator", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Parameter Synthesizer']
--- a/tools/mc/imspin.md
+++ b/tools/mc/imspin.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/MrDiver/ImSpin", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/intrepyd.md
+++ b/tools/mc/intrepyd.md
@@ -5,12 +5,12 @@ 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 = "Source Code", url = "https://github.com/formalmethods/intrepid", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
 # developers = ['']
-licenses = ['BSD']
+licenses = ['BSD-3-Clause']
 # inputs = ['Sally']
 # interfaces = ['CLI']
 maintenance = ['Not Maintained']
--- a/tools/mc/ivy.md
+++ b/tools/mc/ivy.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/kenmcmil/ivy", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Protocol Verifier']
--- a/tools/mc/kind2.md
+++ b/tools/mc/kind2.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/kind2-mc/kind2", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/ltsa.md
+++ b/tools/mc/ltsa.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/ltsmin.md
+++ b/tools/mc/ltsmin.md
@@ -5,12 +5,12 @@ 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 = "Source Code", url = "https://github.com/utwente-fmt/ltsmin", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
 developers = ['University of Twente']
-licenses = ['BSD']
+licenses = ['BSD-3-Clause']
 # inputs = ['Sally']
 # interfaces = ['CLI']
 maintenance = ['Actively Maintained']
--- a/tools/mc/mcltlrs.md
+++ b/tools/mc/mcltlrs.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/NotBad4U/mcltl-rs", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/mcrl2.md
+++ b/tools/mc/mcrl2.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/mCRL2org/mCRL2", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/mercury.md
+++ b/tools/mc/mercury.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/rtsaad/mercury", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/munta.md
+++ b/tools/mc/munta.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/wimmers/munta", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/nusmv.md
+++ b/tools/mc/nusmv.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/nuxmv.md
+++ b/tools/mc/nuxmv.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/pdrc.md
+++ b/tools/mc/pdrc.md
@@ -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" 
--- a/tools/mc/pdrlia.md
+++ b/tools/mc/pdrlia.md
@@ -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
--- a/tools/mc/pnmc.md
+++ b/tools/mc/pnmc.md
@@ -5,12 +5,12 @@ 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 = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
 # developers = ['University of Twente']
-licenses = ['BSD']
+licenses = ['BSD-2-Clause']
 # inputs = ['Sally']
 # interfaces = ['CLI']
 maintenance = ['Actively Maintained']
--- a/tools/mc/pypl.md
+++ b/tools/mc/pypl.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/nclarius/pyPL", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker', 'Model Generator', 'Theorem Prover']
--- a/tools/mc/reach.md
+++ b/tools/mc/reach.md
@@ -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.
--- a/tools/mc/ric3.md
+++ b/tools/mc/ric3.md
@@ -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 
--- a/tools/mc/romeo.md
+++ b/tools/mc/romeo.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/rumur.md
+++ b/tools/mc/rumur.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/Smattr/rumur", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/sally.md
+++ b/tools/mc/sally.md
@@ -5,7 +5,7 @@ title = 'Sally'
 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'  },
+    { title = "Source Code", url = "https://github.com/SRI-CSL/sally", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/simplepdr.md
+++ b/tools/mc/simplepdr.md
@@ -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.
--- a/tools/mc/smpt.md
+++ b/tools/mc/smpt.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/nicolasAmat/SMPT", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/spaceex.md
+++ b/tools/mc/spaceex.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://forge.ispras.ru/projects/blast/repository", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Hybrid Systems']
--- a/tools/mc/spin.md
+++ b/tools/mc/spin.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/nimble-code/Spin", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/stateright.md
+++ b/tools/mc/stateright.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/stateright/stateright", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/tapaal.md
+++ b/tools/mc/tapaal.md
@@ -5,12 +5,12 @@ 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 = "Source Code", url = "https://github.com/TAPAAL/", icon = 'fa-solid fa-code'  },
    # { 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']
+licenses = ['GPL-2.0']
 # inputs = ['Sally']
 # interfaces = ['CLI']
 maintenance = ['Actively Maintained']
--- a/tools/mc/timesolver.md
+++ b/tools/mc/timesolver.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/jkeiren/TimeSolver", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/uppaal.md
+++ b/tools/mc/uppaal.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/imitator-model-checker/imitator", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker']
--- a/tools/mc/z3ic3pdr.md
+++ b/tools/mc/z3ic3pdr.md
@@ -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. 
--- a/tools/mod/jani.md
+++ b/tools/mod/jani.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/koehlma/momba", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Modeling Language']
--- a/tools/mod/momba.md
+++ b/tools/mod/momba.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/koehlma/momba", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Modeling Framework']
--- a/tools/mod/tlaplus.md
+++ b/tools/mod/tlaplus.md
@@ -5,12 +5,12 @@ 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 = "Source Code", url = "https://github.com/TAPAAL/", icon = 'fa-solid fa-code'  },
    # { 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']
+licenses = []
 # inputs = ['Sally']
 # interfaces = ['CLI']
 maintenance = ['Actively Maintained']
--- a/tools/nn/_index.md
+++ b/tools/nn/_index.md
@@ -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.
--- a/tools/nn/dnnf.md
+++ b/tools/nn/dnnf.md
@@ -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. 
--- a/tools/nn/dnnv.md
+++ b/tools/nn/dnnv.md
@@ -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.
--- a/tools/nn/fmdnn.md
+++ b/tools/nn/fmdnn.md
@@ -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 
--- a/tools/nn/incremental-dnn-verification.md
+++ b/tools/nn/incremental-dnn-verification.md
@@ -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 
--- a/tools/nn/ivan.md
+++ b/tools/nn/ivan.md
@@ -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
--- a/tools/nn/verapak.md
+++ b/tools/nn/verapak.md
@@ -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.
--- a/tools/nn/verifydnn.md
+++ b/tools/nn/verifydnn.md
@@ -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 
--- a/tools/nn/verifying-dnn.md
+++ b/tools/nn/verifying-dnn.md
@@ -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 
--- a/tools/nn/verigauge.md
+++ b/tools/nn/verigauge.md
@@ -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.
--- a/tools/nn/veristable.md
+++ b/tools/nn/veristable.md
@@ -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 
--- a/tools/prob/caesar.md
+++ b/tools/prob/caesar.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/moves-rwth/caesar", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Probabilistic Program Prover']
--- a/tools/prob/comics.md
+++ b/tools/prob/comics.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/moves-rwth/storm", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Counterexample Generator']
--- a/tools/prob/dftgui.md
+++ b/tools/prob/dftgui.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/moves-rwth/dft-gui", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Visualizer']
--- a/tools/prob/prinsys.md
+++ b/tools/prob/prinsys.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/moves-rwth/caesar", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Probabilistic Invariant Synthesizer']
--- a/tools/prob/prism.md
+++ b/tools/prob/prism.md
@@ -5,7 +5,7 @@ title = 'PRISM'
 subtitle = 'Probabilistic Model Checker'
 links = [
    { title = "Homepage", url = "https://prismmodelchecker.org/", icon = 'fa-solid fa-home' },
-    { title = "Source Code", url = "https://github.com/prismmodelchecker/prism", icon = 'fa-brands fa-github'  },
+    { title = "Source Code", url = "https://github.com/prismmodelchecker/prism", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Probabilistic Model Checker']
--- a/tools/prob/prophesy.md
+++ b/tools/prob/prophesy.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/moves-rwth/prophesy", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Parameter Synthesizer']
--- a/tools/prob/stamina.md
+++ b/tools/prob/stamina.md
@@ -5,7 +5,7 @@ title = 'STAMINA'
 subtitle = 'Probabilistic Model Checker'
 links = [
    { title = "Homepage", url = "https://staminachecker.org/", icon = 'fa-solid fa-home' },
-    { title = "Source Code", url = "https://staminachecker.org/source.html", icon = 'fa-brands fa-github'  },
+    { title = "Source Code", url = "https://staminachecker.org/source.html", icon = 'fa-solid fa-code'  },
    { title = "Playground", url = "https://staminachecker.org/run.html", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Probabilistic Model Checker']
--- a/tools/prob/storm.md
+++ b/tools/prob/storm.md
@@ -5,7 +5,7 @@ title = 'Storm'
 subtitle = 'Probabilistic Model Checker'
 links = [
    { title = "Homepage", url = "https://www.stormchecker.org/", icon = 'fa-solid fa-home' },
-    { title = "Source Code", url = "https://github.com/moves-rwth/storm", icon = 'fa-brands fa-github'  },
+    { title = "Source Code", url = "https://github.com/moves-rwth/storm", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Probabilistic Model Checker']
--- a/tools/program-synth/_index.md
+++ b/tools/program-synth/_index.md
@@ -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.
--- a/tools/program-synth/codegen2.md
+++ b/tools/program-synth/codegen2.md
@@ -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 
--- a/tools/program-synth/fiat.md
+++ b/tools/program-synth/fiat.md
@@ -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 
--- a/tools/program-synth/lakeroad.md
+++ b/tools/program-synth/lakeroad.md
@@ -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 
--- a/tools/program-synth/minisynth.md
+++ b/tools/program-synth/minisynth.md
@@ -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 
--- a/tools/program-synth/neuralkanren.md
+++ b/tools/program-synth/neuralkanren.md
@@ -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 
--- a/tools/program-synth/prose.md
+++ b/tools/program-synth/prose.md
@@ -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. 
--- a/tools/program-synth/rbsyn.md
+++ b/tools/program-synth/rbsyn.md
@@ -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 
--- a/tools/program-synth/tree-diffusion.md
+++ b/tools/program-synth/tree-diffusion.md
@@ -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 
--- a/tools/programs/aeneas.md
+++ b/tools/programs/aeneas.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/AeneasVerif/aeneas", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Program Prover', 'Rust Verifier']
--- a/tools/programs/creusot.md
+++ b/tools/programs/creusot.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/creusot-rs/creusot", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Program Prover', 'Rust Verifier']
--- a/tools/programs/dafny.md
+++ b/tools/programs/dafny.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/dafny-lang/dafny", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Program Prover']
--- a/tools/programs/gillian.md
+++ b/tools/programs/gillian.md
@@ -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.
--- a/tools/programs/kani.md
+++ b/tools/programs/kani.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/model-checking/kani", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Model Checker', 'Rust Verifier']
--- a/tools/programs/loom.md
+++ b/tools/programs/loom.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/tokio-rs/loom", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Rust Verifier']
--- a/tools/programs/miri.md
+++ b/tools/programs/miri.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/rust-lang/miri", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Rust Verifier']
--- a/tools/programs/prusti.md
+++ b/tools/programs/prusti.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/viperproject/prusti-dev", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Rust Verifier']
--- a/tools/programs/shuttle.md
+++ b/tools/programs/shuttle.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/awslabs/shuttle", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Rust Verifier']
--- a/tools/programs/verus.md
+++ b/tools/programs/verus.md
@@ -5,7 +5,7 @@ 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 = "Source Code", url = "https://github.com/verus-lang/verus", icon = 'fa-solid fa-code'  },
    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
 ]
 applications = ['Rust Verifier']
--- a/tools/proof-assist/_index.md
+++ b/tools/proof-assist/_index.md
@@ -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.
--- a/tools/proof-assist/andromeda.md
+++ b/tools/proof-assist/andromeda.md
@@ -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.
--- a/tools/proof-assist/arend.md
+++ b/tools/proof-assist/arend.md
@@ -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.
--- a/tools/proof-assist/arvo.md
+++ b/tools/proof-assist/arvo.md
@@ -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.
--- a/tools/proof-assist/aya.md
+++ b/tools/proof-assist/aya.md
@@ -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.
--- a/tools/proof-assist/blazeit.md
+++ b/tools/proof-assist/blazeit.md
@@ -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.
--- a/tools/proof-assist/cur.md
+++ b/tools/proof-assist/cur.md
@@ -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.
--- a/tools/proof-assist/holbert.md
+++ b/tools/proof-assist/holbert.md
@@ -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.
--- a/tools/proof-assist/knuckledragger.md
+++ b/tools/proof-assist/knuckledragger.md
@@ -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.
--- a/tools/proof-assist/lambdapi.md
+++ b/tools/proof-assist/lambdapi.md
@@ -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 
--- a/tools/proof-assist/lisa.md
+++ b/tools/proof-assist/lisa.md
@@ -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.
--- a/tools/proof-assist/narya.md
+++ b/tools/proof-assist/narya.md
@@ -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
--- a/Show More
+++ b/Show More
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
Landon Taylor	0cb4f7ed82	fix icon	2025-08-21 16:15:06 -06:00
Landon Taylor	97a87a1679	Close #17 , add tools	2025-08-21 16:14:46 -06:00
Landon Taylor	f1f2354db2	Add Why3, close #16	2025-08-21 15:49:03 -06:00