diff --git a/CLIFlags/README.md b/CLIFlags/README.md
index 80de0286..78e6cf73 100644
--- a/CLIFlags/README.md
+++ b/CLIFlags/README.md
@@ -29,9 +29,9 @@ For more information about available CLI options go to: https://docs.certora.com
 | [--summary_recursion_limit](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#summary-recursion-limit) | |
 | [--optimistic_hashing](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-hashing) | |
 | [--hashing_length_bound](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#hashing-length-bound) | |
-| [--link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#link) | [Liquidity Pool without linking](https://prover.certora.com/output/15800/e80f04180604458597fecc47c2b64e74?anonymousKey=b893bb90a8858acf903ba4aff1006af89a96d188) / [With linking](https://prover.certora.com/output/15800/f8f4b7a9180b49c1acdff4111a3c8e7a?anonymousKey=4a5b9ea156448922f7a1b4a25311d2b1e5c676ad) |
+| [--link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#link) | [Liquidity Pool without linking](https://prover.certora.com/output/15800/e80f04180604458597fecc47c2b64e74?anonymousKey=b893bb90a8858acf903ba4aff1006af89a96d188) / [With linking](https://prover.certora.com/output/15800/f8f4b7a9180b49c1acdff4111a3c8e7a?anonymousKey=4a5b9ea156448922f7a1b4a25311d2b1e5c676ad). **Note**: The spec-based [`links { }` block](../CVLByExample/LinksBlock/) is now the preferred approach, supporting structs, arrays, mappings, and wildcards natively. |
 | [--address](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#address) | |
-| [--struct_link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#struct-link) | |
+| [--struct_link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#struct-link) | **Note**: The spec-based [`links { }` block](../CVLByExample/LinksBlock/) is now the preferred approach. |
 | --foundry_tests_mode | [Foundry integration example](https://prover.certora.com/output/15800/70e5d5141ce34e4eae0f9966b78b34d9?anonymousKey=40a3a0266ff277d769a873681b1fc7829b0b5c55) |
 | --auto_dispatcher | [True](https://prover.certora.com/output/15800/e803efce805b473e9347e6b1b47fd8ac?anonymousKey=8b01aeed7d78c9165d7f79df8639aa7da550f361)/[False](https://prover.certora.com/output/15800/d65194e18b1c442db1182d3266ec6638?anonymousKey=536d7d2b5bf3cb3d75a5a06c0a002fc68a9e76e1) |
 | [--split_rules](https://docs.certora.com/en/latest/docs/prover/cli/options.html#split-rules-rule-name-pattern) | Splitting the rule `permitFrontRun` from an ERC20 full spec run: [Instance only running `permitFrontRun`](https://prover.certora.com/output/15800/662059e5f478418c872504d1c922dcdf?anonymousKey=8da20e873559812bcba3c2045aad35e9e20f6fb7), [Instance running the rest of the rules](https://prover.certora.com/output/15800/6a7d370b3d894807bbbf73d2711c9da0?anonymousKey=149479f02f6bef7df0dcf2571b86c3066dbaa119) |
diff --git a/CVLByExample/LinksBlock/AdvancedLinking.conf b/CVLByExample/LinksBlock/AdvancedLinking.conf
new file mode 100644
index 00000000..bee48f49
--- /dev/null
+++ b/CVLByExample/LinksBlock/AdvancedLinking.conf
@@ -0,0 +1,13 @@
+{
+    "files": [
+        "AdvancedRegistry.sol",
+        "BasicVault.sol",
+        "Tokens.sol:TokenA",
+        "Tokens.sol:TokenB",
+        "Tokens.sol:TokenC",
+        "Tokens.sol:TokenD"
+    ],
+    "verify": "AdvancedRegistry:AdvancedLinking.spec",
+    "rule_sanity": "basic",
+    "msg": "Links block: advanced (wildcards, multi-target, mappings, nesting)"
+}
diff --git a/CVLByExample/LinksBlock/AdvancedLinking.spec b/CVLByExample/LinksBlock/AdvancedLinking.spec
new file mode 100644
index 00000000..95f1e4c7
--- /dev/null
+++ b/CVLByExample/LinksBlock/AdvancedLinking.spec
@@ -0,0 +1,136 @@
+/// Advanced `links { }` block example: wildcards, multi-target dispatch,
+/// mappings, nested containers, and struct arrays.
+///
+/// Demonstrates capabilities that go beyond what the `--link` conf flag can do.
+
+using AdvancedRegistry as registry;
+using TokenA as tokenA;
+using TokenB as tokenB;
+using TokenC as tokenC;
+using TokenD as tokenD;
+
+links {
+    // Multi-target dispatch: the address resolves to one of the listed contracts
+    registry.multiTarget => [tokenA, tokenB];
+
+    // Wildcard dynamic array: all elements resolve to tokenA or tokenB
+    registry.dynamicTokens[_] => [tokenA, tokenB];
+
+    // Mapping with concrete key + wildcard precedence:
+    // Key 0 always resolves to tokenA; all other keys resolve to tokenB
+    registry.tokenMap[0] => tokenA;
+    registry.tokenMap[_] => tokenB;
+
+    // Address-keyed mapping: contract alias used as the key
+    registry.addrMap[tokenA] => tokenC;
+    registry.addrMap[tokenB] => tokenD;
+
+    // Wildcard + concrete precedence on array:
+    // Index 0 is always tokenC; all other indices are tokenA
+    registry.precedenceTokens[0] => tokenC;
+    registry.precedenceTokens[_] => tokenA;
+
+    // bytes4-keyed mapping: to_bytes4(...) cast as the key
+    registry.bytes4Map[to_bytes4(0x12345678)] => tokenA;
+    registry.bytes4Map[to_bytes4(0xdeadbeef)] => tokenB;
+
+    // Nested mapping: two-level indexing
+    registry.mapMap[0][0] => tokenC;
+    registry.mapMap[_][_] => [tokenA, tokenD];
+
+    // Struct in array: wildcard access to a struct field
+    registry.holderArray[_].token => [tokenA, tokenC];
+}
+
+methods {
+    function getMultiTargetValue() external returns (uint) envfree;
+    function getDynamicTokenValue(uint) external returns (uint) envfree;
+    function dynamicTokensLength() external returns (uint) envfree;
+    function getTokenMapValue(uint) external returns (uint) envfree;
+    function getAddrMapValue(address) external returns (uint) envfree;
+    function getPrecedenceValue(uint) external returns (uint) envfree;
+    function precedenceTokensLength() external returns (uint) envfree;
+    function getBytes4MapValue(bytes4) external returns (uint) envfree;
+    function getMapMapValue(uint, uint) external returns (uint) envfree;
+    function getHolderArrayValue(uint) external returns (uint) envfree;
+    function holderArrayLength() external returns (uint) envfree;
+}
+
+/// Multi-target: value must be TokenA (1) or TokenB (2)
+rule multiTargetDispatch {
+    uint val = getMultiTargetValue();
+    assert val == 1 || val == 2;
+    assert registry.multiTarget == tokenA || registry.multiTarget == tokenB;
+}
+
+/// Wildcard dynamic array: every element is TokenA or TokenB
+rule wildcardDynamicArray {
+    uint i;
+    require dynamicTokensLength() > i;
+    uint val = getDynamicTokenValue(i);
+    assert val == 1 || val == 2;
+    assert registry.dynamicTokens[i] == tokenA || registry.dynamicTokens[i] == tokenB;
+}
+
+/// Mapping with wildcard precedence: key 0 -> TokenA (1), all others -> TokenB (2)
+rule mappingWithPrecedence {
+    // Concrete key takes priority
+    assert getTokenMapValue(0) == 1;
+    assert registry.tokenMap[0] == tokenA;
+
+    // Wildcard applies to all other keys
+    uint key;
+    require key != 0;
+    assert getTokenMapValue(key) == 2;
+    assert registry.tokenMap[key] == tokenB;
+}
+
+/// Address-keyed mapping: contract aliases as keys
+rule addressKeyedMapping {
+    assert getAddrMapValue(tokenA) == 3;  // tokenA -> tokenC (value 3)
+    assert getAddrMapValue(tokenB) == 4;  // tokenB -> tokenD (value 4)
+    assert registry.addrMap[tokenA] == tokenC;
+    assert registry.addrMap[tokenB] == tokenD;
+}
+
+/// Wildcard + concrete precedence on array:
+/// Index 0 is tokenC (3), all others are tokenA (1)
+rule arrayPrecedence {
+    require precedenceTokensLength() >= 2;
+
+    assert getPrecedenceValue(0) == 3;
+    assert registry.precedenceTokens[0] == tokenC;
+
+    assert getPrecedenceValue(1) == 1;
+    assert registry.precedenceTokens[1] == tokenA;
+}
+
+/// bytes4-keyed mapping: to_bytes4 casts as keys
+rule bytes4Mapping {
+    assert getBytes4MapValue(to_bytes4(0x12345678)) == 1;  // tokenA
+    assert getBytes4MapValue(to_bytes4(0xdeadbeef)) == 2;  // tokenB
+    assert registry.bytes4Map[to_bytes4(0x12345678)] == tokenA;
+    assert registry.bytes4Map[to_bytes4(0xdeadbeef)] == tokenB;
+}
+
+/// Nested mapping: concrete [0][0] -> tokenC (3),
+/// wildcard [_][_] -> tokenA (1) or tokenD (4)
+rule nestedMapping {
+    // Concrete entry
+    assert getMapMapValue(0, 0) == 3;
+
+    // Wildcard entries
+    uint i; uint j;
+    require i != 0 || j != 0;
+    uint val = getMapMapValue(i, j);
+    assert val == 1 || val == 4;
+}
+
+/// Struct in array: wildcard links holderArray[_].token to tokenA or tokenC
+rule structInArray {
+    uint i;
+    require holderArrayLength() > i;
+    uint val = getHolderArrayValue(i);
+    assert val == 1 || val == 3;
+    assert registry.holderArray[i].token == tokenA || registry.holderArray[i].token == tokenC;
+}
diff --git a/CVLByExample/LinksBlock/AdvancedRegistry.sol b/CVLByExample/LinksBlock/AdvancedRegistry.sol
new file mode 100644
index 00000000..3b72f498
--- /dev/null
+++ b/CVLByExample/LinksBlock/AdvancedRegistry.sol
@@ -0,0 +1,77 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import "./Tokens.sol";
+import {TokenHolder} from "./BasicVault.sol";
+
+contract AdvancedRegistry {
+    // Multi-target dispatch: address could be one of several contracts
+    address public multiTarget;
+
+    // Dynamic array
+    address[] public dynamicTokens;
+
+    // Uint-keyed mapping
+    mapping(uint256 => address) public tokenMap;
+
+    // Address-keyed mapping (contract alias can be used as key in spec)
+    mapping(address => address) public addrMap;
+
+    // For wildcard + concrete precedence demo
+    address[] public precedenceTokens;
+
+    // Bytes4-keyed mapping
+    mapping(bytes4 => address) public bytes4Map;
+
+    // Nested mapping
+    mapping(uint256 => mapping(uint256 => address)) public mapMap;
+
+    // Struct in array
+    TokenHolder[] public holderArray;
+
+    // --- Accessor functions ---
+
+    function getMultiTargetValue() external view returns (uint) {
+        return IToken(multiTarget).getValue();
+    }
+
+    function getDynamicTokenValue(uint i) external view returns (uint) {
+        return IToken(dynamicTokens[i]).getValue();
+    }
+
+    function dynamicTokensLength() external view returns (uint) {
+        return dynamicTokens.length;
+    }
+
+    function getTokenMapValue(uint key) external view returns (uint) {
+        return IToken(tokenMap[key]).getValue();
+    }
+
+    function getAddrMapValue(address key) external view returns (uint) {
+        return IToken(addrMap[key]).getValue();
+    }
+
+    function getPrecedenceValue(uint i) external view returns (uint) {
+        return IToken(precedenceTokens[i]).getValue();
+    }
+
+    function precedenceTokensLength() external view returns (uint) {
+        return precedenceTokens.length;
+    }
+
+    function getBytes4MapValue(bytes4 key) external view returns (uint) {
+        return IToken(bytes4Map[key]).getValue();
+    }
+
+    function getMapMapValue(uint i, uint j) external view returns (uint) {
+        return IToken(mapMap[i][j]).getValue();
+    }
+
+    function getHolderArrayValue(uint i) external view returns (uint) {
+        return IToken(holderArray[i].token).getValue();
+    }
+
+    function holderArrayLength() external view returns (uint) {
+        return holderArray.length;
+    }
+}
diff --git a/CVLByExample/LinksBlock/BasicLinking.conf b/CVLByExample/LinksBlock/BasicLinking.conf
new file mode 100644
index 00000000..5f7ec01c
--- /dev/null
+++ b/CVLByExample/LinksBlock/BasicLinking.conf
@@ -0,0 +1,11 @@
+{
+    "files": [
+        "BasicVault.sol",
+        "Tokens.sol:TokenA",
+        "Tokens.sol:TokenB",
+        "Tokens.sol:TokenC"
+    ],
+    "verify": "BasicVault:BasicLinking.spec",
+    "rule_sanity": "basic",
+    "msg": "Links block: basic linking (scalar, immutable, struct, array)"
+}
diff --git a/CVLByExample/LinksBlock/BasicLinking.spec b/CVLByExample/LinksBlock/BasicLinking.spec
new file mode 100644
index 00000000..96ac024d
--- /dev/null
+++ b/CVLByExample/LinksBlock/BasicLinking.spec
@@ -0,0 +1,51 @@
+/// Basic `links { }` block example: scalar, immutable, struct, and static array linking.
+///
+/// This spec demonstrates the new spec-based linking syntax, replacing the
+/// `--link` and `--struct_link` conf flags. All linking is declared in the spec
+/// alongside the rules that depend on it.
+
+using BasicVault as vault;
+using TokenA as tokenA;
+using TokenB as tokenB;
+using TokenC as tokenC;
+
+links {
+    vault.primaryToken => tokenA;       // scalar field
+    vault.immutableToken => tokenB;     // immutable field
+    vault.holder.token => tokenC;       // struct field (not possible with --link conf flag)
+    vault.fixedTokens[0] => tokenA;    // static array element
+    vault.fixedTokens[1] => tokenB;
+}
+
+methods {
+    function getPrimaryValue() external returns (uint) envfree;
+    function getImmutableValue() external returns (uint) envfree;
+    function getHolderValue() external returns (uint) envfree;
+    function getFixedTokenValue(uint) external returns (uint) envfree;
+}
+
+/// Scalar field: primaryToken is linked to TokenA (value 1)
+rule scalarLinked {
+    assert getPrimaryValue() == 1;
+    assert vault.primaryToken == tokenA;
+}
+
+/// Immutable field: immutableToken is linked to TokenB (value 2)
+rule immutableLinked {
+    assert getImmutableValue() == 2;
+    assert vault.immutableToken == tokenB;
+}
+
+/// Struct field: holder.token is linked to TokenC (value 3)
+rule structFieldLinked {
+    assert getHolderValue() == 3;
+    assert vault.holder.token == tokenC;
+}
+
+/// Static array: fixedTokens[0] = TokenA (1), fixedTokens[1] = TokenB (2)
+rule staticArrayLinked {
+    assert getFixedTokenValue(0) == 1;
+    assert getFixedTokenValue(1) == 2;
+    assert vault.fixedTokens[0] == tokenA;
+    assert vault.fixedTokens[1] == tokenB;
+}
diff --git a/CVLByExample/LinksBlock/BasicVault.sol b/CVLByExample/LinksBlock/BasicVault.sol
new file mode 100644
index 00000000..bdf56ff8
--- /dev/null
+++ b/CVLByExample/LinksBlock/BasicVault.sol
@@ -0,0 +1,36 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import "./Tokens.sol";
+
+struct TokenHolder {
+    address token;
+    uint256 weight;
+}
+
+contract BasicVault {
+    address public primaryToken;
+    address public immutable immutableToken;
+    TokenHolder public holder;
+    address[2] public fixedTokens;
+
+    constructor(address _immutableToken) {
+        immutableToken = _immutableToken;
+    }
+
+    function getPrimaryValue() external view returns (uint) {
+        return IToken(primaryToken).getValue();
+    }
+
+    function getImmutableValue() external view returns (uint) {
+        return IToken(immutableToken).getValue();
+    }
+
+    function getHolderValue() external view returns (uint) {
+        return IToken(holder.token).getValue();
+    }
+
+    function getFixedTokenValue(uint i) external view returns (uint) {
+        return IToken(fixedTokens[i]).getValue();
+    }
+}
diff --git a/CVLByExample/LinksBlock/ConfStyleLinking.conf b/CVLByExample/LinksBlock/ConfStyleLinking.conf
new file mode 100644
index 00000000..cee24c5f
--- /dev/null
+++ b/CVLByExample/LinksBlock/ConfStyleLinking.conf
@@ -0,0 +1,14 @@
+{
+    "files": [
+        "BasicVault.sol",
+        "Tokens.sol:TokenA",
+        "Tokens.sol:TokenB"
+    ],
+    "verify": "BasicVault:ConfStyleLinking.spec",
+    "link": [
+        "BasicVault:primaryToken=TokenA",
+        "BasicVault:immutableToken=TokenB"
+    ],
+    "rule_sanity": "basic",
+    "msg": "Conf-style linking with --link flag (old approach)"
+}
diff --git a/CVLByExample/LinksBlock/ConfStyleLinking.spec b/CVLByExample/LinksBlock/ConfStyleLinking.spec
new file mode 100644
index 00000000..f7b72d2f
--- /dev/null
+++ b/CVLByExample/LinksBlock/ConfStyleLinking.spec
@@ -0,0 +1,27 @@
+/// Conf-style linking example: same contract, but linking is done via the
+/// `--link` conf flag instead of a `links { }` block.
+///
+/// Note: The `--link` conf flag can only link scalar and immutable fields.
+/// Struct fields (like holder.token) and array elements require either
+/// `--struct_link` or the new `links { }` block.
+
+using BasicVault as vault;
+using TokenA as tokenA;
+using TokenB as tokenB;
+
+methods {
+    function getPrimaryValue() external returns (uint) envfree;
+    function getImmutableValue() external returns (uint) envfree;
+}
+
+/// Scalar field: primaryToken is linked to TokenA (value 1) via conf --link
+rule scalarLinked {
+    assert getPrimaryValue() == 1;
+    assert vault.primaryToken == tokenA;
+}
+
+/// Immutable field: immutableToken is linked to TokenB (value 2) via conf --link
+rule immutableLinked {
+    assert getImmutableValue() == 2;
+    assert vault.immutableToken == tokenB;
+}
diff --git a/CVLByExample/LinksBlock/README.md b/CVLByExample/LinksBlock/README.md
new file mode 100644
index 00000000..bad67be8
--- /dev/null
+++ b/CVLByExample/LinksBlock/README.md
@@ -0,0 +1,69 @@
+# Links Block Example
+
+## Overview
+
+The `links { }` block is a CVL feature for declaring contract linking directly in the spec file, replacing the `--link` and `--struct_link` conf flags. Linking tells the Prover which concrete contract an address field points to, enabling precise verification of multi-contract interactions.
+
+With the `links { }` block, linking declarations live alongside the rules that depend on them, and support advanced features like struct field linking, array/mapping indexing, wildcards, and multi-target dispatch.
+
+## Syntax Quick Reference
+
+| Pattern | Description |
+| ------- | ----------- |
+| `main.field => target` | Scalar or immutable field |
+| `main.holder.token => target` | Struct field (dot notation) |
+| `main.arr[0] => target` | Array element (concrete index) |
+| `main.arr[_] => target` | Wildcard (all indices) |
+| `main.arr[0] => targetA; main.arr[_] => targetB` | Concrete precedence (index 0 -> targetA, rest -> targetB) |
+| `main.field => [targetA, targetB]` | Multi-target dispatch |
+| `main.map[0] => target` | Mapping (concrete key) |
+| `main.map[_] => target` | Mapping (wildcard key) |
+| `main.map[to_bytes4(0x1234)] => target` | Typed key cast |
+| `main.map[contractAlias] => target` | Contract alias as key |
+| `main.map[0][0] => target` | Nested mapping/array |
+| `main.arr[_].field => target` | Struct field in array |
+
+## Examples
+
+### 1. BasicLinking — Scalar, immutable, struct, static array
+
+Demonstrates the most common linking patterns using the new `links { }` syntax.
+
+**Command:**
+```bash
+certoraRun BasicLinking.conf
+```
+
+### 2. ConfStyleLinking — Comparison with old `--link` conf flag
+
+Same contract, but linking is done via the `--link` conf flag. Only scalar and immutable fields can be linked this way — struct fields and arrays require the `links { }` block.
+
+**Command:**
+```bash
+certoraRun ConfStyleLinking.conf
+```
+
+### 3. AdvancedLinking — Wildcards, multi-target, mappings, nesting
+
+Demonstrates advanced capabilities:
+- **Multi-target dispatch**: `field => [tokenA, tokenB]` — the Prover considers both targets
+- **Wildcard arrays**: `arr[_] => target` — all indices resolve to the target
+- **Wildcard precedence**: concrete entries override wildcards at the same path
+- **Address-keyed mappings**: contract aliases used as mapping keys
+- **bytes4-keyed mappings**: `to_bytes4(...)` casts as keys
+- **Nested mappings**: `map[i][j] => target`
+- **Struct arrays**: `arr[_].field => target`
+
+**Command:**
+```bash
+certoraRun AdvancedLinking.conf
+```
+
+## Important Notes
+
+- The `links { }` block and `--link`/`--struct_link` conf flags are **mutually exclusive** per contract. You cannot use both for the same contract.
+- For dynamic arrays with concrete element links, the compiler assumes `length > index` for each linked index.
+- When both concrete and wildcard entries exist at the same path, concrete entries take precedence.
+- Wildcard indices cannot be mixed with concrete indices in the same entry (e.g., `arr[0][_]` is not allowed — use all concrete or all wildcards).
+
+For a comprehensive guide on Certora Verification Language, refer to the [Certora Documentation](https://docs.certora.com).
diff --git a/CVLByExample/LinksBlock/Tokens.sol b/CVLByExample/LinksBlock/Tokens.sol
new file mode 100644
index 00000000..3757fb04
--- /dev/null
+++ b/CVLByExample/LinksBlock/Tokens.sol
@@ -0,0 +1,30 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+interface IToken {
+    function getValue() external view returns (uint);
+}
+
+contract TokenA is IToken {
+    function getValue() external pure returns (uint) {
+        return 1;
+    }
+}
+
+contract TokenB is IToken {
+    function getValue() external pure returns (uint) {
+        return 2;
+    }
+}
+
+contract TokenC is IToken {
+    function getValue() external pure returns (uint) {
+        return 3;
+    }
+}
+
+contract TokenD is IToken {
+    function getValue() external pure returns (uint) {
+        return 4;
+    }
+}
diff --git a/CVLByExample/README.md b/CVLByExample/README.md
index 1aa9b4f7..b52b76a5 100644
--- a/CVLByExample/README.md
+++ b/CVLByExample/README.md
@@ -35,6 +35,7 @@
 | **struct**        | [struct return type](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L47),<br> `struct` in `methods` block: [struct parameter](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L23), [struct return type](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L19),<br> [returning a struct as a tuple](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L21),<br> `struct` in a `CVL` function: [struct parameter to a CVL function](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L36),<br> [struct return type of a CVL function](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L47), [returning struct as a tuple](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L53),<br> [assignment to struct](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L98), [Assigning struct to a tuple](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L77) |
 | **use**           | `rule`: [with filters](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L32), [overriding imported filters](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L32),<br> [`invariant`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L10): [overriding imported `preserved`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L12), [builtin rule](https://github.com/Certora/Examples/blob/master/CVLByExample/Reentrancy/certora/spec/ViewReentrancy.spec#L1) |
 | **using**         | [`using`](https://github.com/Certora/Examples/blob/master/DEFI/LiquidityPool/certora/specs/pool_link.spec#L14) |
+| **links { }**     | [Basic linking](CVLByExample/LinksBlock/BasicLinking.spec), [Advanced (wildcards, multi-target, nesting)](CVLByExample/LinksBlock/AdvancedLinking.spec), [Comparison with --link conf flag](CVLByExample/LinksBlock/ConfStyleLinking.spec) |
 | **withrevert**    | [`withrevert`](https://github.com/Certora/Examples/blob/master/CVLByExample/Storage/certora/specs/storage.spec#L44) |
 | **CVL Type**  | [mathint](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L23), [method](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L83), [env](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L20) |
 | **ercecover**  | [example](https://github.com/Certora/Examples/blob/master/CVLByExample/Ecrecover/ecrecover.spec#L67) |