From 0e74e27d2c7f66eb5cb160c86f6add66d30dc0f9 Mon Sep 17 00:00:00 2001 From: Landon Taylor Date: Thu, 10 Jul 2025 12:52:26 -0600 Subject: [PATCH] Fix #15 --- tools/programs/aeneas.md | 22 ++++++++++++++++++++++ tools/programs/creusot.md | 22 ++++++++++++++++++++++ tools/programs/kani.md | 22 ++++++++++++++++++++++ tools/programs/loom.md | 22 ++++++++++++++++++++++ tools/programs/miri.md | 22 ++++++++++++++++++++++ tools/programs/prusti.md | 22 ++++++++++++++++++++++ tools/programs/shuttle.md | 22 ++++++++++++++++++++++ tools/programs/verus.md | 22 ++++++++++++++++++++++ 8 files changed, 176 insertions(+) create mode 100644 tools/programs/aeneas.md create mode 100644 tools/programs/creusot.md create mode 100644 tools/programs/kani.md create mode 100644 tools/programs/loom.md create mode 100644 tools/programs/miri.md create mode 100644 tools/programs/prusti.md create mode 100644 tools/programs/shuttle.md create mode 100644 tools/programs/verus.md diff --git a/tools/programs/aeneas.md b/tools/programs/aeneas.md new file mode 100644 index 0000000..2bab57a --- /dev/null +++ b/tools/programs/aeneas.md @@ -0,0 +1,22 @@ ++++ +date = 2025-07-10 +draft = false +title = 'Aeneas' +subtitle = 'Rust Verifier' +links = [ + { title = "Homepage", url = "https://aeneasverif.github.io/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/AeneasVerif/aeneas", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Program Prover', 'Rust Verifier'] +developers = ['Microsoft Research', 'Inria'] +licenses = ['Apache-2.0'] +inputs = ['Rust'] +interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['Barbosa2022'] ++++ + + +Aeneas (pronunced [Ay-nay-as]) is a verification toolchain for Rust programs. \ No newline at end of file diff --git a/tools/programs/creusot.md b/tools/programs/creusot.md new file mode 100644 index 0000000..febc71b --- /dev/null +++ b/tools/programs/creusot.md @@ -0,0 +1,22 @@ ++++ +date = 2025-07-10 +draft = false +title = 'Creusot' +subtitle = 'Rust Verifier' +links = [ + # { title = "Homepage", url = "https://dafny.org/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/creusot-rs/creusot", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Program Prover', 'Rust Verifier'] +# developers = ['Amazon Web Services'] +licenses = ['LGPLv2.1'] +inputs = ['Rust'] +interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['Barbosa2022'] ++++ + + +Creusot is a deductive verifier for Rust code. \ No newline at end of file diff --git a/tools/programs/kani.md b/tools/programs/kani.md new file mode 100644 index 0000000..d02b6eb --- /dev/null +++ b/tools/programs/kani.md @@ -0,0 +1,22 @@ ++++ +date = 2025-07-10 +draft = false +title = 'Kani' +subtitle = 'Rust Verifier' +links = [ + { title = "Homepage", url = "https://model-checking.github.io/kani/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/model-checking/kani", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Model Checker', 'Rust Verifier'] +# developers = ['Microsoft Research', 'Inria'] +licenses = ['Apache-2.0', 'MIT'] +inputs = ['Rust'] +interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['Barbosa2022'] ++++ + + +The Kani Rust Verifier is a bit-precise model checker for Rust. \ No newline at end of file diff --git a/tools/programs/loom.md b/tools/programs/loom.md new file mode 100644 index 0000000..97d6e33 --- /dev/null +++ b/tools/programs/loom.md @@ -0,0 +1,22 @@ ++++ +date = 2025-07-10 +draft = false +title = 'Loom' +subtitle = 'Rust Verifier' +links = [ + # { title = "Homepage", url = "https://www.pm.inf.ethz.ch/research/prusti.html", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/tokio-rs/loom", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Rust Verifier'] +developers = ['Tokio'] +licenses = ['MIT'] +inputs = ['Rust'] +interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['Barbosa2022'] ++++ + + +Loom is a testing tool for concurrent Rust code. \ No newline at end of file diff --git a/tools/programs/miri.md b/tools/programs/miri.md new file mode 100644 index 0000000..4e70208 --- /dev/null +++ b/tools/programs/miri.md @@ -0,0 +1,22 @@ ++++ +date = 2025-07-10 +draft = false +title = 'Miri' +subtitle = 'Rust Verifier' +links = [ + # { title = "Homepage", url = "https://model-checking.github.io/kani/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/rust-lang/miri", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Rust Verifier'] +# developers = ['Microsoft Research', 'Inria'] +licenses = ['Apache-2.0', 'MIT'] +inputs = ['Rust'] +interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['Barbosa2022'] ++++ + + +Miri is an Undefined Behavior detection tool for Rust. \ No newline at end of file diff --git a/tools/programs/prusti.md b/tools/programs/prusti.md new file mode 100644 index 0000000..4fcfdd2 --- /dev/null +++ b/tools/programs/prusti.md @@ -0,0 +1,22 @@ ++++ +date = 2025-07-10 +draft = false +title = 'Prusti' +subtitle = 'Rust Verifier' +links = [ + { title = "Homepage", url = "https://www.pm.inf.ethz.ch/research/prusti.html", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/viperproject/prusti-dev", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Rust Verifier'] +# developers = ['Microsoft Research', 'Inria'] +licenses = ['Mozilla-2.0'] +inputs = ['Rust'] +interfaces = ['CLI'] +maintenance = ['Not Maintained'] +# techniques = ['CDCL'] +# publications = ['Barbosa2022'] ++++ + +{{}} +Prusti is a prototype verifier for Rust that makes it possible to formally prove absence of bugs and correctness of code contracts. \ No newline at end of file diff --git a/tools/programs/shuttle.md b/tools/programs/shuttle.md new file mode 100644 index 0000000..583155d --- /dev/null +++ b/tools/programs/shuttle.md @@ -0,0 +1,22 @@ ++++ +date = 2025-07-10 +draft = false +title = 'Loom' +subtitle = 'Rust Verifier' +links = [ + # { title = "Homepage", url = "https://www.pm.inf.ethz.ch/research/prusti.html", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/awslabs/shuttle", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Rust Verifier'] +developers = ['Amazon Web Services'] +licenses = ['MIT'] +inputs = ['Rust'] +interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['Barbosa2022'] ++++ + + +Shuttle is a library for testing concurrent Rust code. \ No newline at end of file diff --git a/tools/programs/verus.md b/tools/programs/verus.md new file mode 100644 index 0000000..05c9934 --- /dev/null +++ b/tools/programs/verus.md @@ -0,0 +1,22 @@ ++++ +date = 2025-07-10 +draft = false +title = 'Verus' +subtitle = 'Rust Verifier' +links = [ + # { title = "Homepage", url = "https://www.pm.inf.ethz.ch/research/prusti.html", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/verus-lang/verus", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Rust Verifier'] +# developers = ['Microsoft Research', 'Inria'] +licenses = ['MIT'] +inputs = ['Rust'] +interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['Barbosa2022'] ++++ + + +Verus is a tool for verifying the correctness of code written in Rust. \ No newline at end of file