Certora · shellygr · May 8, 2026 · Apr 26, 2026 · May 8, 2026
diff --git a/docs/cvl/defs.md b/docs/cvl/defs.md
@@ -9,14 +9,14 @@ In CVL, **definitions** serve as type-checked macros, encapsulating commonly use
 
 ```cvl
 methods {
-  foo(uint256) returns bool envfree
+  function foo(uint256) external returns(bool) envfree;
 }
 
-definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffff;
+definition MAX_UINT128() returns uint256 = 0xffffffffffffffffffffffffffffffff;
 definition is_even(uint256 x) returns bool = exists uint256 y . 2 * y == x;
 
 rule my_rule(uint256 x) {
-  require is_even(x) && x <= MAX_UINT256();
+  require is_even(x) && x <= MAX_UINT128();
   foo@withrevert(x);
   assert !lastReverted;
 }
@@ -32,11 +32,11 @@ Definitions can include an application of another definition, allowing for arbit
 `is_odd` and `is_odd_no_overflow` both reference other definitions:
 
 ```cvl
-definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffff;
+definition MAX_UINT128() returns uint256 = 0xffffffffffffffffffffffffffffffff;
 definition is_even(uint256 x) returns bool = exists uint256 y . 2 * y == x;
 definition is_odd(uint256 x) returns bool = !is_even(x);
 definition is_odd_no_overflow(uint256 x) returns bool =
-    is_odd(x) && x <= MAX_UINT256();
+    is_odd(x) && x <= MAX_UINT128();
 ```
 
 ### Type Error circular dependency

diff --git a/docs/cvl/expr.md b/docs/cvl/expr.md
@@ -46,11 +46,11 @@ binop ::= "+" | "-" | "*" | "/" | "%" | "^"
         | "=>" | "<=>" | "xor" | ">>>"
 
 specials_fields ::=
-           | "block" "." [ "number" | "timestamp" ]
-           | "msg"   "." [ "address" | "sender" | "value" ]
+           | "block" "." [ "number" | "timestamp" | "basefee" | "coinbase" | "difficulty" | "gaslimit" ]
+           | "msg"   "." [ "sender" | "value" ]
            | "tx"    "." [ "origin" ]
            | "length"
-           | "selector" | "isPure" | "isView" | "numberOfArguments" | "isFallback"
+           | "selector" | "isPure" | "isView" | "numberOfArguments" | "isFallback" | "contract"
 
 special_vars ::=
            | "lastReverted"

diff --git a/docs/cvl/functions.md b/docs/cvl/functions.md
@@ -14,11 +14,11 @@ The syntax for CVL functions is given by the following [EBNF grammar](ebnf-synta
 function ::= [ "override" ]
              "function" id
              [ "(" params ")" ]
-             [ "returns" type ]
+             [ "returns" ( type | "(" type { "," type } ")" ) ]
              block
 ```
 
-See {doc}`basics` for the `id` production, {doc}`types` for the `type` production,
+See {doc}`basics` for the `id` production, {doc}`types` for the `cvl_type` production,
 and {doc}`statements` for the `block` production.
 
 Examples
@@ -35,6 +35,17 @@ Examples
     }
     ```
 
+- Function returning multiple values:
+    ```cvl
+    function min_max(uint256 x, uint256 y) returns (uint256, uint256) {
+        if (x < y) {
+            return (x, y);
+        } else {
+            return (y, x);
+        }
+    }
+    ```
+
 - [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)

diff --git a/docs/cvl/hooks.md b/docs/cvl/hooks.md
@@ -33,13 +33,25 @@ pattern ::= "Sstore" access_path param [ "(" param ")" ]
 access_path ::= id
               | [ id "." ] "(" "slot" number ")"
               | access_path "." id
+              | access_path "." "length"
               | access_path "[" "KEY"   basic_type id "]"
               | access_path "[" "INDEX" basic_type id "]"
               | access_path "." "(" "offset" number ")"
 
-opcode ::= "ALL_SLOAD" | "ALL_SSTORE" | "ALL_TLOAD" | "ALL_TSTORE" | ...
+opcode ::= "ALL_SLOAD"     | "ALL_SSTORE"   | "ALL_TLOAD"   | "ALL_TSTORE"
+         | "ADDRESS"       | "BALANCE"      | "ORIGIN"      | "CALLER"
+         | "CALLVALUE"     | "CODESIZE"     | "CODECOPY"    | "GASPRICE"
+         | "EXTCODESIZE"   | "EXTCODECOPY"  | "EXTCODEHASH" | "BLOCKHASH"
+         | "COINBASE"      | "TIMESTAMP"    | "NUMBER"      | "DIFFICULTY"
+         | "GASLIMIT"      | "CHAINID"      | "SELFBALANCE" | "BASEFEE"
+         | "MSIZE"         | "GAS"
+         | "LOG0" | "LOG1" | "LOG2" | "LOG3" | "LOG4"
+         | "CREATE1"       | "CREATE2"
+         | "CALL"          | "CALLCODE"     | "DELEGATECALL"| "STATICCALL"
+         | "REVERT"        | "BLOBHASH"     | "SELFDESTRUCT"
 
 param  ::= evm_type id
+params ::= param { "," param }
 ```
 
 See {ref}`opcode-hooks` below for the list of available opcodes.

