diff --git a/.gitignore b/.gitignore
index 4e376dd35..8decb3fef 100644
--- a/.gitignore
+++ b/.gitignore
@@ -41,5 +41,5 @@ test-ledger
 *.txt
 *.log
 
-doc
-tmp.ps1
\ No newline at end of file
+#doc
+doc
\ No newline at end of file
diff --git a/README.md b/README.md
index b6f243dbe..11fc5e32b 100644
--- a/README.md
+++ b/README.md
@@ -64,6 +64,24 @@ cargo dv clean --targets aster_common
 
 You can also run `cargo dv clean` to clean all artifacts at once.
 
+#### Documentation
+
+We provide comprehensive API-level documentation that describes the verified APIs along with their auxiliary lemmas. To generate the documentation, run:
+
+```
+cargo dv doc --target ostd
+```
+
+The generated documentation can be found at `doc/index.html`.
+
+If you are interested in the precise Verus definitions, you can run:
+
+```
+cargo dv doc --target ostd --verus-conds
+```
+
+This will additionally include the Verus specifications and the pre- and post-conditions for each function.
+
 #### IDE Support
 
 For VSCode users, the [`verus-analyzer`](https://marketplace.visualstudio.com/items?itemName=verus-lang.verus-analyzer) extension is available in the Marketplace.
diff --git a/dv b/dv
index a4eef249a..5f92fde64 160000
--- a/dv
+++ b/dv
@@ -1 +1 @@
-Subproject commit a4eef249a8abcae57c42c470f98cb8a8a51af258
+Subproject commit 5f92fde64b1b6e374ed88c180ab204c225223f5f