diff --git a/.gitmodules b/.gitmodules
index f8e63d4..ec17023 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,8 +1,8 @@
-[submodule "lib/forge-std"]
-	path = lib/forge-std
+[submodule "oz_erc20/lib/forge-std"]
+	path = oz_erc20/lib/forge-std
 	url = https://github.com/foundry-rs/forge-std
-[submodule "lib/kontrol-cheatcodes"]
-	path = lib/kontrol-cheatcodes
+[submodule "oz_erc20/lib/kontrol-cheatcodes"]
+	path = oz_erc20/lib/kontrol-cheatcodes
 	url = https://github.com/runtimeverification/kontrol-cheatcodes.git
 [submodule "oz_erc20/lib/forge-std"]
 	path = oz_erc20/lib/forge-std
@@ -13,3 +13,9 @@
 [submodule "oz_erc20/lib/openzeppelin-contracts"]
 	path = oz_erc20/lib/openzeppelin-contracts
 	url = https://github.com/OpenZeppelin/openzeppelin-contracts
+[submodule "wonderland/lib/forge-std"]
+	path = wonderland/lib/forge-std
+	url = https://github.com/foundry-rs/forge-std
+[submodule "wonderland/lib/kontrol-cheatcodes"]
+	path = wonderland/lib/kontrol-cheatcodes
+	url = https://github.com/runtimeverification/kontrol-cheatcodes
diff --git a/oz_erc20/test/RebasingToken.t.sol b/oz_erc20/test/RebasingToken.t.sol
new file mode 100644
index 0000000..ea4e0b7
--- /dev/null
+++ b/oz_erc20/test/RebasingToken.t.sol
@@ -0,0 +1,23 @@
+pragma solidity ^0.8.13;
+
+import {Test, console} from "forge-std/Test.sol";
+
+contract RebasingTokenTest is Test {
+    function check_balanceToRebasingCredits(uint256 rebasingCreditsPerToken, uint256 balance) public {
+        vm.assume(rebasingCreditsPerToken <= 1e27 && rebasingCreditsPerToken >= 1e18);
+        vm.assume(balance <= 1e25);
+
+        uint256 rebasingCredits = ((balance) * rebasingCreditsPerToken + 1e18 - 1) / 1e18;
+        uint256 actualBalance = (rebasingCredits * 1e18) / rebasingCreditsPerToken;
+        assert(actualBalance == balance);
+    }
+
+    function testFail_balanceToRebasingCredits(uint256 rebasingCreditsPerToken, uint256 balance) public {
+        vm.assume(rebasingCreditsPerToken <= 1e27); // && rebasingCreditsPerToken >= 1e18);
+        vm.assume(balance <= 1e25);
+
+        uint256 rebasingCredits = ((balance) * rebasingCreditsPerToken + 1e18 - 1) / 1e18;
+        uint256 actualBalance = (rebasingCredits * 1e18) / rebasingCreditsPerToken;
+        assert(actualBalance == balance);
+    }
+}
\ No newline at end of file
diff --git a/wonderland/.gitignore b/wonderland/.gitignore
new file mode 100644
index 0000000..85198aa
--- /dev/null
+++ b/wonderland/.gitignore
@@ -0,0 +1,14 @@
+# Compiler files
+cache/
+out/
+
+# Ignores development broadcast logs
+!/broadcast
+/broadcast/*/31337/
+/broadcast/**/dry-run/
+
+# Docs
+docs/
+
+# Dotenv file
+.env
diff --git a/wonderland/KONTROL.md b/wonderland/KONTROL.md
new file mode 100644
index 0000000..8307fe0
--- /dev/null
+++ b/wonderland/KONTROL.md
@@ -0,0 +1,54 @@
+
+## Kontrol
+
+**Kontrol grants developers the ability to perform formal verification without learning a new language or tool.**
+
+## Documentation
+
+https://docs.runtimeverification.com/kontrol/cheatsheets/kontrol-cheatsheet
+
+## Usage
+
+### Build
+
+```shell
+$ kontrol build
+```
+
+### Test
+
+```shell
+$ kontrol prove --match-test 'ContractName.TestName()'
+```
+
+### List
+
+```shell
+$ kontrol list
+```
+
+### Show
+
+```shell
+$ kontrol show --match-test 'ContractName.TestName()'
+```
+
+### Explore KCFG
+
+```shell
+$ kontrol view-kcfg 'ContractName.TestName()'
+```
+
+### Clean
+
+```shell
+$ kontrol clean
+```
+
+
+### Help
+
+```shell
+$ kontrol --help
+$ kontrol command --help
+```
diff --git a/wonderland/README.md b/wonderland/README.md
new file mode 100644
index 0000000..9265b45
--- /dev/null
+++ b/wonderland/README.md
@@ -0,0 +1,66 @@
+## Foundry
+
+**Foundry is a blazing fast, portable and modular toolkit for Ethereum application development written in Rust.**
+
+Foundry consists of:
+
+-   **Forge**: Ethereum testing framework (like Truffle, Hardhat and DappTools).
+-   **Cast**: Swiss army knife for interacting with EVM smart contracts, sending transactions and getting chain data.
+-   **Anvil**: Local Ethereum node, akin to Ganache, Hardhat Network.
+-   **Chisel**: Fast, utilitarian, and verbose solidity REPL.
+
+## Documentation
+
+https://book.getfoundry.sh/
+
+## Usage
+
+### Build
+
+```shell
+$ forge build
+```
+
+### Test
+
+```shell
+$ forge test
+```
+
+### Format
+
+```shell
+$ forge fmt
+```
+
+### Gas Snapshots
+
+```shell
+$ forge snapshot
+```
+
+### Anvil
+
+```shell
+$ anvil
+```
+
+### Deploy
+
+```shell
+$ forge script script/Counter.s.sol:CounterScript --rpc-url <your_rpc_url> --private-key <your_private_key>
+```
+
+### Cast
+
+```shell
+$ cast <subcommand>
+```
+
+### Help
+
+```shell
+$ forge --help
+$ anvil --help
+$ cast --help
+```
diff --git a/wonderland/foundry.toml b/wonderland/foundry.toml
new file mode 100644
index 0000000..db9bb3b
--- /dev/null
+++ b/wonderland/foundry.toml
@@ -0,0 +1,8 @@
+[profile.default]
+src = "src"
+out = "out"
+libs = ["lib"]
+
+# See more config options https://github.com/foundry-rs/foundry/blob/master/crates/config/README.md#all-options
+
+extra_output = ['storageLayout']
diff --git a/wonderland/kontrol.toml b/wonderland/kontrol.toml
new file mode 100644
index 0000000..5a82ec9
--- /dev/null
+++ b/wonderland/kontrol.toml
@@ -0,0 +1,41 @@
+[build.default]
+foundry-project-root       = '.'
+regen                      = false
+rekompile                  = false
+verbose                    = false
+debug                      = false
+require                    = 'lemmas.k'
+module-import              = 'TestBase:KONTROL-LEMMAS'
+auxiliary-lemmas           = true
+
+[prove.default]
+foundry-project-root       = '.'
+verbose                    = false
+debug                      = false
+max-depth                  = 25000
+reinit                     = false
+cse                        = false
+workers                    = 4
+failure-information        = true
+counterexample-information = true
+minimize-proofs            = false
+fail-fast                  = true
+smt-timeout                = 1000
+break-every-step           = false
+break-on-jumpi             = false
+break-on-calls             = false
+break-on-storage           = false
+break-on-basic-blocks      = false
+break-on-cheatcodes        = false
+run-constructor            = false
+symbolic-immutables        = true
+
+[show.default]
+foundry-project-root       = '.'
+verbose                    = false
+debug                      = false
+use-hex-encoding           = false
+
+[view-kcfg.default]
+foundry-project-root       = '.'
+use-hex-encoding           = false
diff --git a/wonderland/lemmas.k b/wonderland/lemmas.k
new file mode 100644
index 0000000..1993151
--- /dev/null
+++ b/wonderland/lemmas.k
@@ -0,0 +1,14 @@
+requires "foundry.md"
+
+module KONTROL-LEMMAS
+
+// Your lemmas go here
+// Not sure what to do next? Try checking the documentation for writing lemmas: https://docs.runtimeverification.com/kontrol/guides/advancing-proofs/kevm-lemmas
+
+    imports FOUNDRY
+
+    /*
+    rule bool2Word ( X ) => 1 requires X         [simplification]
+    rule bool2Word ( X ) => 0 requires notBool X [simplification]
+    */
+endmodule
diff --git a/wonderland/lib/forge-std b/wonderland/lib/forge-std
new file mode 160000
index 0000000..1ce7535
--- /dev/null
+++ b/wonderland/lib/forge-std
@@ -0,0 +1 @@
+Subproject commit 1ce7535a517406b9aec7ea1ea27c1b41376f712c
diff --git a/wonderland/lib/kontrol-cheatcodes b/wonderland/lib/kontrol-cheatcodes
new file mode 160000
index 0000000..a5dd4b0
--- /dev/null
+++ b/wonderland/lib/kontrol-cheatcodes
@@ -0,0 +1 @@
+Subproject commit a5dd4b0b0f055fc628248d920cac5c9bcad6da4b
diff --git a/wonderland/src/Portal.sol b/wonderland/src/Portal.sol
new file mode 100644
index 0000000..e1dadcf
--- /dev/null
+++ b/wonderland/src/Portal.sol
@@ -0,0 +1,98 @@
+// SPDX-License-Identifier: MIT
+// (The MIT License)
+
+// Copyright 2020-2024 Optimism
+
+// Permission is hereby granted, free of charge, to any person obtaining
+// a copy of this software and associated documentation files (the
+// "Software"), to deal in the Software without restriction, including
+// without limitation the rights to use, copy, modify, merge, publish,
+// distribute, sublicense, and/or sell copies of the Software, and to
+// permit persons to whom the Software is furnished to do so, subject to
+// the following conditions:
+
+// The above copyright notice and this permission notice shall be
+// included in all copies or substantial portions of the Software.
+
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+// IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+// CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+// TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+// SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+
+pragma solidity ^0.8.13;
+
+library Types {
+    struct OutputRootProof {
+        bytes32 version;
+        bytes32 stateRoot;
+        bytes32 messagePasserStorageRoot;
+        bytes32 latestBlockhash;
+    }
+
+    struct WithdrawalTransaction {
+        uint256 nonce;
+        address sender;
+        address target;
+        uint256 value;
+        uint256 gasLimit;
+        bytes data;
+    }
+}
+
+// Adapted from https://github.com/ethereum-optimism/optimism
+contract Portal  {
+    bool public paused;
+    address public guardian;
+
+    /// @notice Emitted when a withdrawal transaction is proven.
+    event WithdrawalProven(address indexed from, address indexed to);
+
+    /// @notice Emitted when the conract is paused.
+    event Paused();
+
+    /// @notice Reverts when paused.
+    modifier whenNotPaused() {
+        require(paused == false, "Portal: paused");
+        _;
+    }
+
+    constructor() {
+        guardian = msg.sender;
+    }
+
+    /// @notice Pauses this contract.
+    function pause()
+        external
+        whenNotPaused
+    {
+        require(msg.sender == guardian, "Portal: not a guardian");
+        paused = true;
+        // Emit a `Paused` event.
+        emit Paused();
+    }
+
+    /// @notice Accepts ETH value without triggering a deposit to L2.
+    ///         This function mainly exists for the sake of the migration between the legacy
+    ///         Optimism system and Bedrock.
+    function donateETH() external payable {
+        // Intentionally empty.
+    }
+
+   /// @notice Proves a withdrawal transaction.
+    function proveWithdrawalTransaction(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+        whenNotPaused
+    {
+        // Implementation omitted
+        // Emit a `WithdrawalProven` event.
+        emit WithdrawalProven(_tx.sender, _tx.target);
+    }
+}
\ No newline at end of file
diff --git a/wonderland/src/TestToken.sol b/wonderland/src/TestToken.sol
new file mode 100644
index 0000000..c5064ab
--- /dev/null
+++ b/wonderland/src/TestToken.sol
@@ -0,0 +1,171 @@
+// SPDX-License-Identifier: MIT
+// Modified from OpenZeppelin Contracts (last updated v5.0.0) (token/ERC20/ERC20.sol)
+
+pragma solidity ^0.8.13;
+
+contract TestToken {
+    mapping(address account => uint256) private _balances;
+
+    mapping(address account => mapping(address spender => uint256)) private _allowances;
+
+    string private _name;
+    string private _symbol;
+    uint8 private immutable _decimals;
+    uint256 private _totalSupply;
+
+    // Added to illustrate access control checks
+    address guardian;
+    bool paused;
+
+    event Transfer(address indexed from, address indexed to, uint256 value);
+    event Approval(address indexed owner, address indexed spender, uint256 value);
+
+    error ERC20InsufficientBalance(address sender, uint256 balance, uint256 needed);
+    error ERC20InvalidReceiver(address receiver);
+    error ERC20InsufficientAllowance(address spender, uint256 allowance, uint256 needed);
+    error ERC20InvalidApprover(address approver);
+    error ERC20InvalidSpender(address spender);
+    error ERC20InvalidSender(address sender);
+
+    constructor(string memory name_, string memory symbol_, uint8 decimals_) {
+        _name = name_;
+        _symbol = symbol_;
+        _decimals = decimals_;
+
+        guardian = msg.sender;
+    }
+
+    function name() public view virtual returns (string memory) {
+        return _name;
+    }
+
+    function symbol() public view virtual returns (string memory) {
+        return _symbol;
+    }
+
+    function decimals() public view virtual returns (uint8) {
+        return _decimals;
+    }
+
+    function totalSupply() public view virtual returns (uint256) {
+        return _totalSupply;
+    }
+
+    function balanceOf(address account) public view virtual returns (uint256) {
+        return _balances[account];
+    }
+
+    function transfer(address to, uint256 value) public virtual returns (bool) {
+        address owner = msg.sender;
+        _transfer(owner, to, value);
+        return true;
+    }
+
+    function allowance(address owner, address spender) public view virtual returns (uint256) {
+        return _allowances[owner][spender];
+    }
+
+    function pause() public virtual {
+        require(msg.sender == guardian, "Only guardian can pause");
+        paused = true;
+    }
+
+    function approve(address spender, uint256 value) public virtual returns (bool) {
+        address owner = msg.sender;
+        _approve(owner, spender, value);
+        return true;
+    }
+
+    function transferFrom(address from, address to, uint256 value) public virtual returns (bool) {
+        address spender = msg.sender;
+        _spendAllowance(from, spender, value);
+        _transfer(from, to, value);
+        return true;
+    }
+
+    function _transfer(address from, address to, uint256 value) internal {
+        if (from == address(0)) {
+            revert ERC20InvalidSender(address(0));
+        }
+        if (to == address(0)) {
+            revert ERC20InvalidReceiver(address(0));
+        }
+        _update(from, to, value);
+    }
+
+
+    function _update(address from, address to, uint256 value) internal virtual {
+        if (from == address(0)) {
+            // Overflow check required: The rest of the code assumes that totalSupply never overflows
+            _totalSupply += value;
+        } else {
+            uint256 fromBalance = _balances[from];
+            if (fromBalance < value) {
+                revert ERC20InsufficientBalance(from, fromBalance, value);
+            }
+            unchecked {
+                // Overflow not possible: value <= fromBalance <= totalSupply.
+                _balances[from] = fromBalance - value;
+            }
+        }
+
+        if (to == address(0)) {
+            unchecked {
+                // Overflow not possible: value <= totalSupply or value <= fromBalance <= totalSupply.
+                _totalSupply -= value;
+            }
+        } else {
+            unchecked {
+                // Overflow not possible: balance + value is at most totalSupply, which we know fits into a uint256.
+                _balances[to] += value;
+            }
+        }
+
+        emit Transfer(from, to, value);
+    }
+
+    /*
+    function _mint(address account, uint256 value) internal {
+        if (account == address(0)) {
+            revert ERC20InvalidReceiver(address(0));
+        }
+        _update(address(0), account, value);
+    }
+
+    function _burn(address account, uint256 value) internal {
+        if (account == address(0)) {
+            revert ERC20InvalidSender(address(0));
+        }
+        _update(account, address(0), value);
+    }
+    */
+    
+    function _approve(address owner, address spender, uint256 value) internal {
+        _approve(owner, spender, value, true);
+    }
+
+    function _approve(address owner, address spender, uint256 value, bool emitEvent) internal virtual {
+        if (owner == address(0)) {
+            revert ERC20InvalidApprover(address(0));
+        }
+        if (spender == address(0)) {
+            revert ERC20InvalidSpender(address(0));
+        }
+        _allowances[owner][spender] = value;
+        if (emitEvent) {
+            emit Approval(owner, spender, value);
+        }
+    }
+
+    function _spendAllowance(address owner, address spender, uint256 value) internal virtual {
+        uint256 currentAllowance = allowance(owner, spender);
+        if (currentAllowance != type(uint256).max) {
+            if (currentAllowance < value) {
+                revert ERC20InsufficientAllowance(spender, currentAllowance, value);
+            }
+            unchecked {
+                _approve(owner, spender, currentAllowance - value, false);
+            }
+        }
+    }
+}
\ No newline at end of file
diff --git a/wonderland/test/Portal.t.sol b/wonderland/test/Portal.t.sol
new file mode 100644
index 0000000..2d32703
--- /dev/null
+++ b/wonderland/test/Portal.t.sol
@@ -0,0 +1,89 @@
+// SPDX-License-Identifier: MIT
+// Adapted from https://github.com/ethereum-optimism/optimism
+
+pragma solidity ^0.8.13;
+
+import "forge-std/Test.sol";
+import "kontrol-cheatcodes/KontrolCheats.sol";
+
+import "../src/Portal.sol";
+
+contract PortalTest is Test, KontrolCheats {
+    Portal portalContract;
+
+    function setUp() public {
+        portalContract = new Portal();
+    }
+
+    // Anyone can call donateETH successfully 
+    function test_donateETH(address sender, uint256 tokens) external
+    {
+        vm.assume(sender != address(this));
+        vm.assume(sender != address(vm));
+        vm.assume(sender != address(portalContract));
+
+        vm.prank(sender);
+
+        portalContract.donateETH{value: tokens}();
+    }
+
+    function test_donateETH(uint256 tokens, uint256 balance) external
+    {
+        address sender = kevm.freshAddress();       
+        vm.assume(sender != address(portalContract)); 
+
+        vm.deal(sender, balance);
+        vm.prank(sender);
+        portalContract.donateETH{value: tokens}();
+    }
+
+    function test_donateETH_successful(uint256 tokens, uint256 balance) external
+    {
+        address sender = kevm.freshAddress();       
+        vm.assume(sender != address(portalContract)); 
+
+        vm.deal(sender, balance);
+        vm.assume(balance >= tokens);
+        vm.prank(sender);
+        portalContract.donateETH{value: tokens}();
+    }
+
+    /// @custom:kontrol-array-length-equals _withdrawalProof: 2,
+    /// @custom:kontrol-bytes-length-equals _withdrawalProof: 32,
+    /// @custom:kontrol-bytes-length-equals data: 32,
+    function test_withdrawalPaused(
+        Types.WithdrawalTransaction calldata _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+    {
+        portalContract.pause();
+
+        vm.expectRevert();
+        portalContract.proveWithdrawalTransaction(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
+
+    /// @custom:kontrol-array-length-equals _withdrawalProof: 2,
+    /// @custom:kontrol-bytes-length-equals _withdrawalProof: 32,
+    /// @custom:kontrol-bytes-length-equals data: 32,
+    function test_withdrawal(
+        Types.WithdrawalTransaction calldata _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+    {
+        kevm.symbolicStorage(address(portalContract));
+
+        if (portalContract.paused())
+            vm.expectRevert();
+
+        portalContract.proveWithdrawalTransaction(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
+}
+
+
+
diff --git a/wonderland/test/TestToken.sol b/wonderland/test/TestToken.sol
new file mode 100644
index 0000000..f988348
--- /dev/null
+++ b/wonderland/test/TestToken.sol
@@ -0,0 +1,124 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.13;
+
+import {Test, console} from "forge-std/Test.sol";
+import {KontrolCheats} from "kontrol-cheatcodes/KontrolCheats.sol";
+import {TestToken} from "../src/TestToken.sol";
+
+contract TestTokenTest is Test, KontrolCheats {
+    TestToken public token;
+
+    /*
+    Should be executed with `kontrol prove --run-constructor`:
+    string tokenName = "TestToken";
+    */
+
+    function _notBuiltinOrPrecompiledAddress(address addr) internal view {
+        vm.assume(addr != address(vm));
+        vm.assume(addr != address(this));
+        vm.assume(addr != address(token));
+        vm.assume(uint256(uint160(addr)) == 0 || 9 < uint256(uint160(addr)));
+    }
+
+    function setUp() public {
+        uint8 decimals = freshUInt8();
+        token = new TestToken("TestToken", "TT", decimals);
+    }
+
+    function test_approve(address from, address to, uint256 amount) public {
+        // Overwrite the storage of the token contract with symbolic storage
+        kevm.symbolicStorage(address(token));
+
+        vm.assume(from != address(0));
+        vm.assume(to != address(0));
+        _notBuiltinOrPrecompiledAddress(from);
+        _notBuiltinOrPrecompiledAddress(to);
+
+        vm.prank(from);
+        token.approve(to, amount);
+
+        uint256 toAllowance = token.allowance(from, to);
+        assert(toAllowance == amount);
+    }
+
+    function test_pause(address from) public {
+        vm.assume(from != address(0));
+        _notBuiltinOrPrecompiledAddress(from);
+
+        /*
+        https://book.getfoundry.sh/cheatcodes/expect-revert:
+        After calling expectRevert, calls to other cheatcodes before the reverting call are ignored.
+        This means, for example, we can call prank immediately before the reverting call.
+        */
+        vm.prank(from);
+        vm.expectRevert();
+        token.pause();
+    }
+
+    function test_transfer(address from, address to, uint256 amount) public {
+        // Overwrite the storage of the token contract with symbolic storage
+        kevm.symbolicStorage(address(token));
+
+        _notBuiltinOrPrecompiledAddress(from);
+        _notBuiltinOrPrecompiledAddress(to);
+
+        // `from` and `to` are different, non-zero addresses
+        vm.assume(from != to);
+        /* 
+            This would cause branching:
+            vm.assume(from != address(0) && to != address(0));
+        */
+        vm.assume(from != address(0));
+        vm.assume(to != address(0));
+        
+        // `from` has enough tokens
+        vm.assume(amount <= token.balanceOf(from));
+        // no overflow occurs on transfer
+        unchecked {
+            vm.assume(token.balanceOf(to) <= token.balanceOf(to) + amount);
+            // vm.assume(token.balanceOf(to) + amount <= 2**256 - 1);
+        }
+
+        uint256 prev_from = token.balanceOf(from);
+        uint256 prev_to   = token.balanceOf(to);
+
+        vm.prank(from);
+        token.transfer(to, amount);
+
+        assertEq(token.balanceOf(from), prev_from - amount);
+        assertEq(token.balanceOf(to),   prev_to   + amount);
+    }
+
+function test_transfer_revertOnOverflow(address from, address to, uint256 amount) public {
+        // Overwrite the storage of the token contract with symbolic storage
+        kevm.symbolicStorage(address(token));
+
+        // Avoding vacuous nodes
+        vm.assume(from != address(0));
+        vm.assume(to != address(0));
+
+        _notBuiltinOrPrecompiledAddress(from);
+        _notBuiltinOrPrecompiledAddress(to);
+
+        // `from` and `to` are different, non-zero addresses
+        vm.assume(from != to);
+        
+        // `from` has enough tokens
+        vm.assume(amount <= token.balanceOf(from));
+        // no overflow occurs on transfer
+        // not wrapped in `unchecked`:
+        // unchecked {
+            vm.assume(token.balanceOf(to) <= token.balanceOf(to) + amount);
+            // vm.assume(token.balanceOf(to) + amount <= 2**256 - 1);
+        // }
+
+        uint256 prev_from = token.balanceOf(from);
+        uint256 prev_to   = token.balanceOf(to);
+
+        vm.prank(from);
+        token.transfer(to, amount);
+
+        assertEq(token.balanceOf(from), prev_from - amount);
+        assertEq(token.balanceOf(to),   prev_to   + amount);
+    }
+}
\ No newline at end of file
diff --git a/wonderland/test/mulWad.t.sol b/wonderland/test/mulWad.t.sol
new file mode 100644
index 0000000..ba38558
--- /dev/null
+++ b/wonderland/test/mulWad.t.sol
@@ -0,0 +1,46 @@
+pragma solidity ^0.8.13;
+
+import {Test, console} from "forge-std/Test.sol";
+
+/// @author Modified from Solady (https://github.com/vectorized/solady/blob/main/src/utils/FixedPointMathLib.sol)
+/// @author Modified from Solmate (https://github.com/transmissions11/solmate/blob/main/src/utils/FixedPointMathLib.sol)
+contract MulWadTest is Test {
+    /// @dev The scalar of ETH and most ERC20s.
+    uint256 internal constant WAD = 1e18;
+
+    /// @dev Equivalent to `(x * y) / WAD` rounded down.
+    // `mulWad` modified for illustration purposes
+    function modified_mulWad(uint256 x, uint256 y) public pure returns (uint256 z) {
+        /// @solidity memory-safe-assembly
+        assembly {
+            if or(mul(y, gt(x, div(not(0), y))), eq(x, 0xfffffffffff)) {
+                mstore(0x00, 0xbac65e5b) // `MulWadFailed()`.
+                revert(0x1c, 0x04)
+            }
+            z := div(mul(x, y), WAD)
+        }
+    }
+
+    /// @dev Equivalent to `(x * y) / WAD` rounded down.
+    function mulWad(uint256 x, uint256 y) public pure returns (uint256 z) {
+        /// @solidity memory-safe-assembly
+        assembly {
+            if mul(y, gt(x, div(not(0), y))) {
+                mstore(0x00, 0xbac65e5b) // `MulWadFailed()`.
+                revert(0x1c, 0x04)
+            }
+            z := div(mul(x, y), WAD)
+        }
+    }
+
+    function test_mulWad(uint256 x, uint256 y) public {
+        if (y == 0 || x <= type(uint256).max / y) {
+            uint256 zSpec = (x * y) / WAD;
+            uint256 zImpl = mulWad(x, y);
+            assert(zImpl == zSpec);
+        } else {
+            vm.expectRevert();
+            this.mulWad(x, y);
+        }
+    }
+}
\ No newline at end of file