diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
new file mode 100644
index 00000000..a4581783
--- /dev/null
+++ b/.github/CODEOWNERS
@@ -0,0 +1 @@
+/docs/gambit/gambit.md @chandrakananandi
diff --git a/docs/cvl/builtin.md b/docs/cvl/builtin.md
index f74e348e..098fe022 100644
--- a/docs/cvl/builtin.md
+++ b/docs/cvl/builtin.md
@@ -15,7 +15,7 @@ Built-in rules can be included in any spec file by writing `use builtin rule
 Syntax
 ------
 
-The syntax for rules is given by the following [EBNF grammar](syntax):
+The syntax for rules is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 built_in_rule ::= "use" "builtin" "rule" built_in_rule_name ";"
diff --git a/docs/cvl/defs.md b/docs/cvl/defs.md
index 33ea9c23..46f65478 100644
--- a/docs/cvl/defs.md
+++ b/docs/cvl/defs.md
@@ -1,14 +1,41 @@
 Definitions
 ===========
 
-```{todo}
-The documentation for this feature is incomplete.  See [the old documentation](/docs/confluence/anatomy/definitions)
+Definitions are declared at the top-level of a specification and are in scope inside every rule, function and inside other definitions.
+A definition binds parameters for use in an arbitrary expression on the right-hand side, which should evaluate to a value of the declared return type.
+
+Examples
+--------
+
+The following [example](https://github.com/Certora/Examples/blob/be09cf32c55e39f5f5aa8cba1431f9e519b52365/CVLByExample/import/certora/specs/base.spec#L22) 
+introduces a definition called `filterDef` which takes a method argument `m` and produces a `bool`:
+
+```cvl
+definition filterDef(method f) returns bool = f.selector == sig:someUInt().selector;
+```
+
+This definition can then be used as shorthand for `f.selector == sig:someUInt().selector`. 
+For example, in this spec it is [used in the filter](https://github.com/Certora/Examples/blob/be09cf32c55e39f5f5aa8cba1431f9e519b52365/CVLByExample/import/certora/specs/base.spec#L28)
+for `parametricRule`:
+
+```cvl
+rule parametricRuleInBase(method f) filtered { f -> filterDef(f)  }
+{
+...
+}
+```
+This is equivalent to
+
+```cvl
+rule parametricRuleInBase(method f) filtered { f -> f.selector == sig:someUInt().selector  } {
+...
+}
 ```
 
 Syntax
 ------
 
-The syntax for definitions is given by the following [EBNF grammar](syntax):
+The syntax for definitions is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 definition ::= [ "override" ]
diff --git a/docs/cvl/expr.md b/docs/cvl/expr.md
index 50bef11e..5a092b60 100644
--- a/docs/cvl/expr.md
+++ b/docs/cvl/expr.md
@@ -10,7 +10,7 @@ possible expressions in CVL and explains how they are evaluated.
 Syntax
 ------
 
-The syntax for CVL expressions is given by the following [EBNF grammar](syntax):
+The syntax for CVL expressions is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 expr ::= literal
@@ -96,10 +96,6 @@ denotes bitwise exclusive or and `**` denotes exponentiation, whereas in CVL,
 `^` denotes exponentiation and `xor` denotes exclusive or.
 ```
 
-```{todo}
-The `>>>` operator is currently undocumented.
-```
-
 % TODO: migrate this information here.
 See {ref}`cvl2-integer-types` for more information about the interaction between
 mathematical types and the meaning of mathematical operations.
@@ -344,7 +340,7 @@ while verifying the rule, and will provide a separate verification report for
 each checked method.  Rules that use this feature are referred to as
 {term}`parametric rule`s.
 
-
+(with-revert)=
 After the function name, but before the arguments, you can write an optional
 method tag, one of `@norevert`, `@withrevert`, or `@dontsummarize`.
  * `@norevert` indicates that examples where the method revert should not be
@@ -353,6 +349,9 @@ method tag, one of `@norevert`, `@withrevert`, or `@dontsummarize`.
    considered.  In this case, the method will set the `lastReverted` and
    `lastHasThrown` variables to `true` in case the called method reverts or
    throws an exception.
+
+   [`withrevert` example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/storage/certora/specs/storage.spec#L45C19-L45C19)
+
  * ```{todo}
    The `@dontsummarize` tag is currently undocumented.
    ```
@@ -483,7 +482,7 @@ and array/map dereference operations together. For example, if the current contr
 type definitions and state variables:
 
 ```solidity
-contract Example
+contract Example {
    struct Foo {
       mapping (address => uint[]) bar;
    }
diff --git a/docs/cvl/functions.md b/docs/cvl/functions.md
index 20415e3b..cb821763 100644
--- a/docs/cvl/functions.md
+++ b/docs/cvl/functions.md
@@ -1,12 +1,14 @@
+(functions-doc)=
 Functions
 =========
 
-A CVL function provides basic encapsulation for code reuse in a specification.
+CVL functions allow you to reuse parts of a specification, such as common assumptions, assertions, 
+or basic calculations. Additionally they can be used for basic calculations and  for [function summaries](https://github.com/Certora/Examples/blob/bf3255766c28068eea2d0513edb8daca7bcaa206/CVLByExample/function-summary/multi-contract/certora/specs/spec_with_summary.spec#L6).
 
 Syntax
 ------
 
-The syntax for CVL functions is given by the following [EBNF grammar](syntax):
+The syntax for CVL functions is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 function ::= [ "override" ]
@@ -19,7 +21,24 @@ function ::= [ "override" ]
 See {doc}`basics` for the `id` production, {doc}`types` for the `type` production,
 and {doc}`statements` for the `block` production.
 
-```{todo}
-This documentation is incomplete.  See [the old documentation](/docs/confluence/anatomy/functions).
-```
+Examples
+--------
+
+- Function with a return:
+    ```cvl
+    function abs_value_difference(uint256 x, uint256 y) returns uint256 {
+        if (x < y) {
+          return y - x;
+        } else {
+          return x - y;
+        }
+    }```
+  
+- [CVL function with no return](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/LiquidityPool/certora/specs/pool.spec#L24)
+
+- [Overriding a function from imported spec](https://github.com/Certora/Examples/blob/be09cf32c55e39f5f5aa8cba1431f9e519b52365/CVLByExample/import/certora/specs/sub.spec#L38)
+  
+Using CVL functions
+-------------------
+  CVL Function may be called from within a rule, or from within another CVL function.
 
diff --git a/docs/cvl/ghosts.md b/docs/cvl/ghosts.md
index 234a80da..ccc2dc48 100644
--- a/docs/cvl/ghosts.md
+++ b/docs/cvl/ghosts.md
@@ -1,23 +1,37 @@
-(ghost-functions)=
+(ghosts-doc)=
 Ghosts
 ======
 
 Ghosts are a way of defining additional variables for use during verification.
-These variables are often used to communicate information between
-[rules](rules.md) and [hooks](hooks.md).
+These variables are often used to 
+- communicate information between {ref}`rules-main` and {ref}`hooks`.
+- define deterministic [function summaries](https://github.com/Certora/Examples/blob/61ac29b1128c68aff7e8d1e77bc80bfcbd3528d6/CVLByExample/summary/with-env/WithEnvGhostSummary/WithEnv.spec#L10).
+
+Ghosts can be seen as an 'extension' to the state of the contracts under verification.
+This means that in case a call reverts, the ghost values will revert to their pre-state.
+Additionally, if an unresolved call is handled by a havoc, the ghost values will havoc as well.
+Ghosts are regarded as part of the state of the contracts, 
+and when calls are invoked with `at storageVar` statements (see {ref}`storage-type`),
+they are restored to their state as saved in `storageVar`.
+An exception to this rule are ghosts marked _persistent_.
+Persistent ghosts are **never** havoced, and **never** reverted.
+See {ref}`persistent-ghosts` below for more details and examples.
 
 ```{contents}
 ```
 
+The syntax for ghost and persistent ghost declarations is given by the following [EBNF grammar](ebnf-syntax):
+
 Syntax
 ------
 
-The syntax for ghost declarations is given by the following [EBNF grammar](syntax):
-
 ```
 ghost ::= "ghost" type id                             (";" | "{" axioms "}")
         | "ghost" id "(" cvl_types ")" "returns" type (";" | "{" axioms "}")
 
+persistent_ghost ::=  "persistent" "ghost" type id                             (";" | "{" axioms "}")
+                    | "persistent" "ghost" id "(" cvl_types ")" "returns" type (";" | "{" axioms "}")
+
 type ::= basic_type
        | "mapping" "(" cvl_type "=>" type ")"
 
@@ -30,12 +44,11 @@ the `expression` syntax.
 (ghost-variables)=
 Declaring ghost variables
 -------------------------
-
 Ghost variables must be declared at the top level of a specification file.
-A ghost declaration includes the keyword `ghost` followed by the type and name
+A ghost variable declaration includes the keyword `ghost` followed by the type and name
 of the ghost variable.
 
-The type of a ghost may be either a [CVL type](types.md) or a `mapping` type.
+The type of a ghost variable may be either a [CVL type](types.md) or a `mapping` type.
 Mapping types are similar to solidity mapping types.  They must have CVL types
 as keys, but may contain either CVL types or mapping types as values.
 
@@ -54,12 +67,35 @@ ghost (uint, uint) x;                              // tuples are not CVL types
 ghost mapping(mapping(uint => uint) => address) y; // mappings cannot be keys
 ```
 
+- [simple `ghost` variable example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/ERC20/certora/specs/ERC20.spec#L113)
+
+- This example uses an [`init_state` axiom](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/ERC20/certora/specs/ERC20.spec#L114)
+
+- [`ghost mapping` example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/structs/BankAccounts/certora/specs/Bank.spec#L117)
+
+(ghost-functions)=
+Ghost Functions
+---------------
+CVL also has support for "ghost functions".  These serve a different purpose from ghost variables, although they can be
+used in similar ways.
+
+Ghost functions must be declared at the top level of a specification file.
+A ghost function declaration includes the keyword `ghost` followed by the name and signature of the ghost function.
+Ghost functions should be used either:
+- when there are no updates to the ghost as the deterministic behavior and axioms are the only properties of the ghost
+- when updating the ghost - more than one entry is updated and then the havoc assuming statement is used.
+
+  
+  - [`ghost` function example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/QuantifierExamples/DoublyLinkedList/certora/spec/dll-linkedcorrectly.spec#L24)
+
+Restrictions on ghost definitions
+---------------------------------
+- A user-defined type, such as struct, array or interface is not allowed as the key or the output type of a `ghost mapping`.
 
 Using ghost variables
 ---------------------
-
 While verifying a rule or invariant, the Prover considers every possible
-initial value of a ghost variable (subject to its {ref}`axioms <ghost-axioms>`,
+initial value of a ghost variable (subject to its {ref}`ghost-axioms`,
 see below).
 
 Within CVL, you can read or write ghosts using the normal variable syntax.  For
@@ -107,25 +143,162 @@ rule update_changes_no_other(address user, address other) {
 Here the `updated` ghost is used to communicate information from the `userInfo`
 hook back to the `updated_changes_user` and `updated_changes_no_other` rules.
 
-Initial state axioms
---------------------
+(ghost-axioms)=
+Ghost axioms
+------------
+Ghost axioms are properties that the Prover assumes whenever it makes use of a ghost.
 
-```{todo}
-This documentation is incomplete.  See [the old documentation](/docs/confluence/anatomy/ghostfunctions)
-for information about initial state axioms.
+
+(global-axioms)=
+### Global axioms
+
+Sometimes we might want to constrain the behavior of a ghost in some particular way. 
+In CVL this is achieved by writing axioms. Axioms are simply CVL expressions that the tool will then assume are true 
+about the ghost. For example:
+
+```cvl
+ghost bar(uint256) returns uint256 {
+    axiom forall uint256 x. bar(x) > 10;
+}
 ```
 
-(ghost-axioms)=
-Ghost functions
----------------
+In any rule that uses bar, no application of bar could ever evaluate to a number less than or equal to 10. 
 
-CVL also has support for "ghost functions".  These serve a different purpose
-from ghost variables, although they can be used in similar ways.
+- [`axiom` example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/structs/BankAccounts/certora/specs/Bank.spec#L119)
 
-```{todo}
-This documentation is currently incomplete.  See [ghosts](/docs/confluence/anatomy/ghosts)
-and [ghost functions](/docs/confluence/anatomy/ghostfunctions) in the old documentation.
+### Initial state axioms
+
+When writing invariants, initial axioms are a way to express the “constructor state” of a ghost function. They are used 
+only when checking the base step of invariants {ref}`invariant-as-rule`. Before checking the initial state of an invariant, the Certora Prover adds a `require` for each `init_state` axiom. `init_state` axioms are not used in rules or the preservation check for invariants.
+
+```cvl
+ghost mathint sumBalances{
+    // assuming value zero at the initial state before constructor
+    init_state axiom sumBalances == 0;
+}
 ```
 
+- [initial state axiom example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/ConstantProductPool/certora/spec/ConstantProductPool.spec#L207)
+
+
+Restrictions on ghost axioms
+----------------------------
+- A ghost axiom cannot refer to Solidity or CVL functions or to other ghosts. It can refer to the ghost itself.
+- Since the signature of a ghost contains just parameter types without names, it cannot refer to its parameters. 
+ `forall` can be used in order to refer the storage referred to by the parameters. [Example](https://github.com/Certora/Examples/blob/61ac29b1128c68aff7e8d1e77bc80bfcbd3528d6/CVLByExample/summary/ghost-summary/ghost-mapping/certora/specs/WithGhostSummary.spec#L12).
+
 
 
+(persistent-ghosts)=
+Ghosts vs. persistent ghosts
+----------------------------
+
+In most cases, non-persistent ghosts are the natural choice for a specification 
+that requires extra tracking of information.
+
+We present two examples where persistent ghosts are useful.
+
+### Persistent ghosts that survive havocs
+In the first example, we want to track the occurrence of a potential reentrant call[^reentrancy]:
+
+[^reentrancy]: The example given here is very basic,  the examples repository contains [more complete examples of reentrancy checks](https://github.com/Certora/Examples/tree/master/CVLByExample/Reentrancy)
+
+```cvl
+persistent ghost bool reentrancy_happened {
+    init_state axiom !reentrancy_happened;
+}
+
+hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, 
+          uint retOffset, uint retLength) uint rc {
+    if (addr == currentContract) {
+        reentrancy_happened = reentrancy_happened 
+                                || executingContract == currentContract;
+    }
+}
+
+invariant no_reentrant_calls !reentrancy_happened;
+```
+
+To see why a persistent ghost must be used here for the variable `reentrancy_happened`, consider the following contract:
+```solidity
+contract NotReentrant {
+    function transfer1Token(IERC20 a) external {
+        require (address(a) != address(this));
+        a.transfer(msg.sender, 1);
+    }
+}
+```
+
+If we do not apply any linking or dispatching for the call done on the target `a`, the call to `transfer` would havoc.
+During a havoc operation, the Prover conservatively assumes that almost any possible behavior can occur.
+In particular, it must assume that during the execution of the `a.transfer` call, 
+non-persistent ghosts can be updated arbitrarily (e.g. by other contracts),
+and thus (assuming `reentrancy_happenedt` were not marked as persistent), 
+the Prover considers the case where `reentrancy_happened` is set to `true` due to the havoc.
+Thus, when the `CALL` hook executes immediately after, 
+it does so where the `reentrancy_happened` value is already `true`, 
+and thus the value after the hook will remain `true`.
+
+In the lower-level view of the tool, the sequence of events is as follows:
+1. A call to `a.transfer` which cannot be resolved and results in a {ref}`havoc <glossary>` operation.
+Non-persistent ghosts are havoced, in particular `reentrancy_happened` if it were not marked as such.
+2. A `CALL` hook executes, updating `reentrancy_happened` based on its havoced value, meaning it can turn to true.
+
+Therefore even if the addresses of `a` and `NotReentrant` are distinct, we could still falsely detect a reentrant call as `reentrancy_happened` was set to true due to non-determinism.
+The call trace would show `reentrancy_happened` as being determined to be true due to a havoc in the "Ghosts State" view under "Global State".
+
+### Persistent ghosts that survive reverts
+In this example, we use persistent ghosts to determine if a revert happened with user-provided data or not.
+This can help distinguishing between compiler-generated reverts and user-specified reverts (but only in [Solidity versions prior to 0.8.x](https://soliditylang.org/blog/2020/10/28/solidity-0.8.x-preview/)).
+The idea is to set a ghost to true if a `REVERT` opcode is encountered with a positive buffer size. As in early Solidity versions the panic errors would compile to reverts with empty buffers, as well as user-provided `require`s with no message specified. 
+
+```cvl
+persistent ghost bool saw_user_defined_revert_msg;
+
+hook REVERT(uint offset, uint size) {
+    if (size > 0) {
+        saw_user_defined_revert_msg = true;
+    }
+}
+
+rule mark_methods_that_have_user_defined_reverts(method f, env e, calldataarg args) {
+    require !saw_user_defined_revert_msg;
+
+    f@withrevert(e, args);
+
+    satisfy saw_user_defined_revert_msg;
+}
+```
+
+To see why a regular ghost cannot be used to implement this rule, let's consider the following trivial contract:
+```solidity
+contract Reverting {
+	function noUserDefinedRevertFlows(uint a, uint b) external {
+		uint c = a/b; // will see a potential division-by-zero revert
+		uint[] memory arr = new uint[](1);
+		uint d = arr[a+b]; // will see a potential out-of-bounds access revert;
+	}
+
+	function userDefinedRequireMsg(uint a) external {
+		require(a != 0, "a != 0");
+	}
+
+	function emptyRequire(uint a) external {
+		require(a != 0);
+	}
+}
+```
+
+It is expected for the method `userDefinedRequireMsg` to satisfy the rule, 
+and it should be the only method to satisfy it.
+Assuming `saw_user_defined_revert_msg` was defined as a regular, non-persistent ghost, 
+the rule would not be satisfied for `userDefinedRequireMsg`: in case the input argument `a` is equal to 0,
+the contract reverts, and the value of `saw_user_defined_revert_msg` 
+is reset to its value before the call, which must be `false`
+(because the rule required it before the call).
+In this case, after the call `saw_user_defined_revert_msg` cannot be set to true and thus the `satisfy` fails.
+Applying the same reasoning, it is clear that the same behavior happens 
+for reverting behaviors of `noUserDefinedRevertFlows` and `emptyRequire`,
+which do not have user-defined revert messages. 
+This means that if `saw_user_defined_revert_msg` is not marked persistent, 
+the rule cannot distinguishing between methods that may revert with user-defined messages and methods that may not.
\ No newline at end of file
diff --git a/docs/cvl/hooks.md b/docs/cvl/hooks.md
index 84d53303..8c24eccc 100644
--- a/docs/cvl/hooks.md
+++ b/docs/cvl/hooks.md
@@ -17,7 +17,7 @@ for additional information.  See also {doc}`ghosts` and {doc}`opcodes`.
 Syntax
 ------
 
-The syntax for hooks is given by the following [EBNF grammar](syntax):
+The syntax for hooks is given by the following EBNF grammar:
 
 ```
 hook ::= store_hook | load_hook | opcode_hook
@@ -94,3 +94,9 @@ slot_pattern ::= slot_pattern_nested:sp {: RESULT = sp; :}
              ;
 
 ```
+
+Examples
+--------
+- [store hook example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/ERC20/certora/specs/ERC20.spec#L117)
+- [load hook example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/structs/BankAccounts/certora/specs/Bank.spec#L141)
+
diff --git a/docs/cvl/imports.md b/docs/cvl/imports.md
index aa20c6bf..aa22c1b3 100644
--- a/docs/cvl/imports.md
+++ b/docs/cvl/imports.md
@@ -5,16 +5,24 @@ Import and Use Statements
 Contents of additional spec files can be imported using the `import` command.
 Some parts of the imported spec files are implicitly included in the importing
 spec file, while others such as rules and invariants must be explicitly
-`use`d.
-
-```{todo}
-This feature is currently undocumented.
-```
+`use`d. Functions, definitions, filters, and preserved blocks of the imported spec can be overridden by the importing 
+spec. If a spec defines a function and uses it (e.g. in a rule or function), and another spec imports it and overrides 
+it, uses in the imported spec use the new version.
+
+Examples
+--------
+- [Example for `import`](https://github.com/Certora/Examples/blob/be09cf32c55e39f5f5aa8cba1431f9e519b52365/CVLByExample/import/certora/specs/sub.spec#L1)
+- [`use rule`](https://github.com/Certora/Examples/blob/61ac29b1128c68aff7e8d1e77bc80bfcbd3528d6/CVLByExample/import/certora/specs/sub.spec#L24)
+- [`use rule` with filters](https://github.com/Certora/Examples/blob/be09cf32c55e39f5f5aa8cba1431f9e519b52365/CVLByExample/import/certora/specs/sub.spec#L3)
+- [overriding imported filters](https://github.com/Certora/Examples/blob/be09cf32c55e39f5f5aa8cba1431f9e519b52365/CVLByExample/import/certora/specs/sub.spec#L3)
+- [`use invariant`](https://github.com/Certora/Examples/blob/be09cf32c55e39f5f5aa8cba1431f9e519b52365/CVLByExample/import/certora/specs/sub.spec#L8)
+    - [overriding imported `preserved`](https://github.com/Certora/Examples/blob/be09cf32c55e39f5f5aa8cba1431f9e519b52365/CVLByExample/import/certora/specs/sub.spec#L10)
+    - [adding a `preserved` block](https://github.com/Certora/Examples/blob/be09cf32c55e39f5f5aa8cba1431f9e519b52365/CVLByExample/import/certora/specs/sub.spec#L14)
 
 Syntax
 ------
 
-The syntax for `import` and `use` statements is given by the following [EBNF grammar](syntax):
+The syntax for `import` and `use` statements is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 import ::= "import" string
@@ -26,6 +34,6 @@ use ::= "use" "rule" id
 
 ```
 
-See {doc}`basics` for the `string` and `id` productions, {doc}`expr` for the
-`expression` production, and {doc}`invariants` for the `preserved_block` production.
+See {doc}`basics` for the `string` and `id` productions, {doc}`expr` for the `expression` production, and 
+{doc}`invariants` for the `preserved_block` production.
 
diff --git a/docs/cvl/invariants.md b/docs/cvl/invariants.md
index a63d74f9..944627bf 100644
--- a/docs/cvl/invariants.md
+++ b/docs/cvl/invariants.md
@@ -15,6 +15,7 @@ also unsound if some of the methods are filtered out using the
 details.
 ```
 
+
 ```{contents}
 ```
 
@@ -22,7 +23,7 @@ details.
 Syntax
 ------
 
-The syntax for invariants is given by the following [EBNF grammar](syntax):
+The syntax for invariants is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 invariant ::= "invariant" id
@@ -111,6 +112,18 @@ Nevertheless, the invariant will pass.  The reason is that before a call to
 `add` pushes a nonzero integer into `a[i]`, the length of `a` was `i-1`, so the
 call to `get(i)` will revert.  Therefore, the Prover would discard the
 counterexample instead of reporting it.
+As above, an invariant stating that `supply() == token.totalSupply()` would be
+verified, but a method on `token` might change the total supply without updating
+the `SupplyTracker` contract.  Since the Prover only checks the main contract's
+methods for preservation, it will not report that the invariant can be
+falsified.
+
+For this reason, invariants that depend on the environment or on the state of
+external contracts are a potential source of {term}`unsoundness <unsound>`, and should be
+used with care.
+
+There is an additional source of unsoundness that occurs if the invariant
+expression reverts in the before state but not in the after state.
 
 (preserved)=
 Preserved blocks
diff --git a/docs/cvl/methods.md b/docs/cvl/methods.md
index 0e576701..6b59658d 100644
--- a/docs/cvl/methods.md
+++ b/docs/cvl/methods.md
@@ -38,7 +38,7 @@ Syntax
 The syntax for methods block entries {doc}`changed in CVL 2 <cvl2/changes>`.
 ```
 
-The syntax for the `methods` block is given by the following [EBNF grammar](syntax):
+The syntax for the `methods` block is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 methods          ::= "methods" "{" { method_spec } "}"
@@ -520,14 +520,14 @@ The behavior of the `AUTO` summary depends on the type of call[^opcodes]:
  * Calls to non-library `view` and `pure` methods use the `NONDET` approximation:
    they keep all state unchanged.
 
- * Normal calls and constructors use the `HAVOC_ECF` approximation: they are
-   assumed to change the state of external contracts arbitrarily but to leave
-   the caller's state unchanged.
-
  * Calls to library methods and `delegatecall`s are assumed to change
    the caller's storage in an arbitrary way, but are assumed to leave ETH
    balances and the storage of other contracts unchanged.
 
+ * All other calls and constructors use the `HAVOC_ECF` approximation: they are
+   assumed to change the state of external contracts arbitrarily but to leave
+   the caller's state unchanged.
+
 [^opcodes]: The behavior of `AUTO` summaries is actually determined by the EVM
   opcode used to make the call: calls made using the `STATICCALL` opcode use
   the `NONDET` summary, calls using `CALL` or `CREATE` opcode use the `HAVOC_ECF`
diff --git a/docs/cvl/overview.md b/docs/cvl/overview.md
index 94b2112b..57ff2dfc 100644
--- a/docs/cvl/overview.md
+++ b/docs/cvl/overview.md
@@ -19,7 +19,7 @@ A spec may contain any of the following:
  - **[Methods blocks](methods):** `methods` blocks contain information on how methods
    should be summarized by the Prover during verification.
 
- - **[Rules](rules):** A rule describes the expected behavior of the methods of a
+ - **[Rules](rules-main):** A rule describes the expected behavior of the methods of a
    contract.
 
  - **{ref}`invariants`:** Invariants describe facts about the state of a contract that
@@ -40,7 +40,7 @@ A spec may contain any of the following:
 The remainder of this chapter describes the syntax and semantics of a
 specification file in detail.
 
-(syntax)=
+(ebnf-syntax)=
 Syntactic Conventions
 ---------------------
 
diff --git a/docs/cvl/rules.md b/docs/cvl/rules.md
index b2369bec..08647e49 100644
--- a/docs/cvl/rules.md
+++ b/docs/cvl/rules.md
@@ -1,3 +1,4 @@
+(rules-main)=
 Rules
 =====
 
@@ -18,7 +19,7 @@ these features.
 Syntax
 ------
 
-The syntax for rules is given by the following [EBNF grammar](syntax):
+The syntax for rules is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 rule ::= [ "rule" ]
@@ -61,6 +62,26 @@ of the `assert` statements evaluate to true.  If all of the `assert` statements
 evaluate to true on every example, the rule passes.  Otherwise, the Prover will
 output a specific counterexample that causes the assertions to fail.
 
+- [simple rule example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/LiquidityPool/certora/specs/pool.spec#L54)
+
+    ```cvl
+    /// `deposit` must increase the pool's underlying asset balance
+    rule integrityOfDeposit {
+    
+        mathint balance_before = underlyingBalance();
+    
+    
+        env e; uint256 amount;
+        safeAssumptions(_, e);
+    
+        deposit(e, amount);
+    
+        mathint balance_after = underlyingBalance();
+    
+        assert balance_after == balance_before + amount,
+            "deposit must increase the underlying balance of the pool";
+    }
+    ```
 ```{caution}
 `assert` statements in contract code are handled differently from `assert`
 statements in rules.
@@ -68,7 +89,7 @@ statements in rules.
 An `assert` statement in Solidity causes the transaction to revert, in the same
 way that a `require` statement in Solidity would.  By default, examples that
 cause contract functions to revert are {ref}`ignored by the prover
-<withrevert>`, and these examples will *not* be reported as counterexamples.
+<with-revert>`, and these examples will *not* be reported as counterexamples.
 
 The {ref}`--multi_assert_check` option causes assertions in the contract code
 to be reported as counterexamples.
@@ -116,6 +137,16 @@ rule r {
 
 It is an error to call the same `method` variable on two different contracts.
 
+```cvl
+  rule sanity(method f) {
+    env e;
+    calldataarg args;
+    f(e,args);
+    assert false;
+    }
+  ```
+- [parameteric rule example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/structs/BankAccounts/certora/specs/Bank.spec#L94)
+  
 
 (rule-filters)=
 Filters
@@ -141,6 +172,9 @@ For example, the following rule has two filters.  The rule will only be
 verified with `f` instantiated by a view method, and `g` instantiated by a
 method other than `exampleMethod(uint,uint)` or `otherExample(address)`:
 
+
+- [filters example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/Reentrancy/certora/spec/Reentrancy.spec#L29C9-L29C9)
+
 ```cvl
 rule r(method f, method g) filtered {
     f -> f.isView,
diff --git a/docs/cvl/sorts.md b/docs/cvl/sorts.md
index 88cbfed2..dbbcb151 100644
--- a/docs/cvl/sorts.md
+++ b/docs/cvl/sorts.md
@@ -1,14 +1,7 @@
 Uninterpreted Sorts
 ===================
 
-```{todo}
-This documentation is incomplete.  See [the old documentation](/docs/confluence/anatomy/ghostfunctions).
-```
-
-Syntax
-------
-
-The syntax for `sort` declarations is given by the following [EBNF grammar](syntax):
+The syntax for `sort` declarations is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 sort ::= "sort" id ";"
@@ -16,3 +9,52 @@ sort ::= "sort" id ";"
 
 See {ref}`identifiers` for the `id` production.
 
+
+There are then 3 things we can do with these sorts:
+
+1.  Declare variables of said sort: `Node x`.
+    
+2.  Test equality between two elements of this sort: `Node x; Node y; assert x == y;`;
+    
+3.  Use these sorts in the signatures of `ghost` function `ghost myGhost(uint256 x, Foo f) returns Foo`.
+
+4. Use these sorts in ghosts: `ghost mapping(uint256 => Node) toNode;`
+
+Putting these pieces together we might write the following useless, but demonstrative example:
+
+```cvl
+sort Foo;
+ghost bar(Foo, Foo) returns Foo;
+
+rule myRule {
+  Foo x;
+  Foo y;
+  Foo z = bar(x, y);
+  assert x == y && y == z;
+}
+```
+
+The following is an example for using `sort` using ghosts.
+
+``` cvl
+ghost mapping(uint256 => Node) toNode;
+ghost mapping(Node => mapping(Node => bool)) reach {
+  axiom forall Node X. reach[X][X];
+  axiom forall Node X. forall Node Y.
+      reach[X][Y] && reach[Y][X] => X == Y;
+  axiom forall Node X. forall Node Y. forall Node Z.
+      reach[X][Y] && reach[Y][Z] => reach[X][Z];
+  axiom forall Node X. forall Node Y. forall Node Z.
+      reach[X][Y] && reach[X][Z] => (reach[Y][Z] || reach[Z][Y]);
+}
+
+definition isSucc(Node a, Node b) returns bool =
+    reach[a][b] && a != b &&
+        (forall Node X. reach[a][X] && reach[X][b] => (a == X || b == X));
+        
+rule checkGetSucc {
+  uint256 key;
+  uint256 afterKey = getSucc(key);
+  assert reach[toNode[key]][toNode[afterKey]];
+}
+```
diff --git a/docs/cvl/statements.md b/docs/cvl/statements.md
index 14c342c9..ae061278 100644
--- a/docs/cvl/statements.md
+++ b/docs/cvl/statements.md
@@ -15,7 +15,7 @@ CVL commands.
 Syntax
 ------
 
-The syntax for statements in CVL is given by the following [EBNF grammar](syntax):
+The syntax for statements in CVL is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 block ::= statement { statement }
@@ -93,6 +93,32 @@ about the counterexamples to the message.
 Unlike Solidity's `assert` and `require`, the CVL syntax for `assert` and
 `require` does not require parentheses around the expression and message.
 ```
+### Examples
+
+```cvl
+rule withdraw_succeeds {
+    env e; // env represents the bytecode environment passed on every call
+    // invoke function withdraw and assume that it does not revert
+    bool success = withdraw(e);  // e is passed as an additional argument
+    assert success, "withdraw must succeed"; // verify that withdraw succeeded
+}
+
+rule totalFundsAfterDeposit(uint256 amount) {
+	 env e; 
+	
+	 deposit(e, amount);
+	
+	 uint256 userFundsAfter = getFunds(e, e.msg.sender);
+	 uint256 totalAfter = getTotalFunds(e);
+	
+	 // Verify that the total funds of the system is at least the current funds of the msg.sender.
+	 assert totalAfter >= userFundsAfter;
+}
+
+```
+- [`assert` example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/ConstantProductPool/certora/spec/ConstantProductPool.spec#L75)
+
+- [`require` example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/ConstantProductPool/certora/spec/ConstantProductPool.spec#L44)
 
 (satisfy)=
 `satisfy` statements
@@ -127,35 +153,21 @@ some arbitrary state.  It is not possible to check that every possible starting
 state has an execution that satisfies the condition.
 ```
 
+- [`satisfy` example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/ConstantProductPool/certora/spec/ConstantProductPool.spec#L243)
+
 (requireInvariant)=
 `requireInvariant` statements
 -----------------------------
 
-```{todo}
-This feature is currently undocumented.
-```
+`requireInvariant` is shorthand for `require` of the expression of the invariant where the invariant parameters have to be substituted with the values/ variables for which the invariant should hold.
+
+- [`requireInvariant` example](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/ConstantProductPool/certora/spec/ConstantProductPool.spec#L178)
 
 ```{note}
 `requireInvariant` is always safe for invariants that have been proved, even in
 `preserved` blocks; see {ref}`invariant-induction` for a detailed explanation.
 ```
 
-(control-flow)=
-Solidity-like statements
-------------------------
-
-```{todo}
-This feature is currently undocumented.
-```
-
-(withrevert)=
-Function calls
---------------
-
-```{todo}
-This feature is currently undocumented.  See {ref}`call-expr` for partial information.
-```
-
 (havoc-stmt)=
 `havoc` statements
 ------------------
@@ -164,7 +176,6 @@ This feature is currently undocumented.  See {ref}`call-expr` for partial inform
 This section is currently incomplete.  See
 [ghosts](/docs/confluence/anatomy/ghosts) and {ref}`two-state-old`
 for the old documentation.
-```
 
 ```{todo}
 Be sure to document `@old` and `@new` (two-state contexts).  They are not documented in {doc}`expr`
@@ -172,3 +183,12 @@ because I think `havoc ... assuming ...` is the only place that they are
 available.
 ```
 
+(control-flow)=
+Solidity-like statements
+------------------------
+
+```{todo}
+This feature is currently undocumented.
+```
+
+
diff --git a/docs/cvl/types.md b/docs/cvl/types.md
index 740bc8ce..6516a45c 100644
--- a/docs/cvl/types.md
+++ b/docs/cvl/types.md
@@ -19,7 +19,7 @@ The additional CVL types are:
 Syntax
 ------
 
-The syntax for types in CVL is given by the following [EBNF grammar](syntax):
+The syntax for types in CVL is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 basic_type ::= "int*" | "uint*" | "address" | "bool"
diff --git a/docs/cvl/using.md b/docs/cvl/using.md
index a8be99ac..438cff0e 100644
--- a/docs/cvl/using.md
+++ b/docs/cvl/using.md
@@ -5,19 +5,19 @@ Using Statements
 The `using` statement introduces a variable that can be used to call methods on
 contracts other than the main contract being verified.
 
-```{todo}
-The documentation for this feature is incomplete.  See
-[the old documentation](/docs/confluence/advanced/multicontract)
-for more information.
-```
-
 ```{contents}
+
 ```
 
+Examples
+--------
+- [Accessing  additional contracts from CVL]{ref}`using-example`
+- [An example for `using`](https://github.com/Certora/Examples/blob/14668d39a6ddc67af349bc5b82f73db73349ef18/CVLByExample/LiquidityPool/certora/specs/pool_link.spec#L14)
+
 Syntax
 ------
 
-The syntax for `using` statements is given by the following [EBNF grammar](syntax):
+The syntax for `using` statements is given by the following [EBNF grammar](ebnf-syntax):
 
 ```
 using ::= "using" id "as" id
@@ -25,3 +25,5 @@ using ::= "using" id "as" id
 
 See {ref}`identifiers` for the `id` production.
 
+
+
diff --git a/docs/gambit/gambit.md b/docs/gambit/gambit.md
index ae30dc56..3e7044b3 100644
--- a/docs/gambit/gambit.md
+++ b/docs/gambit/gambit.md
@@ -101,7 +101,10 @@ file to mutate.
 
 ```bash
 gambit mutate -f benchmarks/BinaryOpMutation/BinaryOpMutation.sol
+```
 
+This will generate:
+```
 Generated 34 mutants in 0.69 seconds
 ```
 
@@ -119,7 +122,10 @@ provides a way to randomly downsample the number of mutants with the
 
 ```bash
 gambit mutate -f benchmarks/BinaryOpMutation/BinaryOpMutation.sol -n 3
+```
 
+which will generate:
+```
 Generated 3 mutants in 0.15 seconds
 ```
 
@@ -132,7 +138,10 @@ Gambit outputs all of its results in `gambit_out`:
 
 ```bash
 tree -L 2 gambit_out
+```
 
+This produces:
+```
 gambit_out
 ├── gambit_results.json
 ├── input_json
@@ -237,6 +246,7 @@ Here are some examples of using the `--sourceroot` option.
    ```
 
    This should output the following:
+
    ```
    Generated 1 mutants in 0.13 seconds
    1,BinaryOpMutation,benchmarks/BinaryOpMutation/BinaryOpMutation.sol,23:10, % ,*
@@ -274,6 +284,7 @@ Here are some examples of using the `--sourceroot` option.
    ```bash
    gambit mutate -f benchmarks/BinaryOpMutation/BinaryOpMutation.sol -n 1 --sourceroot scripts
    ```
+
    This will try to find the specified file inside of `scripts`, and since it
    doesn't exist Gambit reports the error:
 
@@ -384,7 +395,11 @@ to the `benchmarks/` directory the `"filename"` would need to be updated to
 ```bash
 gambit mutate -f benchmarks/BinaryOpMutation/BinaryOpMutation.sol -n 5
 tree gambit_out -L 2
+```
 
+which produces:
+
+```
 Generated 5 mutants in 0.15 seconds
 
 gambit_out
diff --git a/docs/gambit/mutation-verifier.md b/docs/gambit/mutation-verifier.md
index 00c5b8b6..37ceabec 100644
--- a/docs/gambit/mutation-verifier.md
+++ b/docs/gambit/mutation-verifier.md
@@ -69,10 +69,10 @@ In `prover.conf`:
 In `mutation.conf`:
 
 ```json
-{ "gambit": {
+{ "gambit": [{
     "filename" : "C.sol",
-    "num-mutants": 5
-  }
+    "num_mutants": 5
+  }]
 }
 ```
 
@@ -80,10 +80,10 @@ In `mutation.conf`:
 You can add manual mutations to `mutation.conf` like so:
 
 ```json
-{ "gambit": {
+{ "gambit": [{
     "filename" : "C.sol",
-    "num-mutants": 5
-  },
+    "num_mutants": 5
+  }],
   "manual_mutants": {
      "C.sol": "path/to/dir/with/manual_mutants/for/C"
   }
diff --git a/docs/prover/approx/hashing.md b/docs/prover/approx/hashing.md
index 82b8a250..534fe2e8 100644
--- a/docs/prover/approx/hashing.md
+++ b/docs/prover/approx/hashing.md
@@ -1,6 +1,6 @@
 (hashing)=
-Modeling of Hashing in the Prover
-==========================
+Modeling of Hashing in the Certora Prover
+=========================================
 
 In this document we present how the Keccak hash function is modeled in the
 Certora Prover and how that impacts smart contract verification.
@@ -12,7 +12,7 @@ implicit way.
 Most prominently, all unbounded data structures in storage (arrays, mappings) 
 receive their storage addresses as values of the Keccak function.
 It is also possible to call the Keccak hash function explicitly, both through
-a solidity builtin function and through inline assembly.
+a solidity built in function and through inline assembly.
 
 The Certora Prover does not operate with an actual implementation of the Keccak
 hash function, since this would make most verification intractable and provide 
@@ -22,7 +22,7 @@ function that are crucial for the function of the smart contracts under
 verification while abstracting away from implementation details of the actual
 hash function.
 
-## Modeling the Keccak Function (bounded case)
+## Modeling the Keccak function (bounded case)
 
 The Certora Prover models the Keccak hash function as an arbitrary function that
 is _injective with large gaps_.
@@ -33,16 +33,19 @@ inputs `x` and `y`
   - the gap between `hash(x)` and `hash(y)` is large enough that every additive 
     term `hash(x) + i` that occurs in the program is also distinct from `hash(y)`.
 
-Furthermore, the initial storage slots are reserved, i.e., we make sure that no
-hash value ends up colliding with slots 0 to 10000.
+Furthermore, the initial storage slots and large constants that appear in the code 
+are reserved. I.e., we make sure that no hash value ends up colliding with slots 
+0 to 10000 nor with any constant that is explicitly given in the source code. (The
+latter constraint is necessary to avoid collisions with hashes that the solidity 
+compiler has precompiled.)
 
 These constraints are enough for the Solidity storage model to work as expected.
-However this modeling allows Certora Prover to pick hash functions that show 
-different behavior from the actual Keccak function, for instance it is unlikely 
-that the individual numeric values or their ordering matches that of the Keccak
-function. We present some examples in the following subsection.
-We have not observed a practical use case yet where the numeric values of the 
-hash function play a role, thus we chose this modeling for tractability reasons.
+However, this modeling allows the Certora Prover to pick hash functions that
+show different behavior from the actual Keccak function. For instance, it is
+unlikely that the individual numeric values or their ordering matches that of
+the Keccak function. We present some examples in the following subsection. We
+have not observed a practical use case yet where the numeric values of the hash
+function play a role, thus we chose this modeling for tractability reasons.
 
 See the later subsection {ref}`Background: The Solidity Storage Model` for 
 details on why this property is an adequate model for maintaining integrity
@@ -50,16 +53,16 @@ of solidity's storage operations.
 
 ### Examples (Imprecision of Modeling)
 
-We illustrate the consequences of our modeling on a few examples.
+We illustrate the implications of our modeling decisions using a few examples.
 
 ### Modeling does not account for individual values of the Keccak function
 
 The Keccak256-hash of the string `hello` is 
 `0x1c8aff950685c2ed4bc3174f3472287b56d9517b9c948127319a09a7a36deac8`.
-However, due to our modeling, Certora Prover cannot prove that fact. The rule 
-`hashOf17Eq` will show as "violated" since Certora Prover can pick a function 
+However, due to our modeling, the Certora Prover cannot prove that fact. the
+rule `hashOf17Eq` will show as "violated" since the Prover can pick a function 
 for `keccak256` that assigns `hello` differently.
-For the same reason Certora Prover also does not disprove that the hash of `17`
+For the same reason the Prover also does not disprove that the hash of `17`
 is `0x1c8aff950685c2ed4bc3174f3472287b56d9517b9c948127319a09a7a36deac8`, since 
 we allow it to choose `keccak256` appropriately.
 
@@ -83,10 +86,10 @@ contract C {
 }
 ```
 
-#### Modeling Does Not Account for Ordering
+### Modeling does not account for ordering
 
 Whichever distinct values we chose for `x` and `y` in the example below, on the
-real Keccak function one rule would be violated and one rule would not. In the 
+real Keccak function, one rule would be violated and one rule would not. In the 
 modeling of the Certora Prover, both rules are violated, since the Prover is 
 allowed to "invent" a hash function for each rule and will choose one that 
 violates the property whenever there is such a function (as long as that 
@@ -117,8 +120,80 @@ contract C {
 }
 ```
 
+### Constants in code vs hashes
 
-## Hashing of Unbounded Data
+A special case in Certora Prover's modeling of hashing is the treatment of 
+constants that appear in the code: The Prover implicitly assumes that the hash 
+function never outputs one of these constants on any of the concrete inputs it 
+gets in that program.
+
+For an example, consider this rule and spec:
+
+```
+// CVL:
+methods {
+    function readAtSlotAddress() external returns (uint) envfree;
+    function updateMap(uint k, uint v) external envfree;
+}
+
+rule foo {
+	uint v1 = readAtSlotAddress();
+
+	uint preImage;
+	uint x; 
+
+	updateMap(preImage, x);
+
+	uint v2 = readAtSlotAddress();
+
+	assert(v1 == v2);
+}
+
+// solidity
+contract C {
+	uint constant slotAddress = 1000000;
+
+	mapping(uint => uint) map;
+
+	function updateMap(uint k, uint v) public {
+		map[k] = v;
+	}
+
+	function readAtSlotAddress() public returns (uint r) {
+		assembly {
+			r := sload(slotAddress)
+		}
+	}
+}
+```
+
+The function `readAtSlotAddress` reads from storage at the slot with the number
+1000000. The function `updateMap` updates a mapping; this means it updates
+storage at a hash computed from its identifier (here 1, since it is the second
+field in the contract) and the key `k`. Now, if `k` is chosen such that
+`keccak(1, k)` equals 1000000, the map update would overwrite that storage
+slot, and thus the assertion in the rule `foo` would be violated.
+
+However, the Certora Prover will return "not violated" for this assertion, since
+it assumes that no hash ever collides with the constant 1000000, which occurs in
+the program.
+
+On the other hand, if we change the contract to leave `slotAddress`
+uninitialized, then Certora Prover will return a violation, since then it can
+choose the values such that `keccak(2, preImage)` == `slotAddress`.
+
+Also see this [example run](https://prover.certora.com/output/91772/e02fc5c0f57c4404b6fe28f237ecab07?anonymousKey=9e9e40a985a82d55446b0cdc2c75a7540ca696bc) 
+for a further illustration of both cases.
+
+```{note}
+The reader may wonder at first whether this means that the Certora Prover computes 
+the inverse value of the Keccak function for some image value (which would be a 
+challenging task in and of itself). This is not the case, in practice the Prover 
+makes up any arbitrary function that fulfills the previously described axioms and 
+also maps that single input to an output accordingly.
+```
+
+## Hashing of unbounded data
 
 In the discussion so far we only considered hashes of data whose length is 
 already known before program execution (e.g. a `uint` variable always has 256 
@@ -162,11 +237,11 @@ Then, the first hash operation, triggered by the mapping access `m[b1]`, behaves
 like the hash of a bounded data chunk. The `--optimstic_hashing` flag has no 
 impact on this hash operation.
 
-Behavior of the second hash operation, triggered by the mapping access `m[b2]`,
+The behavior of the second hash operation, triggered by the mapping access `m[b2]`,
 depends on whether `--optimistic_hashing` is set. 
 
  - If the `--optimistic_hashing` flag is not set, the violation of an internal 
-assertion will be reported by the Prover, stating that an chunk of data is being
+assertion will be reported by the Prover, stating that a chunk of data is being
 hashed that may exceed the given bound of 224.
 The reported message will look like this:
 ```text
@@ -181,14 +256,14 @@ assumption (equivalent to a `require` statement) on `b2` stating that its length
 exceed 224 bytes.
 
 The third operation, triggered by the mapping access `m[b3]` behaves like the second, 
-since also no length constraint on `b3` is made by the program. 
+since no length constraint on `b3` is made by the program. 
 However, we can see the impact of the `--optimistic_hashing` flag on the `assert` 
 command that follows the hash operation: 
 When the flag is set, the assertion will be shown as not violated
 even though nothing in the program itself prevents `b3` from being longer than 
 300 bytes. This is an example of unsoundness coming from "optimistic" assumptions.
 (When `--optimistic_hashing` is not set, then we get a violation from any or all
-assertions, depending on the configuration of Certora Prover.)
+assertions, depending on the configuration of the Certora Prover.)
 
 
 ### Examples for Unbounded Hashing
@@ -223,7 +298,7 @@ and unbounded.
 Further use cases include direct calls of the Keccak function, either directly
 on Solidity or inside an inline assembly snippet.
 
-Note that Certora Prover's static analysis is aware of the ABI encoder. Thus,
+Note that the Certora Prover's static analysis is aware of the ABI encoder. Thus,
 in many cases, it can figure out that when `x, y, z` are scalars that 
 `keccak256(abi.encode(x, y, z))` is actually a bounded hash of the form 
 `hash(x, y, z)` as opposed to an unbounded hash of the `bytes` array that is the
@@ -271,7 +346,7 @@ The comments of the function `foo` illustrate how storage is laid out by
 Solidity.
 The occurrences of `sstore(x, y)` in the line comments above denote a storage
 update of storage address `x` to value `y`.
-The scalar `i` is stored at storage address `0`, which is derived from it's 
+The scalar `i` is stored at storage address `0`, which is derived from its 
 slot number in the contract (slots are numbered in order of appearance in the
 source code).
 The array `a` is stored contiguously, starting from slot `hash(1)`.
@@ -281,15 +356,15 @@ mapping is being accessed; thus the storage slot used for the entry of `m` under
  key `k` is computed as `hash(2, k)`.
 
 We can see that non-collision of hashes is essential for storage integrity. 
-E.g., if `hash(1) + j` was equal to `hash(2, k)` then the operations on `a` an
+E.g., if `hash(1) + j` was equal to `hash(2, k)` then the operations on `a` and
 `m` would interfere with each other, and `foo` would return the value of 
 `writeToMap` rather than the value of `writeToArray`.
 
 
 ## Conclusion
 
-To summarize, Certora Prover handles hashing in a way that behaves as expected
-for most hashes. 
+To summarize, the Certora Prover handles hashing in a way that behaves as
+expected for most hashes. 
 
 However, it is good to be aware of limitations of the modeling; i.e. that not
 all properties of the actual Keccak function are preserved but only the ones 
diff --git a/docs/user-guide/getting-started/install.md b/docs/user-guide/getting-started/install.md
index d710c7ea..056cbaf6 100644
--- a/docs/user-guide/getting-started/install.md
+++ b/docs/user-guide/getting-started/install.md
@@ -231,6 +231,9 @@ follow the next steps:
     source .zshenv
     ```
 
+When running the Certora Prover in the Visual Studio Code Extension, you may need
+to restart VSCode or your computer.
+
 </details>
 
 <details>
diff --git a/docs/user-guide/glossary.md b/docs/user-guide/glossary.md
index f85e0606..6801d901 100644
--- a/docs/user-guide/glossary.md
+++ b/docs/user-guide/glossary.md
@@ -1,3 +1,4 @@
+(glossary)=
 Glossary
 ========
 
@@ -15,12 +16,11 @@ control flow graph
   control flow graph.
   A CVL rule can be seen as a program with some extra "assert" commands, thus 
   a rule has a CFG like regular programs.
-  Certora Prover's [TAC reports](tac-reports) contain a control flow graph of 
-  the {term}`TAC` intermediate representation of each given CVL rule.
-  Further reading: [wikipedia](https://en.wikipedia.org/wiki/Control-flow_graph)
+  The Certora Prover's [TAC reports](tac-reports) contain a control flow graph 
+  of the {term}`TAC` intermediate representation of each given CVL rule.
+  Further reading: [Wikipedia](https://en.wikipedia.org/wiki/Control-flow_graph)
   % TODO: ok to mention TAC here?
 
-
 environment
   The environment of a method call refers to the global variables that solidity
   provides, including `msg`, `block`, and `tx`.  CVL represents these variables
@@ -28,11 +28,23 @@ environment
   the contract state or the state of other contracts --- these are referred to
   as the {ref}`storage <storage-type>`.
 
+EVM
+Ethereum Virtual Machine
+EVM bytecode
+  EVM is short for Ethereum Virtual Machine.
+  EVM bytecode is one of the source languages that the Certora Prover internally
+  can take as input for verification. It is produced by the Solidity and Vyper 
+  compilers, among others.
+  For details on what the EVM is and how it works, the following links provide
+  good entry points.
+  [Official documentation](https://ethereum.org/en/developers/docs/evm/)
+  [Wikipedia](https://en.wikipedia.org/wiki/Ethereum#Virtual_machine)
+
 havoc
-  In some cases, the Prover should assume that some variables can change in an
-  unknown way.  For example, an external function on an unknown contract may
-  have an arbitrary effect on the state of a third contract.  In this case, we
-  say that the variable was "havoced".  See {ref}`havoc-summary` and
+  In some cases, the Certora Prover should assume that some variables can change 
+  in an unknown way.  For example, an external function on an unknown contract 
+  may have an arbitrary effect on the state of a third contract.  In this case, 
+  we say that the variable was "havoced".  See {ref}`havoc-summary` and
   {ref}`havoc-stmt` for more details.
 
 hyperproperty
@@ -49,9 +61,18 @@ invariant
 model
 example
 counterexample
-  The terms "model", "example", and "counterexample" are used interchangeably.
-  They all refer to an assignment of values to all of the CVL variables and
-  contract storage.  See {ref}`rule-overview`.
+witness example
+  We use the terms "model" and "example" interchangeably.
+  In the context of a CVL rule, they refer to an assignment of values to all of 
+  the CVL variables and contract storage that either violates an `assert` 
+  statement or fulfills a `satisfy` statement. 
+  In the `assert` case, we also call the model a "counterexample". In the 
+  `satisfy` case, we also call the model "witness example".
+  See {ref}`rule-overview`.
+  In the context of {term}`SMT solver`s, a model is a valuation of the logical 
+  constants and uninterpreted functions in the input formula that makes the formula
+  evaluate to `true`, also see {term}`SAT result`.
+
 
 linear arithmetic
 nonlinear arithmetic
@@ -69,9 +90,11 @@ underapproximation
   simpler that is easier to reason about.  If the approximation includes all of
   the possible behaviors of the original code (and possibly others), it is
   called an "overapproximation"; if it does not then it is called an
-  "underapproximation".  For example, a {ref}`NONDET <view-summary>` summary is
+  "underapproximation".  
+  
+  Example: A {ref}`NONDET <view-summary>` summary is
   an overapproximation because every possible value that the original
-  implementation could return is considered by the Prover, while an
+  implementation could return is considered by the Certora Prover, while an
   {ref}`ALWAYS <view-summary>` summary is an underapproximation if the
   summarized method could return more than one value.
 
@@ -83,8 +106,8 @@ underapproximation
 
 parametric rule
   A parametric rule is a rule that calls an ambiguous method, either using a
-  method variable, or using an overloaded function name.  The Prover will
-  generate a separate report for each possible instantiation of the method.
+  method variable, or using an overloaded function name. The Certora Prover 
+  will generate a separate report for each possible instantiation of the method.
   See {ref}`parametric-rules` for more information.
 
 quantifier
@@ -99,9 +122,24 @@ sanity
   This section is incomplete.  See {ref}`--rule_sanity` and {ref}`built-in-sanity` for partial information.
   ```
 
+SAT result
+UNSAT result
+  *SAT* and *UNSAT* are the results that an {term}`SMT solver` returns on a 
+  successful run (i.e. not a timeout). SAT means that the input formula is 
+  satisfiable and a {term}`model` has been found. UNSAT means that the input 
+  formula is unsatisfiable (and thus there is no model for it).
+  Within the Certora Prover, what SAT means depends on the type of rule 
+  being checked: For an `assert` rule, SAT means the rule is violated and the 
+  SMT model corresponds to a counterexample.
+  For a `satisfy` rule, SAT means the rule is not violated and the SMT model
+  corresponds to a witness example.
+  Conversely, UNSAT means that an `assert` is never violated or a `satisfy` never
+  fulfilled respectively.
+  (See also {ref}`rule-overview`.)
+
 scene
-  The *scene* refers to the set of contract instances that the Prover knows
-  about.
+  The *scene* refers to the set of contract instances that the Certora Prover 
+  knows about.
 
 SMT
 SMT solver
@@ -117,30 +155,30 @@ SMT solver
   formula evaluate to "true". For instance, on the formula "x > 5 /\ x = y * y", 
   a solver will return SAT, and produce any valuation where x is the square of
   an integer and larger than 5, and y is the root of x.
-  Further reading: [wikipedia](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)
+  Further reading: [Wikipedia](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)
 
 sound
 unsound
   Soundness means that any rule violations in the code being verified are
-  guaranteed to be reported by the Prover.  Unsound approximations such as
-  loop unrolling or certain kinds of harnessing may cause real bugs to be
-  missed by the Prover, and should therefore be used with caution.  See
+  guaranteed to be reported by the Certora Prover.  Unsound approximations 
+  such as loop unrolling or certain kinds of harnessing may cause real bugs 
+  to be missed by the Prover, and should therefore be used with caution. See
   {doc}`/docs/prover/approx/index` for more details.
 
 summary
 summarize
   A method summary is a user-provided approximation of the behavior of a
   contract method.  Summaries are useful if the implementation of a method is
-  not available or if the implementation is too complex for the Prover to
-  analyze without timing out.  See {doc}`/docs/cvl/methods` for
+  not available or if the implementation is too complex for the Certora 
+  Prover to analyze without timing out.  See {doc}`/docs/cvl/methods` for
   complete information on different types of method summaries.
 
 TAC
   TAC (originally short for "three address code") is an intermediate 
   representation
-  ([wikipedia](https://en.wikipedia.org/wiki/Intermediate_representation))
+  ([Wikipedia](https://en.wikipedia.org/wiki/Intermediate_representation))
   used by the Certora Prover. TAC code is kept invisible to the 
-  user most of the time, so it's details are not in the scope of this 
+  user most of the time, so its details are not in the scope of this 
   documentation. We provide a working understanding, which is helpful for some 
   advanced proving tasks, in the {ref}`tac-reports` section.
 
diff --git a/docs/user-guide/tutorials.md b/docs/user-guide/tutorials.md
index e0cf2e4d..c6335a0a 100644
--- a/docs/user-guide/tutorials.md
+++ b/docs/user-guide/tutorials.md
@@ -44,6 +44,7 @@ following topics:
 | [The Certora Prover pipeline](https://youtu.be/vg6da3A7lSs) | ({download}`slides <basics/stanford/09-pipeline.pdf>`)        |
 | [SMT solvers                ](https://youtu.be/9QuS_8cL91w) | ({download}`slides <basics/stanford/10-smt.pdf>`)             |
 
+The covered examples are available in the [CVL examples repository](https://github.com/Certora/Examples).
 
 [stanford]: https://www.youtube.com/playlist?list=PLKtu7wuOMP9Wp_O8kylKbtFYgM8HVTGIA