diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md
index 784ec075d183..d534cf1f7f22 100644
--- a/docs/src/SUMMARY.md
+++ b/docs/src/SUMMARY.md
@@ -7,6 +7,8 @@
   - [Using Kani](./usage.md)
   - [Verification results](./verification-results.md)
 
+- [Crates Documentation](./crates/index.md)
+
 - [Tutorial](./kani-tutorial.md)
   - [First steps](./tutorial-first-steps.md)
   - [Failures that Kani can spot](./tutorial-kinds-of-failure.md)
@@ -18,6 +20,7 @@
   - [Experimental features](./reference/experimental/experimental-features.md)
     - [Coverage](./reference/experimental/coverage.md)
     - [Stubbing](./reference/experimental/stubbing.md)
+    - [Contracts](./reference/experimental/contracts.md)
     - [Concrete Playback](./reference/experimental/concrete-playback.md)
 - [Application](./application.md)
   - [Comparison with other tools](./tool-comparison.md)
@@ -45,8 +48,6 @@
     - [Unstable features](./rust-feature-support/unstable.md)
   - [Overrides](./overrides.md)
 
-- [Crates Documentation](./crates/index.md)
-
 ---
 
 - [FAQ](./faq.md)
diff --git a/docs/src/getting-started.md b/docs/src/getting-started.md
index 5de7ae431850..1acfd039ce97 100644
--- a/docs/src/getting-started.md
+++ b/docs/src/getting-started.md
@@ -15,6 +15,7 @@ Proof harnesses are similar to test harnesses, especially property-based test ha
 Kani is currently under active development.
 Releases are published [here](https://github.com/model-checking/kani/releases).
 Major changes to Kani are documented in the [RFC Book](https://model-checking.github.io/kani/rfc).
+We also publish updates on Kani use cases and features on our [blog](https://model-checking.github.io/kani-verifier-blog/).
 
 There is support for a fair amount of Rust language features, but not all (e.g., concurrency).
 Please see [Limitations](./limitations.md) for a detailed list of supported features.
diff --git a/docs/src/reference/experimental/contracts.md b/docs/src/reference/experimental/contracts.md
new file mode 100644
index 000000000000..fd4e8169bc34
--- /dev/null
+++ b/docs/src/reference/experimental/contracts.md
@@ -0,0 +1,66 @@
+# Contracts
+
+Consider the following example:
+
+```rust
+fn gcd(mut max: u8, mut min: u8) -> u8 {
+    if min > max {
+        std::mem::swap(&mut max, &mut min);
+    }
+
+    let rest = max % min;
+    if rest == 0 { min } else { gcd(min, rest) }
+}
+```
+Let's assume we want to verify some code that calls `gcd`.
+In the [worst case](https://en.wikipedia.org/wiki/Euclidean_algorithm#Worst-case), the number of steps (recursions) in `gcd` approaches 1.5 times the number of bits needed to represent the input numbers. 
+So, for two large 64-bit numbers, a single call to `gcd` can take almost 96 iterations.
+It would be very expensive for Kani to unroll each of these iterations and then perform symbolic execution.
+
+Instead, we can write *contracts* with guarantees about `gcd`'s behavior.
+Once Kani verifies that `gcd`'s contracts are correct, it can replace each invocation of `gcd` with its contracts, which reduces verification time for `gcd`'s callers.
+For example, perhaps we want to ensure that the returned `result` does indeed divide both `max` and `min`.
+In that case, we could write contracts like these:
+
+```rust
+#[kani::requires(min != 0 && max != 0)]
+#[kani::ensures(|result| *result != 0 && max % *result == 0 && min % *result == 0)]
+#[kani::recursion]
+fn gcd(mut max: u8, mut min: u8) -> u8 { ... }
+```
+
+Since `gcd` performs `max % min` (and perhaps swaps those values), passing zero as an argument could cause a division by zero.
+The `requires` contract tells Kani to restrict the range of nondeterministic inputs to nonzero ones so that we don't run into this error.
+The `ensures` contract is what actually checks that the result is a correct divisor for the inputs.
+(The `recursion` attribute is required when using contracts on recursive functions).
+
+Then, we would write a harness to *verify* those contracts, like so:
+
+```rust
+#[kani::proof_for_contract(gcd)]
+fn check_gcd() {
+    let max: u8 = kani::any();
+    let min: u8 = kani::any();
+    gcd(max, min);
+}
+```
+
+and verify it by running `kani -Z function-contracts`.
+
+Once Kani verifies the contracts, we can use Kani's [stubbing feature](stubbing.md) to replace all invocations to `gcd` with its contracts, for instance:
+
+```rust
+// Assume foo() invokes gcd().
+// By using stub_verified, we tell Kani to replace 
+// invocations of gcd() with its verified contracts.
+#[kani::proof]
+#[kani::stub_verified(gcd)]
+fn check_foo() {
+    let x: u8 = kani::any();
+    foo(x);
+}
+```
+By leveraging the stubbing feature, we can replace the (expensive) `gcd` call with a *verified abstraction* of its behavior, greatly reducing verification time for `foo`.
+
+There is far more to learn about contracts.
+We highly recommend reading our [blog post about contracts](https://model-checking.github.io/kani-verifier-blog/2024/01/29/function-contracts.html) (from which this `gcd` example is taken). We also recommend looking at the `contracts` module in our [documentation](../../crates/index.md).
diff --git a/docs/src/reference/experimental/coverage.md b/docs/src/reference/experimental/coverage.md
index fb73d5f7c05b..5e536b3992b6 100644
--- a/docs/src/reference/experimental/coverage.md
+++ b/docs/src/reference/experimental/coverage.md
@@ -1,4 +1,4 @@
-## Coverage
+# Coverage
 
 Recall our `estimate_size` example from [First steps](../../tutorial-first-steps.md),
 where we wrote a proof harness constraining the range of inputs to integers less than 4096: