diff --git a/docs/user-guide/install.md b/docs/user-guide/install.md
index 94c0df81..6c0aac3e 100644
--- a/docs/user-guide/install.md
+++ b/docs/user-guide/install.md
@@ -426,10 +426,21 @@ full path to the `solc` executables folder every time.
               source .profile
 ```
 
+```{index} single: install; vyper
+```
+
+Step 5 (optional, for Vyper users): Install the Vyper compiler (`vyper`)
+--------------------------------------------------------------------------------
+[Vyper](https://github.com/vyperlang/vyper) is an EVM compatible Pythonic smart contract language.
+Since the Certora Prover operates on the bytecode, it can be applied to any source-level language
+that compiles to EVM bytecode.
+We recommend to install Vyper either from PyPi (i.e., `pip install vyper`) or to get a 
+binary executable for the desired version.
+
 ```{index} single: VS code; extension
 ```
 
-Step 5 (for VS Code users): Install the Certora Verification Language LSP
+Step 6 (for VS Code users): Install the Certora Verification Language LSP
 -------------------------------------------------------------------------
 
 All users of the Certora Prover can access the tool using the command line 
diff --git a/spelling_wordlist.txt b/spelling_wordlist.txt
index 41ba3fb4..baacde84 100644
--- a/spelling_wordlist.txt
+++ b/spelling_wordlist.txt
@@ -15,6 +15,7 @@ Linux
 Mainnet
 OOM
 Prover
+Pythonic
 SMT
 Secureum
 Solana