diff --git a/docs/cvl/invariants.md b/docs/cvl/invariants.md
@@ -34,7 +34,7 @@ The syntax for invariants is given by the following [EBNF grammar](ebnf-syntax):
 invariant ::= [ "weak" | "strong" ] "invariant" id
               [ "(" params ")" ]
               expression
-              [ "filtered" "{" id "->" expression "}" ]
+              [ "filtered" "{" id "->" expression { "," id "->" expression } "}" ]
               [ "{" { preserved_block } "}" ]
 
 preserved_block ::= "preserved"

diff --git a/docs/cvl/linking.md b/docs/cvl/linking.md
@@ -32,8 +32,10 @@ link_path     ::= id "." id { link_segment }
 link_segment  ::= "." id
                | "[" index_expr "]"
 
+to_bytes_fn   ::= "to_bytes1" | "to_bytes2" | ... | "to_bytes32"
+
 index_expr    ::= number
-               | "to_bytes" number "(" number ")"
+               | to_bytes_fn "(" number ")"
                | id
                | "_"
 ```

diff --git a/docs/cvl/methods.md b/docs/cvl/methods.md
@@ -58,7 +58,7 @@ pattern          ::= exact_pattern | wildcard_pattern | catch_all_pattern
 
 exact_pattern    ::= [ id "." ] id "(" evm_params ")" visibility [ "returns" "(" evm_types ")" ]
 wildcard_pattern ::= "_" "." id "(" evm_params ")" visibility
-catch_all_pattern ::= id "." "_" "external"
+catch_all_pattern ::= ( id | "_" ) "." "_" "external"
 
 visibility ::= "internal" | "external"
 
@@ -70,22 +70,22 @@ method_summary   ::= "ALWAYS" "(" value ")"
                    | "NONDET"
                    | "HAVOC_ECF"
                    | "HAVOC_ALL"
-                   | "DISPATCHER" [ "(" ( "true" | "false" ) ")" ]
+                   | "DISPATCHER" [ "(" ( "true" | "false" | dispatch_args ) ")" ]
                    | "AUTO"
                    | "ASSERT_FALSE"
                    | expr [ "expect" id ]
                    | dispatch_list
 
-dispatch_list     ::=
-                   | "DISPATCH" [ "(optimistic=false)" ]  "[" dispatch_list_pattern [","] | empty "]" "default" method_summary
-                   | "DISPATCH" [ "(optimistic=true)" ]  "[" dispatch_list_pattern [","] | empty "]"
+dispatch_list    ::= "DISPATCH" [ "(" dispatch_args ")" ]
+                     "[" [ dispatch_pattern { "," dispatch_pattern } [ "," ] ] "]"
+                     [ "default" method_summary ]
 
-dispatch_list_patterns ::= dispatch_list_patterns "," dispatch_pattern
-                          | dispatch_pattern
+dispatch_args    ::= dispatch_arg { "," dispatch_arg }
+dispatch_arg     ::= ( "optimistic" | "use_fallback" ) "=" ( "true" | "false" )
 
-dispatch_pattern ::= | "_" "." id "(" evm_params ")"
-                     | id "." "_"
-                     | id "." id "(" evm_params ")"
+dispatch_pattern ::= "_" "." id "(" evm_params ")"
+                   | id "." "_"
+                   | id "." id "(" evm_params ")"
 ```
 
 See {doc}`types` for the `evm_type` production.  See {doc}`basics`
@@ -461,7 +461,8 @@ methods {
 `with(env e)` clauses
 ---------------------
 
-After the `optional` annotation, an entry may contain a `with(env e)` clause.
+An entry may contain a `with(env e)` clause in place of the `envfree` annotation,
+before any `optional` annotation.
 The `with` clause introduces a new variable (`e` for `with(env e)`) to represent
 the {ref}`environment <env>` that is passed to a summarized function; the
 variable can be used in function summaries.  `with` clauses may only be used if
@@ -722,7 +723,7 @@ In some cases there's a proxy contract that only has a fallback function and
 that fallback then delegates function calls it receives to some other contract.
 For this case it could be useful for `DISPATCHER` summaries to also inline the
 `fallback` function of known contracts. To enable this use the following syntax:
- * `DISPATCHER(optimistic=<true|false>, use_fallback<true|false>)`
+ * `DISPATCHER(optimistic=<true|false>, use_fallback=<true|false>)`
 
 ```{note}
 The most commonly used dispatcher mode is `DISPATCHER(true)`, because in almost

diff --git a/docs/cvl/statements.md b/docs/cvl/statements.md
@@ -38,7 +38,8 @@ statement ::= type id [ "=" expr ] ";"
 
             | "havoc" id [ "assuming" expr ] ";"
 
-lhs ::= id [ "[" expr "]" ] [ "," lhs ]
+lhs_atom ::= id { "[" expr "]" } { "." id }
+lhs      ::= lhs_atom { "," lhs_atom }
 ```
 
 See {doc}`basics` for the `id` and `string` productions.  See {doc}`types` for