diff --git a/README.md b/README.md
index 5cbea16..607e0f6 100644
--- a/README.md
+++ b/README.md
@@ -104,6 +104,10 @@ Turns out, there is an entire subcategory on crates.io [Development tools::Testi
 ### Model Based Testing
 
 * [model](https://crates.io/crates/model)
+* [kani](https://crates.io/crates/kani-verifier)
+* [creusot](https://github.com/creusot-rs/creusot)
+* [prusti](https://github.com/viperproject/prusti-dev)
+* [aeneas](https://github.com/AeneasVerif/aeneas)
 
 ### Testing Webservices