diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md
index 3d101033efb3..15ce73d460c0 100644
--- a/doc/SUMMARY.md
+++ b/doc/SUMMARY.md
@@ -8,6 +8,7 @@
   - [Platform Developer](./getting-started/plat-dev.md)
     - [Network Configuration](./network.md)
   - [Verification](./getting-started/verification.md)
+    - [Model Checking](./islet-model-checking.md)
 - [Components](./components/index.md)
   - [CCA platform architecture](./components/cca_design.md)
   - [Realm Management Monitor](./components/rmm.md)
diff --git a/doc/getting-started/verification.md b/doc/getting-started/verification.md
index e8bece138082..330eb8455f99 100644
--- a/doc/getting-started/verification.md
+++ b/doc/getting-started/verification.md
@@ -25,3 +25,5 @@ rmi_granule_undelegate
 # Choose one among the list in `Available RMI targets` for the value of `RMI_TARGET`
 $ RMI_TARGET=rmi_granule_undelegate make verify
 ```
+
+For more about Islet's model-checking, please refer to [here](../islet-model-checking.md).