Repository: pcaversaccio/snekmate (language: python)

Issue:
💥 Integrate 🐍 snekmate Contracts With Halmos
[Halmos](https://github.com/a16z/halmos) is a symbolic testing tool for EVM smart contracts. Solidity is currently offered by default, but Vyper support is added incrementally. Since we write all tests in Solidity (and is fully open-source), it integrates well with our test framework. Thus, we should use Halmos to formally verify 🐍 snekmate contracts.

## References

- https://github.com/a16z/halmos
- https://github.com/zobront/vyper-halmos


Discussion / hints:

Fix patch:
diff --git a/.gas-snapshot b/.gas-snapshot
index ce497e32..dd7d090c 100644
--- a/.gas-snapshot
+++ b/.gas-snapshot
@@ -4,12 +4,12 @@ AccessControlTest:testFuzzGrantRoleAdminRoleSuccess(address) (runs: 256, μ: 440
 AccessControlTest:testFuzzGrantRoleMultipleTimesSuccess(address) (runs: 256, μ: 49983, ~: 49983)
 AccessControlTest:testFuzzGrantRoleNonAdmin(address,address) (runs: 256, μ: 16471, ~: 16471)
 AccessControlTest:testFuzzGrantRoleSuccess(address) (runs: 256, μ: 44148, ~: 44148)
-AccessControlTest:testFuzzRenounceRoleMultipleTimesSuccess(address) (runs: 256, μ: 45997, ~: 45980)
+AccessControlTest:testFuzzRenounceRoleMultipleTimesSuccess(address) (runs: 256, μ: 45995, ~: 45980)
 AccessControlTest:testFuzzRenounceRoleNonMsgSender(address) (runs: 256, μ: 9483, ~: 9483)
-AccessControlTest:testFuzzRenounceRoleSuccess(address) (runs: 256, μ: 41954, ~: 41938)
-AccessControlTest:testFuzzRevokeRoleMultipleTimesSuccess(address) (runs: 256, μ: 41760, ~: 41744)
+AccessControlTest:testFuzzRenounceRoleSuccess(address) (runs: 256, μ: 41952, ~: 41938)
+AccessControlTest:testFuzzRevokeRoleMultipleTimesSuccess(address) (runs: 256, μ: 41758, ~: 41744)
 AccessControlTest:testFuzzRevokeRoleNonAdmin(address,address) (runs: 256, μ: 16425, ~: 16425)
-AccessControlTest:testFuzzRevokeRoleSuccess(address) (runs: 256, μ: 40592, ~: 40576)
+AccessControlTest:testFuzzRevokeRoleSuccess(address) (runs: 256, μ: 40590, ~: 40576)
 AccessControlTest:testFuzzSetRoleAdminPreviousAdminCallsGrantRole(address,address) (runs: 256, μ: 76002, ~: 76002)
 AccessControlTest:testFuzzSetRoleAdminPreviousAdminCallsRevokeRole(address,address) (runs: 256, μ: 101546, ~: 101546)
 AccessControlTest:testFuzzSetRoleAdminSuccess(address,address) (runs: 256, μ: 91046, ~: 91046)
@@ -48,8 +48,8 @@ Base64Test:testEncodeSingleCharacter() (gas: 173373)
 Base64Test:testEncodeWithDoublePadding() (gas: 178882)
 Base64Test:testEncodeWithNoPadding() (gas: 177869)
 Base64Test:testEncodeWithSinglePadding() (gas: 178985)
-BatchDistributorInvariants:statefulFuzzNoEtherBalance() (runs: 256, calls: 3840, reverts: 3826)
-BatchDistributorInvariants:statefulFuzzNoTokenBalance() (runs: 256, calls: 3840, reverts: 3826)
+BatchDistributorInvariants:statefulFuzzNoEtherBalance() (runs: 256, calls: 3840, reverts: 3821)
+BatchDistributorInvariants:statefulFuzzNoTokenBalance() (runs: 256, calls: 3840, reverts: 3821)
 BatchDistributorTest:testDistributeEtherMultipleAddressesSuccess() (gas: 135471)
 BatchDistributorTest:testDistributeEtherOneAddressSuccess() (gas: 61669)
 BatchDistributorTest:testDistributeEtherReentrancy() (gas: 1642700)
@@ -61,8 +61,8 @@ BatchDistributorTest:testDistributeTokenMultipleAddressesSuccess() (gas: 616682)
 BatchDistributorTest:testDistributeTokenOneAddressSuccess() (gas: 578787)
 BatchDistributorTest:testDistributeTokenRevertWithInsufficientAllowance() (gas: 573340)
 BatchDistributorTest:testDistributeTokenRevertWithInsufficientBalance() (gas: 573993)
-BatchDistributorTest:testFuzzDistributeEtherMultipleAddressesSuccess(((address,uint256)[]),uint256) (runs: 256, μ: 1838293, ~: 1785125)
-BatchDistributorTest:testFuzzDistributeTokenMultipleAddressesSuccess(((address,uint256)[]),address,uint256) (runs: 256, μ: 1316788, ~: 1279476)
+BatchDistributorTest:testFuzzDistributeEtherMultipleAddressesSuccess(((address,uint256)[]),uint256) (runs: 256, μ: 1890749, ~: 1855801)
+BatchDistributorTest:testFuzzDistributeTokenMultipleAddressesSuccess(((address,uint256)[]),address,uint256) (runs: 256, μ: 1291992, ~: 1294056)
 Create2AddressTest:testComputeAddress() (gas: 531976)
 Create2AddressTest:testComputeAddressSelf() (gas: 540703)
 Create2AddressTest:testFuzzComputeAddress(bytes32,address) (runs: 256, μ: 532571, ~: 532571)
@@ -88,30 +88,30 @@ CreateAddressTest:testComputeAddressSelfNonceUint56() (gas: 534722)
 CreateAddressTest:testComputeAddressSelfNonceUint64() (gas: 534830)
 CreateAddressTest:testComputeAddressSelfNonceUint8() (gas: 534449)
 CreateAddressTest:testComputeAddressSelfRevertTooHighNonce() (gas: 8899)
-CreateAddressTest:testFuzzComputeAddressNonce0x7f(uint64,address) (runs: 256, μ: 532982, ~: 533050)
-CreateAddressTest:testFuzzComputeAddressNonceUint16(uint64,address) (runs: 256, μ: 532363, ~: 532652)
-CreateAddressTest:testFuzzComputeAddressNonceUint24(uint64,address) (runs: 256, μ: 532545, ~: 532629)
-CreateAddressTest:testFuzzComputeAddressNonceUint32(uint64,address) (runs: 256, μ: 532533, ~: 532636)
-CreateAddressTest:testFuzzComputeAddressNonceUint40(uint64,address) (runs: 256, μ: 532660, ~: 532728)
-CreateAddressTest:testFuzzComputeAddressNonceUint48(uint64,address) (runs: 256, μ: 532649, ~: 532712)
-CreateAddressTest:testFuzzComputeAddressNonceUint56(uint64,address) (runs: 256, μ: 532660, ~: 532737)
-CreateAddressTest:testFuzzComputeAddressNonceUint64(uint64,address) (runs: 256, μ: 532738, ~: 532832)
-CreateAddressTest:testFuzzComputeAddressNonceUint8(uint64,address) (runs: 256, μ: 532455, ~: 532503)
-CreateAddressTest:testFuzzComputeAddressRevertTooHighNonce(uint256,address) (runs: 256, μ: 12870, ~: 13145)
-CreateAddressTest:testFuzzComputeAddressSelfNonce0x7f(uint64) (runs: 256, μ: 539230, ~: 539297)
-CreateAddressTest:testFuzzComputeAddressSelfNonceUint16(uint64) (runs: 256, μ: 538431, ~: 538725)
-CreateAddressTest:testFuzzComputeAddressSelfNonceUint24(uint64) (runs: 256, μ: 538712, ~: 538777)
-CreateAddressTest:testFuzzComputeAddressSelfNonceUint32(uint64) (runs: 256, μ: 538781, ~: 538873)
-CreateAddressTest:testFuzzComputeAddressSelfNonceUint40(uint64) (runs: 256, μ: 538778, ~: 538857)
-CreateAddressTest:testFuzzComputeAddressSelfNonceUint48(uint64) (runs: 256, μ: 538868, ~: 538931)
-CreateAddressTest:testFuzzComputeAddressSelfNonceUint56(uint64) (runs: 256, μ: 538929, ~: 538997)
-CreateAddressTest:testFuzzComputeAddressSelfNonceUint64(uint64) (runs: 256, μ: 539037, ~: 539118)
-CreateAddressTest:testFuzzComputeAddressSelfNonceUint8(uint64) (runs: 256, μ: 538520, ~: 538568)
-CreateAddressTest:testFuzzComputeAddressSelfRevertTooHighNonce(uint256) (runs: 256, μ: 12687, ~: 12618)
-ECDSATest:testFuzzRecoverWithInvalidSignature(bytes,string) (runs: 256, μ: 15356, ~: 15361)
-ECDSATest:testFuzzRecoverWithTooLongSignature(bytes,string) (runs: 256, μ: 13748, ~: 13751)
+CreateAddressTest:testFuzzComputeAddressNonce0x7f(uint64,address) (runs: 256, μ: 532980, ~: 533050)
+CreateAddressTest:testFuzzComputeAddressNonceUint16(uint64,address) (runs: 256, μ: 532392, ~: 532654)
+CreateAddressTest:testFuzzComputeAddressNonceUint24(uint64,address) (runs: 256, μ: 532563, ~: 532629)
+CreateAddressTest:testFuzzComputeAddressNonceUint32(uint64,address) (runs: 256, μ: 532519, ~: 532636)
+CreateAddressTest:testFuzzComputeAddressNonceUint40(uint64,address) (runs: 256, μ: 532643, ~: 532728)
+CreateAddressTest:testFuzzComputeAddressNonceUint48(uint64,address) (runs: 256, μ: 532632, ~: 532712)
+CreateAddressTest:testFuzzComputeAddressNonceUint56(uint64,address) (runs: 256, μ: 532652, ~: 532737)
+CreateAddressTest:testFuzzComputeAddressNonceUint64(uint64,address) (runs: 256, μ: 532739, ~: 532832)
+CreateAddressTest:testFuzzComputeAddressNonceUint8(uint64,address) (runs: 256, μ: 532449, ~: 532503)
+CreateAddressTest:testFuzzComputeAddressRevertTooHighNonce(uint256,address) (runs: 256, μ: 12839, ~: 13145)
+CreateAddressTest:testFuzzComputeAddressSelfNonce0x7f(uint64) (runs: 256, μ: 539222, ~: 539297)
+CreateAddressTest:testFuzzComputeAddressSelfNonceUint16(uint64) (runs: 256, μ: 538437, ~: 538725)
+CreateAddressTest:testFuzzComputeAddressSelfNonceUint24(uint64) (runs: 256, μ: 538705, ~: 538777)
+CreateAddressTest:testFuzzComputeAddressSelfNonceUint32(uint64) (runs: 256, μ: 538750, ~: 538873)
+CreateAddressTest:testFuzzComputeAddressSelfNonceUint40(uint64) (runs: 256, μ: 538774, ~: 538857)
+CreateAddressTest:testFuzzComputeAddressSelfNonceUint48(uint64) (runs: 256, μ: 538853, ~: 538931)
+CreateAddressTest:testFuzzComputeAddressSelfNonceUint56(uint64) (runs: 256, μ: 538946, ~: 538997)
+CreateAddressTest:testFuzzComputeAddressSelfNonceUint64(uint64) (runs: 256, μ: 539036, ~: 539118)
+CreateAddressTest:testFuzzComputeAddressSelfNonceUint8(uint64) (runs: 256, μ: 538515, ~: 538568)
+CreateAddressTest:testFuzzComputeAddressSelfRevertTooHighNonce(uint256) (runs: 256, μ: 12702, ~: 13020)
+ECDSATest:testFuzzRecoverWithInvalidSignature(bytes,string) (runs: 256, μ: 15357, ~: 15361)
+ECDSATest:testFuzzRecoverWithTooLongSignature(bytes,string) (runs: 256, μ: 13747, ~: 13751)
 ECDSATest:testFuzzRecoverWithValidSignature(string,string) (runs: 256, μ: 21685, ~: 21690)
-ECDSATest:testFuzzRecoverWithWrongMessage(string,string,bytes32) (runs: 256, μ: 21761, ~: 21760)
+ECDSATest:testFuzzRecoverWithWrongMessage(string,string,bytes32) (runs: 256, μ: 21760, ~: 21755)
 ECDSATest:testRecoverWith0x00Value() (gas: 14956)
 ECDSATest:testRecoverWithArbitraryMessage() (gas: 20662)
 ECDSATest:testRecoverWithCorrectVersion() (gas: 21116)
@@ -125,11 +125,11 @@ ECDSATest:testRecoverWithWrongVersion() (gas: 14962)
 EIP712DomainSeparatorTest:testCachedDomainSeparatorV4() (gas: 10476)
 EIP712DomainSeparatorTest:testDomainSeparatorV4() (gas: 11731)
 EIP712DomainSeparatorTest:testEIP712Domain() (gas: 18037)
-EIP712DomainSeparatorTest:testFuzzDomainSeparatorV4(uint8) (runs: 256, μ: 11884, ~: 11906)
-EIP712DomainSeparatorTest:testFuzzEIP712Domain(bytes1,uint8,bytes32,uint256[]) (runs: 256, μ: 21457, ~: 21524)
+EIP712DomainSeparatorTest:testFuzzDomainSeparatorV4(uint8) (runs: 256, μ: 11882, ~: 11906)
+EIP712DomainSeparatorTest:testFuzzEIP712Domain(bytes1,uint8,bytes32,uint256[]) (runs: 256, μ: 21479, ~: 21517)
 EIP712DomainSeparatorTest:testFuzzHashTypedDataV4(address,address,uint256,uint256,uint64) (runs: 256, μ: 10679, ~: 10679)
 EIP712DomainSeparatorTest:testHashTypedDataV4() (gas: 13167)
-ERC1155Invariants:statefulFuzzOwner() (runs: 256, calls: 3840, reverts: 3464)
+ERC1155Invariants:statefulFuzzOwner() (runs: 256, calls: 3840, reverts: 3480)
 ERC1155Test:testBalanceOfBatchCase1() (gas: 275438)
 ERC1155Test:testBalanceOfBatchCase2() (gas: 230030)
 ERC1155Test:testBalanceOfBatchCase3() (gas: 37418)
@@ -154,39 +154,39 @@ ERC1155Test:testExistsAfterBatchMint() (gas: 142296)
 ERC1155Test:testExistsAfterSingleBurn() (gas: 134886)
 ERC1155Test:testExistsAfterSingleMint() (gas: 116835)
 ERC1155Test:testExistsBeforeMint() (gas: 10481)
-ERC1155Test:testFuzzBurnBatchSuccess(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 131635, ~: 131625)
+ERC1155Test:testFuzzBurnBatchSuccess(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 131637, ~: 131636)
 ERC1155Test:testFuzzBurnSuccess(address,address,uint256) (runs: 256, μ: 137843, ~: 137853)
 ERC1155Test:testFuzzRenounceOwnershipNonOwner(address) (runs: 256, μ: 13962, ~: 13962)
-ERC1155Test:testFuzzRenounceOwnershipSuccess(address) (runs: 256, μ: 48760, ~: 48744)
-ERC1155Test:testFuzzSafeBatchTransferFromByApprovedOperator(address,address,address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 223955, ~: 223927)
-ERC1155Test:testFuzzSafeBatchTransferFromEOAReceiver(address,address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 188496, ~: 188467)
-ERC1155Test:testFuzzSafeBatchTransferFromNoData(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 557952, ~: 557962)
-ERC1155Test:testFuzzSafeBatchTransferFromWithData(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 558380, ~: 558664)
+ERC1155Test:testFuzzRenounceOwnershipSuccess(address) (runs: 256, μ: 48758, ~: 48744)
+ERC1155Test:testFuzzSafeBatchTransferFromByApprovedOperator(address,address,address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 223963, ~: 223927)
+ERC1155Test:testFuzzSafeBatchTransferFromEOAReceiver(address,address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 188497, ~: 188467)
+ERC1155Test:testFuzzSafeBatchTransferFromNoData(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 557962, ~: 557962)
+ERC1155Test:testFuzzSafeBatchTransferFromWithData(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 558323, ~: 558032)
 ERC1155Test:testFuzzSafeMintBatchEOAReceiver(address,address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 152105, ~: 152095)
-ERC1155Test:testFuzzSafeMintBatchNoData(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 515444, ~: 515454)
+ERC1155Test:testFuzzSafeMintBatchNoData(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 515454, ~: 515454)
 ERC1155Test:testFuzzSafeMintBatchNonMinter(address) (runs: 256, μ: 40642, ~: 40642)
-ERC1155Test:testFuzzSafeMintBatchWithData(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 515752, ~: 515910)
-ERC1155Test:testFuzzSafeMintEOAReceiver(address,address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 150179, ~: 150157)
-ERC1155Test:testFuzzSafeMintNoData(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 514468, ~: 514478)
+ERC1155Test:testFuzzSafeMintBatchWithData(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 515726, ~: 515569)
+ERC1155Test:testFuzzSafeMintEOAReceiver(address,address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 150180, ~: 150157)
+ERC1155Test:testFuzzSafeMintNoData(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 514478, ~: 514478)
 ERC1155Test:testFuzzSafeMintNonMinter(address) (runs: 256, μ: 32906, ~: 32906)
-ERC1155Test:testFuzzSafeMintWithData(address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 515620, ~: 515276)
-ERC1155Test:testFuzzSafeTransferFromByApprovedOperator(address,address,address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 202241, ~: 202204)
-ERC1155Test:testFuzzSafeTransferFromEOAReceiver(address,address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 166869, ~: 166831)
-ERC1155Test:testFuzzSafeTransferFromNoData(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 599394, ~: 599404)
-ERC1155Test:testFuzzSafeTransferFromWithData(address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 601446, ~: 600760)
-ERC1155Test:testFuzzSetApprovalForAllRevoke(address,address) (runs: 256, μ: 31971, ~: 31942)
+ERC1155Test:testFuzzSafeMintWithData(address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 515639, ~: 515276)
+ERC1155Test:testFuzzSafeTransferFromByApprovedOperator(address,address,address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 202250, ~: 202204)
+ERC1155Test:testFuzzSafeTransferFromEOAReceiver(address,address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 166871, ~: 166831)
+ERC1155Test:testFuzzSafeTransferFromNoData(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 599404, ~: 599404)
+ERC1155Test:testFuzzSafeTransferFromWithData(address,uint256,uint256,uint256,uint256,bytes) (runs: 256, μ: 601474, ~: 600760)
+ERC1155Test:testFuzzSetApprovalForAllRevoke(address,address) (runs: 256, μ: 31974, ~: 31942)
 ERC1155Test:testFuzzSetApprovalForAllSuccess(address,address) (runs: 256, μ: 45350, ~: 45350)
-ERC1155Test:testFuzzSetMinterNonOwner(address,string) (runs: 256, μ: 15510, ~: 15511)
+ERC1155Test:testFuzzSetMinterNonOwner(address,string) (runs: 256, μ: 15509, ~: 15499)
 ERC1155Test:testFuzzSetMinterSuccess(string) (runs: 256, μ: 33573, ~: 33584)
 ERC1155Test:testFuzzSetUriNonMinter(address) (runs: 256, μ: 14420, ~: 14420)
-ERC1155Test:testFuzzTotalSupplyAfterBatchBurn(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 125208, ~: 125198)
-ERC1155Test:testFuzzTotalSupplyAfterBatchMint(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 140221, ~: 140261)
-ERC1155Test:testFuzzTotalSupplyAfterSingleBurn(address,uint256,bytes) (runs: 256, μ: 134909, ~: 134880)
-ERC1155Test:testFuzzTotalSupplyAfterSingleMint(uint256,uint256,bytes) (runs: 256, μ: 87600, ~: 87641)
+ERC1155Test:testFuzzTotalSupplyAfterBatchBurn(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 125210, ~: 125209)
+ERC1155Test:testFuzzTotalSupplyAfterBatchMint(address,uint256,uint256,uint256,uint256) (runs: 256, μ: 140223, ~: 140192)
+ERC1155Test:testFuzzTotalSupplyAfterSingleBurn(address,uint256,bytes) (runs: 256, μ: 134918, ~: 134880)
+ERC1155Test:testFuzzTotalSupplyAfterSingleMint(uint256,uint256,bytes) (runs: 256, μ: 86894, ~: 57847)
 ERC1155Test:testFuzzTransferOwnershipNonOwner(address,address) (runs: 256, μ: 14071, ~: 14071)
-ERC1155Test:testFuzzTransferOwnershipSuccess(address,address) (runs: 256, μ: 75748, ~: 75719)
+ERC1155Test:testFuzzTransferOwnershipSuccess(address,address) (runs: 256, μ: 75751, ~: 75719)
 ERC1155Test:testHasOwner() (gas: 12614)
-ERC1155Test:testInitialSetup() (gas: 2784641)
+ERC1155Test:testInitialSetup() (gas: 2895175)
 ERC1155Test:testRenounceOwnershipNonOwner() (gas: 10903)
 ERC1155Test:testRenounceOwnershipSuccess() (gas: 22923)
 ERC1155Test:testSafeBatchTransferFromByApprovedOperator() (gas: 337520)
@@ -253,12 +253,12 @@ ERC1155Test:testTotalSupplyBeforeMint() (gas: 10460)
 ERC1155Test:testTransferOwnershipNonOwner() (gas: 12455)
 ERC1155Test:testTransferOwnershipSuccess() (gas: 53866)
 ERC1155Test:testTransferOwnershipToZeroAddress() (gas: 15610)
-ERC1155Test:testUriBaseAndTokenUriNotSet() (gas: 2743473)
+ERC1155Test:testUriBaseAndTokenUriNotSet() (gas: 2854007)
 ERC1155Test:testUriBaseAndTokenUriSet() (gas: 64201)
-ERC1155Test:testUriNoBaseURI() (gas: 2792872)
+ERC1155Test:testUriNoBaseURI() (gas: 2903406)
 ERC1155Test:testUriNoTokenUri() (gas: 18859)
-ERC20Invariants:statefulFuzzOwner() (runs: 256, calls: 3840, reverts: 3405)
-ERC20Invariants:statefulFuzzTotalSupply() (runs: 256, calls: 3840, reverts: 3405)
+ERC20Invariants:statefulFuzzOwner() (runs: 256, calls: 3840, reverts: 3482)
+ERC20Invariants:statefulFuzzTotalSupply() (runs: 256, calls: 3840, reverts: 3482)
 ERC20Test:testApproveExceedingBalanceCase1() (gas: 40805)
 ERC20Test:testApproveExceedingBalanceCase2() (gas: 47826)
 ERC20Test:testApproveFromZeroAddress() (gas: 12969)
@@ -280,29 +280,29 @@ ERC20Test:testBurnSuccessCase2() (gas: 31362)
 ERC20Test:testCachedDomainSeparator() (gas: 10601)
 ERC20Test:testDomainSeparator() (gas: 11831)
 ERC20Test:testEIP712Domain() (gas: 18191)
-ERC20Test:testFuzzApproveSuccess(address,uint256) (runs: 256, μ: 41125, ~: 41203)
-ERC20Test:testFuzzBurnFromInsufficientAllowance(address,uint256,uint8) (runs: 256, μ: 205994, ~: 206071)
-ERC20Test:testFuzzBurnFromSuccess(address,uint256) (runs: 256, μ: 339783, ~: 339652)
+ERC20Test:testFuzzApproveSuccess(address,uint256) (runs: 256, μ: 40736, ~: 41203)
+ERC20Test:testFuzzBurnFromInsufficientAllowance(address,uint256,uint8) (runs: 256, μ: 206197, ~: 206071)
+ERC20Test:testFuzzBurnFromSuccess(address,uint256) (runs: 256, μ: 339472, ~: 339652)
 ERC20Test:testFuzzBurnInvalidAmount(address,uint256) (runs: 256, μ: 16382, ~: 16382)
-ERC20Test:testFuzzBurnSuccessCase(uint256) (runs: 256, μ: 314380, ~: 314151)
-ERC20Test:testFuzzDomainSeparator(uint8) (runs: 256, μ: 12045, ~: 12067)
-ERC20Test:testFuzzEIP712Domain(bytes1,uint8,bytes32,uint256[]) (runs: 256, μ: 21712, ~: 21777)
-ERC20Test:testFuzzMintNonMinter(string,uint256) (runs: 256, μ: 12915, ~: 12916)
-ERC20Test:testFuzzMintSuccess(string,uint256) (runs: 256, μ: 55293, ~: 55531)
-ERC20Test:testFuzzPermitInvalid(string,string,uint16) (runs: 256, μ: 44588, ~: 44584)
-ERC20Test:testFuzzPermitSuccess(string,string,uint16) (runs: 256, μ: 70582, ~: 70584)
+ERC20Test:testFuzzBurnSuccessCase(uint256) (runs: 256, μ: 314364, ~: 314151)
+ERC20Test:testFuzzDomainSeparator(uint8) (runs: 256, μ: 12043, ~: 12067)
+ERC20Test:testFuzzEIP712Domain(bytes1,uint8,bytes32,uint256[]) (runs: 256, μ: 21730, ~: 21770)
+ERC20Test:testFuzzMintNonMinter(string,uint256) (runs: 256, μ: 12914, ~: 12916)
+ERC20Test:testFuzzMintSuccess(string,uint256) (runs: 256, μ: 55208, ~: 55532)
+ERC20Test:testFuzzPermitInvalid(string,string,uint16) (runs: 256, μ: 44591, ~: 44593)
+ERC20Test:testFuzzPermitSuccess(string,string,uint16) (runs: 256, μ: 70584, ~: 70584)
 ERC20Test:testFuzzRenounceOwnershipNonOwner(address) (runs: 256, μ: 13941, ~: 13941)
-ERC20Test:testFuzzRenounceOwnershipSuccess(address) (runs: 256, μ: 48670, ~: 48654)
-ERC20Test:testFuzzSetMinterNonOwner(address,string) (runs: 256, μ: 15519, ~: 15520)
+ERC20Test:testFuzzRenounceOwnershipSuccess(address) (runs: 256, μ: 48668, ~: 48654)
+ERC20Test:testFuzzSetMinterNonOwner(address,string) (runs: 256, μ: 15518, ~: 15508)
 ERC20Test:testFuzzSetMinterSuccess(string) (runs: 256, μ: 33594, ~: 33604)
-ERC20Test:testFuzzTransferFromInsufficientAllowance(address,address,uint256,uint8) (runs: 256, μ: 204418, ~: 204581)
-ERC20Test:testFuzzTransferFromSuccess(address,address,uint256) (runs: 256, μ: 234205, ~: 234156)
+ERC20Test:testFuzzTransferFromInsufficientAllowance(address,address,uint256,uint8) (runs: 256, μ: 204644, ~: 204581)
+ERC20Test:testFuzzTransferFromSuccess(address,address,uint256) (runs: 256, μ: 233937, ~: 234156)
 ERC20Test:testFuzzTransferInvalidAmount(address,address,uint256) (runs: 256, μ: 16762, ~: 16762)
 ERC20Test:testFuzzTransferOwnershipNonOwner(address,address) (runs: 256, μ: 14053, ~: 14053)
-ERC20Test:testFuzzTransferOwnershipSuccess(address,address) (runs: 256, μ: 75695, ~: 75665)
-ERC20Test:testFuzzTransferSuccess(address,uint256) (runs: 256, μ: 205588, ~: 205650)
+ERC20Test:testFuzzTransferOwnershipSuccess(address,address) (runs: 256, μ: 75696, ~: 75665)
+ERC20Test:testFuzzTransferSuccess(address,uint256) (runs: 256, μ: 205277, ~: 205648)
 ERC20Test:testHasOwner() (gas: 12658)
-ERC20Test:testInitialSetup() (gas: 1568990)
+ERC20Test:testInitialSetup() (gas: 1568253)
 ERC20Test:testMintNonMinter() (gas: 12464)
 ERC20Test:testMintOverflow() (gas: 16790)
 ERC20Test:testMintSuccess() (gas: 51814)
@@ -340,18 +340,18 @@ ERC2981Test:testDeleteDefaultRoyaltyNonOwner() (gas: 10651)
 ERC2981Test:testFuzzDeleteDefaultRoyaltyNonOwner(address) (runs: 256, μ: 13385, ~: 13385)
 ERC2981Test:testFuzzRenounceOwnershipNonOwner(address) (runs: 256, μ: 13935, ~: 13935)
 ERC2981Test:testFuzzRenounceOwnershipSuccess(address) (runs: 256, μ: 25266, ~: 25266)
-ERC2981Test:testFuzzResetTokenRoyalty(address,address,uint256,uint256,uint96,uint256) (runs: 256, μ: 96592, ~: 97794)
+ERC2981Test:testFuzzResetTokenRoyalty(address,address,uint256,uint256,uint96,uint256) (runs: 256, μ: 97082, ~: 97801)
 ERC2981Test:testFuzzResetTokenRoyaltyNonOwner(address) (runs: 256, μ: 13337, ~: 13337)
-ERC2981Test:testFuzzRoyaltyInfoDefaultRoyalty(address,uint256,uint256,uint96,uint256) (runs: 256, μ: 80625, ~: 81225)
-ERC2981Test:testFuzzRoyaltyInfoDeleteDefaultRoyalty(address,uint256,uint256,uint96,uint256) (runs: 256, μ: 65531, ~: 65956)
-ERC2981Test:testFuzzRoyaltyInfoSetTokenRoyalty(address,address,uint256,uint256,uint96,uint256) (runs: 256, μ: 121026, ~: 122709)
-ERC2981Test:testFuzzRoyaltyInfoSetTokenRoyaltyUpdate(address,address,uint256,uint256,uint96,uint256) (runs: 256, μ: 166952, ~: 169412)
-ERC2981Test:testFuzzRoyaltyInfoUpdateDefaultRoyalty(address,address,uint256,uint256,uint96,uint256) (runs: 256, μ: 88039, ~: 88945)
+ERC2981Test:testFuzzRoyaltyInfoDefaultRoyalty(address,uint256,uint256,uint96,uint256) (runs: 256, μ: 80858, ~: 81225)
+ERC2981Test:testFuzzRoyaltyInfoDeleteDefaultRoyalty(address,uint256,uint256,uint96,uint256) (runs: 256, μ: 65729, ~: 65970)
+ERC2981Test:testFuzzRoyaltyInfoSetTokenRoyalty(address,address,uint256,uint256,uint96,uint256) (runs: 256, μ: 121662, ~: 122709)
+ERC2981Test:testFuzzRoyaltyInfoSetTokenRoyaltyUpdate(address,address,uint256,uint256,uint96,uint256) (runs: 256, μ: 167898, ~: 169412)
+ERC2981Test:testFuzzRoyaltyInfoUpdateDefaultRoyalty(address,address,uint256,uint256,uint96,uint256) (runs: 256, μ: 88364, ~: 88945)
 ERC2981Test:testFuzzSetDefaultRoyaltyNonOwner(address) (runs: 256, μ: 15642, ~: 15642)
-ERC2981Test:testFuzzSetDefaultRoyaltyTooHighFeeNumerator(uint96) (runs: 256, μ: 21133, ~: 20916)
+ERC2981Test:testFuzzSetDefaultRoyaltyTooHighFeeNumerator(uint96) (runs: 256, μ: 21073, ~: 20916)
 ERC2981Test:testFuzzSetTokenRoyaltyInvalidReceiver(address) (runs: 256, μ: 18713, ~: 18713)
 ERC2981Test:testFuzzSetTokenRoyaltyNonOwner(address) (runs: 256, μ: 15659, ~: 15659)
-ERC2981Test:testFuzzSetTokenRoyaltyTooHighFeeNumerator(uint96) (runs: 256, μ: 21151, ~: 20934)
+ERC2981Test:testFuzzSetTokenRoyaltyTooHighFeeNumerator(uint96) (runs: 256, μ: 21091, ~: 20934)
 ERC2981Test:testFuzzTransferOwnershipNonOwner(address,address) (runs: 256, μ: 14002, ~: 14002)
 ERC2981Test:testFuzzTransferOwnershipSuccess(address,address) (runs: 256, μ: 30257, ~: 30257)
 ERC2981Test:testHasOwner() (gas: 12548)
@@ -379,8 +379,8 @@ ERC2981Test:testSupportsInterfaceSuccessGasCost() (gas: 9207)
 ERC2981Test:testTransferOwnershipNonOwner() (gas: 12383)
 ERC2981Test:testTransferOwnershipSuccess() (gas: 22202)
 ERC2981Test:testTransferOwnershipToZeroAddress() (gas: 15473)
-ERC4626VaultInvariants:statefulFuzzTotalAssets() (runs: 256, calls: 3840, reverts: 3336)
-ERC4626VaultInvariants:statefulFuzzTotalSupply() (runs: 256, calls: 3840, reverts: 3336)
+ERC4626VaultInvariants:statefulFuzzTotalAssets() (runs: 256, calls: 3840, reverts: 3307)
+ERC4626VaultInvariants:statefulFuzzTotalSupply() (runs: 256, calls: 3840, reverts: 3307)
 ERC4626VaultTest:testCachedDomainSeparator() (gas: 10578)
 ERC4626VaultTest:testDepositInsufficientAllowance() (gas: 82493)
 ERC4626VaultTest:testDepositWithNoApproval() (gas: 24428)
@@ -391,13 +391,13 @@ ERC4626VaultTest:testEmptyVaultDeposit() (gas: 567236)
 ERC4626VaultTest:testEmptyVaultMint() (gas: 568121)
 ERC4626VaultTest:testEmptyVaultRedeem() (gas: 202623)
 ERC4626VaultTest:testEmptyVaultwithdraw() (gas: 215356)
-ERC4626VaultTest:testFail_redeem((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 552560, ~: 556293)
-ERC4626VaultTest:testFail_withdraw((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 554402, ~: 557992)
-ERC4626VaultTest:testFuzzDomainSeparator(uint8) (runs: 256, μ: 11935, ~: 11959)
-ERC4626VaultTest:testFuzzEIP712Domain(bytes1,uint8,bytes32,uint256[]) (runs: 256, μ: 21644, ~: 21722)
-ERC4626VaultTest:testFuzzPermitInvalid(string,string,uint16) (runs: 256, μ: 44500, ~: 44496)
-ERC4626VaultTest:testFuzzPermitSuccess(string,string,uint16) (runs: 256, μ: 70436, ~: 70438)
-ERC4626VaultTest:testInitialSetup() (gas: 5954122)
+ERC4626VaultTest:testFail_redeem((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 553240, ~: 556206)
+ERC4626VaultTest:testFail_withdraw((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 554937, ~: 557992)
+ERC4626VaultTest:testFuzzDomainSeparator(uint8) (runs: 256, μ: 11937, ~: 11959)
+ERC4626VaultTest:testFuzzEIP712Domain(bytes1,uint8,bytes32,uint256[]) (runs: 256, μ: 21657, ~: 21696)
+ERC4626VaultTest:testFuzzPermitInvalid(string,string,uint16) (runs: 256, μ: 44503, ~: 44505)
+ERC4626VaultTest:testFuzzPermitSuccess(string,string,uint16) (runs: 256, μ: 70438, ~: 70438)
+ERC4626VaultTest:testInitialSetup() (gas: 5951716)
 ERC4626VaultTest:testMintWithNoApproval() (gas: 24474)
 ERC4626VaultTest:testMintZero() (gas: 41187)
 ERC4626VaultTest:testMultipleMintDepositRedeemWithdraw() (gas: 376838)
@@ -415,32 +415,32 @@ ERC4626VaultTest:testVaultInteractionsForSomeoneElse() (gas: 224101)
 ERC4626VaultTest:testWithdrawInsufficientAllowance() (gas: 122360)
 ERC4626VaultTest:testWithdrawInsufficientAssets() (gas: 117768)
 ERC4626VaultTest:testWithdrawWithNoAssets() (gas: 21289)
-ERC4626VaultTest:test_RT_deposit_redeem((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 472118, ~: 473112)
-ERC4626VaultTest:test_RT_deposit_withdraw((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 473849, ~: 474342)
-ERC4626VaultTest:test_RT_mint_redeem((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 472175, ~: 473185)
-ERC4626VaultTest:test_RT_mint_withdraw((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 473723, ~: 474487)
-ERC4626VaultTest:test_RT_redeem_deposit((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 472415, ~: 473165)
-ERC4626VaultTest:test_RT_redeem_mint((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 472312, ~: 473234)
-ERC4626VaultTest:test_RT_withdraw_deposit((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 473748, ~: 474372)
-ERC4626VaultTest:test_RT_withdraw_mint((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 473766, ~: 474478)
-ERC4626VaultTest:test_asset((address[4],uint256[4],uint256[4],int256)) (runs: 256, μ: 424533, ~: 426272)
-ERC4626VaultTest:test_convertToAssets((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 428451, ~: 430500)
-ERC4626VaultTest:test_convertToShares((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 428326, ~: 430518)
-ERC4626VaultTest:test_deposit((address[4],uint256[4],uint256[4],int256),uint256,uint256) (runs: 256, μ: 468410, ~: 471064)
-ERC4626VaultTest:test_maxDeposit((address[4],uint256[4],uint256[4],int256)) (runs: 256, μ: 424528, ~: 426266)
-ERC4626VaultTest:test_maxMint((address[4],uint256[4],uint256[4],int256)) (runs: 256, μ: 424552, ~: 426291)
-ERC4626VaultTest:test_maxRedeem((address[4],uint256[4],uint256[4],int256)) (runs: 256, μ: 424668, ~: 426406)
-ERC4626VaultTest:test_maxWithdraw((address[4],uint256[4],uint256[4],int256)) (runs: 256, μ: 426097, ~: 427641)
-ERC4626VaultTest:test_mint((address[4],uint256[4],uint256[4],int256),uint256,uint256) (runs: 256, μ: 468663, ~: 471186)
-ERC4626VaultTest:test_previewDeposit((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 464868, ~: 465740)
-ERC4626VaultTest:test_previewMint((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 465107, ~: 465920)
-ERC4626VaultTest:test_previewRedeem((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 466520, ~: 467176)
-ERC4626VaultTest:test_previewWithdraw((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 468127, ~: 468511)
-ERC4626VaultTest:test_redeem((address[4],uint256[4],uint256[4],int256),uint256,uint256) (runs: 256, μ: 471223, ~: 473797)
-ERC4626VaultTest:test_totalAssets((address[4],uint256[4],uint256[4],int256)) (runs: 256, μ: 425116, ~: 426855)
-ERC4626VaultTest:test_withdraw((address[4],uint256[4],uint256[4],int256),uint256,uint256) (runs: 256, μ: 473801, ~: 474990)
-ERC721Invariants:statefulFuzzOwner() (runs: 256, calls: 3840, reverts: 3493)
-ERC721Invariants:statefulFuzzTotalSupply() (runs: 256, calls: 3840, reverts: 3493)
+ERC4626VaultTest:test_RT_deposit_redeem((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 471827, ~: 473108)
+ERC4626VaultTest:test_RT_deposit_withdraw((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 473511, ~: 474335)
+ERC4626VaultTest:test_RT_mint_redeem((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 471989, ~: 473180)
+ERC4626VaultTest:test_RT_mint_withdraw((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 473693, ~: 474407)
+ERC4626VaultTest:test_RT_redeem_deposit((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 472258, ~: 473144)
+ERC4626VaultTest:test_RT_redeem_mint((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 472330, ~: 473228)
+ERC4626VaultTest:test_RT_withdraw_deposit((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 473598, ~: 474366)
+ERC4626VaultTest:test_RT_withdraw_mint((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 473948, ~: 474473)
+ERC4626VaultTest:test_asset((address[4],uint256[4],uint256[4],int256)) (runs: 256, μ: 423209, ~: 426272)
+ERC4626VaultTest:test_convertToAssets((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 428855, ~: 430497)
+ERC4626VaultTest:test_convertToShares((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 428782, ~: 430516)
+ERC4626VaultTest:test_deposit((address[4],uint256[4],uint256[4],int256),uint256,uint256) (runs: 256, μ: 469311, ~: 471063)
+ERC4626VaultTest:test_maxDeposit((address[4],uint256[4],uint256[4],int256)) (runs: 256, μ: 423203, ~: 426266)
+ERC4626VaultTest:test_maxMint((address[4],uint256[4],uint256[4],int256)) (runs: 256, μ: 423228, ~: 426291)
+ERC4626VaultTest:test_maxRedeem((address[4],uint256[4],uint256[4],int256)) (runs: 256, μ: 423343, ~: 426406)
+ERC4626VaultTest:test_maxWithdraw((address[4],uint256[4],uint256[4],int256)) (runs: 256, μ: 424777, ~: 427641)
+ERC4626VaultTest:test_mint((address[4],uint256[4],uint256[4],int256),uint256,uint256) (runs: 256, μ: 469187, ~: 471186)
+ERC4626VaultTest:test_previewDeposit((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 464580, ~: 465736)
+ERC4626VaultTest:test_previewMint((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 464924, ~: 465915)
+ERC4626VaultTest:test_previewRedeem((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 465335, ~: 467174)
+ERC4626VaultTest:test_previewWithdraw((address[4],uint256[4],uint256[4],int256),uint256) (runs: 256, μ: 467858, ~: 468483)
+ERC4626VaultTest:test_redeem((address[4],uint256[4],uint256[4],int256),uint256,uint256) (runs: 256, μ: 472841, ~: 473796)
+ERC4626VaultTest:test_totalAssets((address[4],uint256[4],uint256[4],int256)) (runs: 256, μ: 423793, ~: 426855)
+ERC4626VaultTest:test_withdraw((address[4],uint256[4],uint256[4],int256),uint256,uint256) (runs: 256, μ: 474557, ~: 474992)
+ERC721Invariants:statefulFuzzOwner() (runs: 256, calls: 3840, reverts: 3449)
+ERC721Invariants:statefulFuzzTotalSupply() (runs: 256, calls: 3840, reverts: 3449)
 ERC721Test:testApproveClearingApprovalWithNoPriorApproval() (gas: 177123)
 ERC721Test:testApproveClearingApprovalWithPriorApproval() (gas: 186025)
 ERC721Test:testApproveFromApprovedAddress() (gas: 198741)
@@ -460,36 +460,36 @@ ERC721Test:testBurnSuccessViaApproveAndSetApprovalForAll() (gas: 371431)
 ERC721Test:testCachedDomainSeparator() (gas: 10624)
 ERC721Test:testDomainSeparator() (gas: 11855)
 ERC721Test:testEIP712Domain() (gas: 18299)
-ERC721Test:testFuzzApproveClearingApprovalWithNoPriorApproval(address,address) (runs: 256, μ: 196800, ~: 196800)
-ERC721Test:testFuzzApproveClearingApprovalWithPriorApproval(address,address) (runs: 256, μ: 184459, ~: 184459)
+ERC721Test:testFuzzApproveClearingApprovalWithNoPriorApproval(address,address) (runs: 256, μ: 196790, ~: 196800)
+ERC721Test:testFuzzApproveClearingApprovalWithPriorApproval(address,address) (runs: 256, μ: 184449, ~: 184459)
 ERC721Test:testFuzzApproveFromNonOwner(address) (runs: 256, μ: 172095, ~: 172095)
 ERC721Test:testFuzzApproveFromOperatorAddress(address,address,address) (runs: 256, μ: 222944, ~: 222944)
-ERC721Test:testFuzzApproveWithNoPriorApproval(address,address) (runs: 256, μ: 196755, ~: 196755)
-ERC721Test:testFuzzApproveWithPriorApproval(address,address) (runs: 256, μ: 204271, ~: 204271)
-ERC721Test:testFuzzBurnSuccess(address) (runs: 256, μ: 305376, ~: 305360)
-ERC721Test:testFuzzDomainSeparator(uint8) (runs: 256, μ: 12045, ~: 12068)
-ERC721Test:testFuzzEIP712Domain(bytes1,uint8,bytes32,uint256[]) (runs: 256, μ: 21813, ~: 21848)
-ERC721Test:testFuzzGetApprovedApprovedTokenId(address,address) (runs: 256, μ: 194386, ~: 194386)
-ERC721Test:testFuzzPermitInvalid(string,string,uint16) (runs: 256, μ: 200611, ~: 200607)
-ERC721Test:testFuzzPermitSuccess(string,string,uint16) (runs: 256, μ: 227060, ~: 227062)
+ERC721Test:testFuzzApproveWithNoPriorApproval(address,address) (runs: 256, μ: 196745, ~: 196755)
+ERC721Test:testFuzzApproveWithPriorApproval(address,address) (runs: 256, μ: 204261, ~: 204271)
+ERC721Test:testFuzzBurnSuccess(address) (runs: 256, μ: 305367, ~: 305360)
+ERC721Test:testFuzzDomainSeparator(uint8) (runs: 256, μ: 12044, ~: 12068)
+ERC721Test:testFuzzEIP712Domain(bytes1,uint8,bytes32,uint256[]) (runs: 256, μ: 21834, ~: 21873)
+ERC721Test:testFuzzGetApprovedApprovedTokenId(address,address) (runs: 256, μ: 194376, ~: 194386)
+ERC721Test:testFuzzPermitInvalid(string,string,uint16) (runs: 256, μ: 200614, ~: 200616)
+ERC721Test:testFuzzPermitSuccess(string,string,uint16) (runs: 256, μ: 227062, ~: 227062)
 ERC721Test:testFuzzRenounceOwnershipNonOwner(address) (runs: 256, μ: 13923, ~: 13923)
-ERC721Test:testFuzzRenounceOwnershipSuccess(address) (runs: 256, μ: 48683, ~: 48667)
+ERC721Test:testFuzzRenounceOwnershipSuccess(address) (runs: 256, μ: 48681, ~: 48667)
 ERC721Test:testFuzzSafeMintNonMinter(address) (runs: 256, μ: 15704, ~: 15704)
-ERC721Test:testFuzzSafeMintSuccess(address[]) (runs: 256, μ: 20701993, ~: 19485926)
-ERC721Test:testFuzzSafeTransferFromWithData(address,address,address,bytes) (runs: 256, μ: 1432061, ~: 1432474)
+ERC721Test:testFuzzSafeMintSuccess(address[]) (runs: 256, μ: 20297614, ~: 17050171)
+ERC721Test:testFuzzSafeTransferFromWithData(address,address,address,bytes) (runs: 256, μ: 1432207, ~: 1432472)
 ERC721Test:testFuzzSetApprovalForAllSuccess(address,address) (runs: 256, μ: 189197, ~: 189197)
-ERC721Test:testFuzzSetMinterNonOwner(address,string) (runs: 256, μ: 15541, ~: 15542)
+ERC721Test:testFuzzSetMinterNonOwner(address,string) (runs: 256, μ: 15540, ~: 15530)
 ERC721Test:testFuzzSetMinterSuccess(string) (runs: 256, μ: 33649, ~: 33660)
-ERC721Test:testFuzzTokenByIndex(address,string[]) (runs: 256, μ: 22675247, ~: 23560031)
-ERC721Test:testFuzzTotalSupply(address,string[]) (runs: 256, μ: 22487414, ~: 23364180)
-ERC721Test:testFuzzTransferFrom(address,address,address) (runs: 256, μ: 564995, ~: 564978)
+ERC721Test:testFuzzTokenByIndex(address,string[]) (runs: 256, μ: 21709742, ~: 21415516)
+ERC721Test:testFuzzTotalSupply(address,string[]) (runs: 256, μ: 21529979, ~: 21239176)
+ERC721Test:testFuzzTransferFrom(address,address,address) (runs: 256, μ: 565001, ~: 564978)
 ERC721Test:testFuzzTransferOwnershipNonOwner(address,address) (runs: 256, μ: 14075, ~: 14075)
-ERC721Test:testFuzzTransferOwnershipSuccess(address,address) (runs: 256, μ: 75811, ~: 75782)
+ERC721Test:testFuzzTransferOwnershipSuccess(address,address) (runs: 256, μ: 75814, ~: 75782)
 ERC721Test:testGetApprovedApprovedTokenId() (gas: 193932)
 ERC721Test:testGetApprovedInvalidTokenId() (gas: 11082)
 ERC721Test:testGetApprovedNotApprovedTokenId() (gas: 170336)
 ERC721Test:testHasOwner() (gas: 12584)
-ERC721Test:testInitialSetup() (gas: 2510958)
+ERC721Test:testInitialSetup() (gas: 2510203)
 ERC721Test:testOwnerOf() (gas: 165977)
 ERC721Test:testOwnerOfInvalidTokenId() (gas: 11037)
 ERC721Test:testPermitBadChainId() (gas: 199381)
@@ -537,7 +537,7 @@ ERC721Test:testTokenOfOwnerByIndexReverts() (gas: 545726)
 ERC721Test:testTokenURIAfterBurning() (gas: 138552)
 ERC721Test:testTokenURIDefault() (gas: 168123)
 ERC721Test:testTokenURIInvalidTokenId() (gas: 13142)
-ERC721Test:testTokenURINoBaseURI() (gas: 2630371)
+ERC721Test:testTokenURINoBaseURI() (gas: 2629616)
 ERC721Test:testTokenURINoTokenUri() (gas: 125692)
 ERC721Test:testTotalSupply() (gas: 328195)
 ERC721Test:testTransferFrom() (gas: 574245)
@@ -547,19 +547,19 @@ ERC721Test:testTransferOwnershipToZeroAddress() (gas: 15546)
 MathTest:testCbrtRoundDown() (gas: 51656)
 MathTest:testCbrtRoundUp() (gas: 52303)
 MathTest:testCeilDiv() (gas: 14712)
-MathTest:testFuzzCbrt(uint256,bool) (runs: 256, μ: 22475, ~: 22395)
-MathTest:testFuzzCeilDiv(uint256,uint256) (runs: 256, μ: 9766, ~: 9770)
+MathTest:testFuzzCbrt(uint256,bool) (runs: 256, μ: 22310, ~: 22226)
+MathTest:testFuzzCeilDiv(uint256,uint256) (runs: 256, μ: 9765, ~: 9770)
 MathTest:testFuzzInt256Average(int256,int256) (runs: 256, μ: 8625, ~: 8625)
-MathTest:testFuzzLog10(uint256,bool) (runs: 256, μ: 10389, ~: 10325)
-MathTest:testFuzzLog2(uint256,bool) (runs: 256, μ: 10097, ~: 10048)
-MathTest:testFuzzLog256(uint256,bool) (runs: 256, μ: 10227, ~: 10146)
-MathTest:testFuzzMulDiv(uint256,uint256,uint256) (runs: 256, μ: 14393, ~: 14078)
-MathTest:testFuzzMulDivDomain(uint256,uint256,uint256) (runs: 256, μ: 10850, ~: 10890)
-MathTest:testFuzzSignum(int256) (runs: 256, μ: 8508, ~: 8500)
+MathTest:testFuzzLog10(uint256,bool) (runs: 256, μ: 10350, ~: 10307)
+MathTest:testFuzzLog2(uint256,bool) (runs: 256, μ: 10061, ~: 10030)
+MathTest:testFuzzLog256(uint256,bool) (runs: 256, μ: 10192, ~: 10119)
+MathTest:testFuzzMulDiv(uint256,uint256,uint256) (runs: 256, μ: 14329, ~: 14078)
+MathTest:testFuzzMulDivDomain(uint256,uint256,uint256) (runs: 256, μ: 10856, ~: 10890)
+MathTest:testFuzzSignum(int256) (runs: 256, μ: 8507, ~: 8500)
 MathTest:testFuzzUint256Average(uint256,uint256) (runs: 256, μ: 8688, ~: 8688)
-MathTest:testFuzzWadCbrt(uint256) (runs: 256, μ: 22264, ~: 21978)
-MathTest:testFuzzWadExp(int256) (runs: 256, μ: 14807, ~: 15098)
-MathTest:testFuzzWadLn(int256) (runs: 256, μ: 16383, ~: 16133)
+MathTest:testFuzzWadCbrt(uint256) (runs: 256, μ: 22260, ~: 22081)
+MathTest:testFuzzWadExp(int256) (runs: 256, μ: 14792, ~: 15098)
+MathTest:testFuzzWadLn(int256) (runs: 256, μ: 16383, ~: 16141)
 MathTest:testInt256Average() (gas: 18843)
 MathTest:testLog10RoundDown() (gas: 26211)
 MathTest:testLog10RoundUp() (gas: 27392)
@@ -580,8 +580,8 @@ MathTest:testWadExp() (gas: 34590)
 MathTest:testWadExpOverflow() (gas: 11169)
 MathTest:testWadLn() (gas: 31356)
 MathTest:testWadLnNegativeValues() (gas: 11096)
-MerkleProofVerificationTest:testFuzzMultiProofVerifySingleLeaf(bytes32[],uint256) (runs: 256, μ: 258218, ~: 254331)
-MerkleProofVerificationTest:testFuzzVerify(bytes32[],uint256) (runs: 256, μ: 172994, ~: 169014)
+MerkleProofVerificationTest:testFuzzMultiProofVerifySingleLeaf(bytes32[],uint256) (runs: 256, μ: 263268, ~: 263689)
+MerkleProofVerificationTest:testFuzzVerify(bytes32[],uint256) (runs: 256, μ: 177795, ~: 177454)
 MerkleProofVerificationTest:testFuzzVerifyMultiProofMultipleLeaves(bool,bool,bool) (runs: 256, μ: 45507, ~: 45498)
 MerkleProofVerificationTest:testInvalidMerkleMultiProof() (gas: 46737)
 MerkleProofVerificationTest:testInvalidMerkleProof() (gas: 18823)
@@ -594,8 +594,8 @@ MerkleProofVerificationTest:testMultiProofVerify() (gas: 50351)
 MerkleProofVerificationTest:testVerify() (gas: 35513)
 MessageHashUtilsTest:testEthSignedMessageHash() (gas: 8614)
 MessageHashUtilsTest:testFuzzEthSignedMessageHash(string) (runs: 256, μ: 9321, ~: 9315)
-MessageHashUtilsTest:testFuzzToDataWithIntendedValidatorHash(address,bytes) (runs: 256, μ: 9900, ~: 9885)
-MessageHashUtilsTest:testFuzzToDataWithIntendedValidatorHashSelf(bytes) (runs: 256, μ: 11889, ~: 11872)
+MessageHashUtilsTest:testFuzzToDataWithIntendedValidatorHash(address,bytes) (runs: 256, μ: 9901, ~: 9885)
+MessageHashUtilsTest:testFuzzToDataWithIntendedValidatorHashSelf(bytes) (runs: 256, μ: 11886, ~: 11872)
 MessageHashUtilsTest:testFuzzToTypedDataHash(string,string) (runs: 256, μ: 9948, ~: 9949)
 MessageHashUtilsTest:testToDataWithIntendedValidatorHash() (gas: 11129)
 MessageHashUtilsTest:testToDataWithIntendedValidatorHashSelf() (gas: 11747)
@@ -614,10 +614,10 @@ Ownable2StepInvariants:statefulFuzzPendingOwner() (runs: 256, calls: 3840, rever
 Ownable2StepTest:testAcceptOwnershipNonPendingOwner() (gas: 47364)
 Ownable2StepTest:testAcceptOwnershipSuccess() (gas: 40661)
 Ownable2StepTest:testFuzzAcceptOwnershipNonPendingOwner(address) (runs: 256, μ: 46803, ~: 46803)
-Ownable2StepTest:testFuzzAcceptOwnershipSuccess(address,address) (runs: 256, μ: 67717, ~: 67688)
-Ownable2StepTest:testFuzzPendingOwnerResetAfterRenounceOwnership(address) (runs: 256, μ: 40133, ~: 40117)
+Ownable2StepTest:testFuzzAcceptOwnershipSuccess(address,address) (runs: 256, μ: 67719, ~: 67688)
+Ownable2StepTest:testFuzzPendingOwnerResetAfterRenounceOwnership(address) (runs: 256, μ: 40131, ~: 40117)
 Ownable2StepTest:testFuzzRenounceOwnershipNonOwner(address) (runs: 256, μ: 13872, ~: 13872)
-Ownable2StepTest:testFuzzRenounceOwnershipSuccess(address) (runs: 256, μ: 45433, ~: 45417)
+Ownable2StepTest:testFuzzRenounceOwnershipSuccess(address) (runs: 256, μ: 45431, ~: 45417)
 Ownable2StepTest:testFuzzTransferOwnershipNonOwner(address,address) (runs: 256, μ: 14024, ~: 14024)
 Ownable2StepTest:testFuzzTransferOwnershipSuccess(address,address) (runs: 256, μ: 52221, ~: 52221)
 Ownable2StepTest:testHasOwner() (gas: 12527)
@@ -648,7 +648,7 @@ P256Test:testVerifyWithValidSignature() (gas: 554107)
 P256Test:testVerifyWithZeroInputs() (gas: 8654)
 P256Test:testVerifyWycheproofData() (gas: 230719221)
 SignatureCheckerTest:testEIP1271NoIsValidSignatureFunction() (gas: 18765)
-SignatureCheckerTest:testEIP1271WithInvalidSignature(bytes,string) (runs: 256, μ: 23593, ~: 23590)
+SignatureCheckerTest:testEIP1271WithInvalidSignature(bytes,string) (runs: 256, μ: 23595, ~: 23590)
 SignatureCheckerTest:testEIP1271WithInvalidSignature1() (gas: 29733)
 SignatureCheckerTest:testEIP1271WithInvalidSignature2() (gas: 31422)
 SignatureCheckerTest:testEIP1271WithInvalidSigner() (gas: 29811)
@@ -661,17 +661,17 @@ SignatureCheckerTest:testEOAWithTooHighSValue() (gas: 19974)
 SignatureCheckerTest:testEOAWithValidSignature() (gas: 19372)
 SignatureCheckerTest:testFuzzEIP1271WithInvalidSigner(string,string) (runs: 256, μ: 31652, ~: 31661)
 SignatureCheckerTest:testFuzzEIP1271WithValidSignature(string) (runs: 256, μ: 30299, ~: 30293)
-SignatureCheckerTest:testFuzzEOAWithInvalidSignature(bytes,string) (runs: 256, μ: 16382, ~: 16383)
+SignatureCheckerTest:testFuzzEOAWithInvalidSignature(bytes,string) (runs: 256, μ: 16383, ~: 16383)
 SignatureCheckerTest:testFuzzEOAWithInvalidSigner(string,string) (runs: 256, μ: 20404, ~: 20408)
 SignatureCheckerTest:testFuzzEOAWithValidSignature(string,string) (runs: 256, μ: 20314, ~: 20318)
 SignatureCheckerTest:testInitialSetup() (gas: 8292)
-TimelockControllerInvariants:statefulFuzzExecutedLessThanOrEqualToScheduled() (runs: 256, calls: 3840, reverts: 1241)
-TimelockControllerInvariants:statefulFuzzExecutedProposalCancellation() (runs: 256, calls: 3840, reverts: 1226)
-TimelockControllerInvariants:statefulFuzzExecutingCancelledProposal() (runs: 256, calls: 3840, reverts: 1258)
-TimelockControllerInvariants:statefulFuzzExecutingNotReadyProposal() (runs: 256, calls: 3840, reverts: 1237)
-TimelockControllerInvariants:statefulFuzzOnceProposalExecution() (runs: 256, calls: 3840, reverts: 1233)
-TimelockControllerInvariants:statefulFuzzProposalsExecutedMatchCount() (runs: 256, calls: 3840, reverts: 1241)
-TimelockControllerInvariants:statefulFuzzSumOfProposals() (runs: 256, calls: 3840, reverts: 1241)
+TimelockControllerInvariants:statefulFuzzExecutedLessThanOrEqualToScheduled() (runs: 256, calls: 3840, reverts: 1251)
+TimelockControllerInvariants:statefulFuzzExecutedProposalCancellation() (runs: 256, calls: 3840, reverts: 1250)
+TimelockControllerInvariants:statefulFuzzExecutingCancelledProposal() (runs: 256, calls: 3840, reverts: 1260)
+TimelockControllerInvariants:statefulFuzzExecutingNotReadyProposal() (runs: 256, calls: 3840, reverts: 1281)
+TimelockControllerInvariants:statefulFuzzOnceProposalExecution() (runs: 256, calls: 3840, reverts: 1281)
+TimelockControllerInvariants:statefulFuzzProposalsExecutedMatchCount() (runs: 256, calls: 3840, reverts: 1250)
+TimelockControllerInvariants:statefulFuzzSumOfProposals() (runs: 256, calls: 3840, reverts: 1249)
 TimelockControllerTest:testAdminCannotBatchExecute() (gas: 750675)
 TimelockControllerTest:testAdminCannotBatchSchedule() (gas: 748462)
 TimelockControllerTest:testAdminCannotCancel() (gas: 13375)
@@ -709,12 +709,12 @@ TimelockControllerTest:testExecutorCanExecute() (gas: 29504)
 TimelockControllerTest:testExecutorCannotBatchSchedule() (gas: 1485581)
 TimelockControllerTest:testExecutorCannotCancel() (gas: 15471)
 TimelockControllerTest:testExecutorCannotSchedule() (gas: 19169)
-TimelockControllerTest:testFuzzBatchValue(uint256) (runs: 256, μ: 4650565, ~: 4650302)
-TimelockControllerTest:testFuzzHashOperation(address,uint256,bytes,bytes32,bytes32) (runs: 256, μ: 10565, ~: 10545)
-TimelockControllerTest:testFuzzHashOperationBatch(address[],uint256[],bytes[],bytes32,bytes32) (runs: 256, μ: 1829506, ~: 1832547)
-TimelockControllerTest:testFuzzOperationValue(uint256) (runs: 256, μ: 111638, ~: 111375)
-TimelockControllerTest:testHandleERC1155() (gas: 41475555)
-TimelockControllerTest:testHandleERC721() (gas: 7158566)
+TimelockControllerTest:testFuzzBatchValue(uint256) (runs: 256, μ: 4650539, ~: 4650302)
+TimelockControllerTest:testFuzzHashOperation(address,uint256,bytes,bytes32,bytes32) (runs: 256, μ: 10568, ~: 10545)
+TimelockControllerTest:testFuzzHashOperationBatch(address[],uint256[],bytes[],bytes32,bytes32) (runs: 256, μ: 1829893, ~: 1828649)
+TimelockControllerTest:testFuzzOperationValue(uint256) (runs: 256, μ: 111612, ~: 111375)
+TimelockControllerTest:testHandleERC1155() (gas: 41586089)
+TimelockControllerTest:testHandleERC721() (gas: 7157811)
 TimelockControllerTest:testHashOperation() (gas: 12363)
 TimelockControllerTest:testHashOperationBatch() (gas: 1525346)
 TimelockControllerTest:testInitialSetup() (gas: 4297248)
diff --git a/.github/workflows/checks.yml b/.github/workflows/checks.yml
index 2882744f..e85d3054 100644
--- a/.github/workflows/checks.yml
+++ b/.github/workflows/checks.yml
@@ -3,7 +3,7 @@ name: 👮‍♂️ Sanity checks
 on: [push, pull_request, workflow_dispatch]
 
 concurrency:
-  group: ${{github.workflow}}-${{github.ref}}
+  group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
@@ -13,10 +13,10 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-        architecture:
-          - x64
         python_version:
           - 3.12
+        architecture:
+          - x64
         node_version:
           - 20
 
diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml
index d09b4784..389e5691 100644
--- a/.github/workflows/codeql.yml
+++ b/.github/workflows/codeql.yml
@@ -3,7 +3,7 @@ name: 🔍️ CodeQL
 on: [push, pull_request, workflow_dispatch]
 
 concurrency:
-  group: ${{github.workflow}}-${{github.ref}}
+  group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
@@ -35,4 +35,4 @@ jobs:
       - name: Perform CodeQL analysis
         uses: github/codeql-action/analyze@v3
         with:
-          category: "/language:${{matrix.language}}"
+          category: "/language:${{ matrix.language }}"
diff --git a/.github/workflows/halmos.yml b/.github/workflows/halmos.yml
new file mode 100644
index 00000000..570a8aae
--- /dev/null
+++ b/.github/workflows/halmos.yml
@@ -0,0 +1,87 @@
+name: 👁️ Halmos symbolic tests
+
+on:
+  schedule:
+    - cron: "30 3 * * *"
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  halmos-tests:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os:
+          - ubuntu-latest
+        python_version:
+          - 3.12
+        architecture:
+          - x64
+        halmos:
+          - "--function testHalmos --storage-layout generic --solver-command=yices-smt2 --solver-parallel --test-parallel --early-exit --ffi --statistics -v"
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Setup Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: ${{ matrix.python_version }}
+          architecture: ${{ matrix.architecture }}
+
+      - name: Install Vyper
+        run: pip install git+https://github.com/vyperlang/vyper.git@master
+
+      - name: Show the Vyper version
+        run: vyper --version
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
+
+      - name: Install `setuptools`
+        run: pip install setuptools
+
+      - name: Install Halmos
+        run: pip install git+https://github.com/a16z/halmos.git@main
+
+      - name: Show the Halmos version
+        run: halmos --version
+
+      - name: Install Homebrew
+        uses: Homebrew/actions/setup-homebrew@master
+
+      - name: Install Yices 2 SMT solver
+        run: brew install SRI-CSL/sri-csl/yices2
+
+      - name: Show the Foundry Halmos config
+        run: forge config
+        env:
+          FOUNDRY_PROFILE: halmos
+
+      - name: Run Halmos ERC-20 symbolic tests
+        run: halmos --contract ERC20TestHalmos ${{ matrix.halmos }}
+        env:
+          FOUNDRY_PROFILE: halmos
+
+      - name: Run Halmos ERC-721 symbolic tests
+        run: halmos --contract ERC721TestHalmos ${{ matrix.halmos }}
+        env:
+          FOUNDRY_PROFILE: halmos
+
+      - name: Run Halmos ERC-1155 symbolic tests
+        run: halmos --contract ERC1155TestHalmos ${{ matrix.halmos }}
+        env:
+          FOUNDRY_PROFILE: halmos
+
+      - name: Run Halmos math symbolic tests
+        run: halmos --contract MathTestHalmos ${{ matrix.halmos }}
+        env:
+          FOUNDRY_PROFILE: halmos
diff --git a/.github/workflows/publish-pypi.yml b/.github/workflows/publish-pypi.yml
index 6e72627f..fc177f3a 100644
--- a/.github/workflows/publish-pypi.yml
+++ b/.github/workflows/publish-pypi.yml
@@ -17,10 +17,10 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-        architecture:
-          - x64
         python_version:
           - 3.12
+        architecture:
+          - x64
 
     steps:
       - name: Checkout
diff --git a/.gitmodules b/.gitmodules
index 264c9614..f706870d 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -25,6 +25,9 @@
 [submodule "lib/FreshCryptoLib"]
 	path = lib/FreshCryptoLib
 	url = https://github.com/rdubois-crypto/FreshCryptoLib.git
+[submodule "lib/halmos-cheatcodes"]
+	path = lib/halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes.git
 [submodule "lib/solidity-bytes-utils"]
 	path = lib/solidity-bytes-utils
 	url = https://github.com/GNSPS/solidity-bytes-utils.git
diff --git a/.prettierignore b/.prettierignore
index 070d4f6e..612a610e 100644
--- a/.prettierignore
+++ b/.prettierignore
@@ -8,6 +8,7 @@ lib/properties
 lib/create-util
 lib/erc4626-tests
 lib/FreshCryptoLib
+lib/halmos-cheatcodes
 lib/solidity-bytes-utils
 lib/openzeppelin-contracts
 echidna-corpus
diff --git a/.solhintignore b/.solhintignore
index 070d4f6e..612a610e 100644
--- a/.solhintignore
+++ b/.solhintignore
@@ -8,6 +8,7 @@ lib/properties
 lib/create-util
 lib/erc4626-tests
 lib/FreshCryptoLib
+lib/halmos-cheatcodes
 lib/solidity-bytes-utils
 lib/openzeppelin-contracts
 echidna-corpus
diff --git a/CHANGELOG.md b/CHANGELOG.md
index db94dbd0..a74e9ad9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -36,8 +36,15 @@
 ### 🥢 Test Coverage
 
 - **Tokens**
-  - [`erc20`](https://github.com/pcaversaccio/snekmate/blob/v0.1.0/src/snekmate/tokens/erc20.vy): Add `echidna`-based `erc20` property tests. ([#239](https://github.com/pcaversaccio/snekmate/pull/239))
-  - [`erc721`](https://github.com/pcaversaccio/snekmate/blob/v0.1.0/src/snekmate/tokens/erc721.vy): Add `echidna`-based `erc721` property tests. ([#239](https://github.com/pcaversaccio/snekmate/pull/239))
+  - [`erc20`](https://github.com/pcaversaccio/snekmate/blob/v0.1.0/src/snekmate/tokens/erc20.vy):
+    - Add `echidna`-based `erc20` property tests. ([#239](https://github.com/pcaversaccio/snekmate/pull/239))
+    - Add `halmos`-based `erc20` symbolic tests. ([#240](https://github.com/pcaversaccio/snekmate/pull/240))
+  - [`erc721`](https://github.com/pcaversaccio/snekmate/blob/v0.1.0/src/snekmate/tokens/erc721.vy):
+    - Add `echidna`-based `erc721` property tests. ([#239](https://github.com/pcaversaccio/snekmate/pull/239))
+    - Add `halmos`-based `erc721` symbolic tests. ([#240](https://github.com/pcaversaccio/snekmate/pull/240))
+  - [`erc1155`](https://github.com/pcaversaccio/snekmate/blob/v0.1.0/src/snekmate/tokens/erc1155.vy): Add `halmos`-based `erc1155` symbolic tests. ([#240](https://github.com/pcaversaccio/snekmate/pull/240))
+- **Utility Functions**
+  - [`math`](https://github.com/pcaversaccio/snekmate/blob/v0.1.0/src/snekmate/utils/math.vy): Add `halmos`-based `math` symbolic tests. ([#240](https://github.com/pcaversaccio/snekmate/pull/240))
 
 ### ❗️ Breaking Changes
 
diff --git a/README.md b/README.md
index 7cb9e7b1..6d36a5e4 100644
--- a/README.md
+++ b/README.md
@@ -182,6 +182,22 @@ Furthermore, the [`echidna`](https://github.com/crytic/echidna)-based [property]
 ~$ FOUNDRY_PROFILE=echidna echidna test/tokens/echidna/ERC721Properties.sol --contract CryticERC721ExternalHarness --config test/tokens/echidna/echidna-config.yaml
 ```
 
+Eventually, the [`halmos`](https://github.com/a16z/halmos)-based symbolic tests for the [`erc20`](./src/snekmate/tokens/erc20.vy), [`erc721`](./src/snekmate/tokens/erc721.vy), [`erc1155`](./src/snekmate/tokens/erc1155.vy), and [`math`](./src/snekmate/utils/math.vy) contracts are available in the [`test/tokens/halmos/`](./test/tokens/halmos) and [`test/utils/halmos/`](./test/utils/halmos) directories. You can run the tests by invoking:
+
+```console
+# Run Halmos ERC-20 symbolic tests.
+~$ FOUNDRY_PROFILE=halmos halmos --contract ERC20TestHalmos --function testHalmos --storage-layout generic --ffi
+
+# Run Halmos ERC-721 symbolic tests. Be careful, this is a very time-consuming operation.
+~$ FOUNDRY_PROFILE=halmos halmos --contract ERC721TestHalmos --function testHalmos --storage-layout generic --ffi
+
+# Run Halmos ERC-1155 symbolic tests. Be careful, this is a very time-consuming operation.
+~$ FOUNDRY_PROFILE=halmos halmos --contract ERC1155TestHalmos --function testHalmos --storage-layout generic --ffi
+
+# Run Halmos math symbolic tests.
+~$ FOUNDRY_PROFILE=halmos halmos --contract MathTestHalmos --function testHalmos --storage-layout generic --ffi
+```
+
 > [!TIP]
 > If you encounter any issues, please ensure that you have the [latest](https://github.com/vyperlang/vyper/releases) Vyper version installed locally.
 
diff --git a/eslint.config.js b/eslint.config.js
index a55faeb9..44d1d9c1 100644
--- a/eslint.config.js
+++ b/eslint.config.js
@@ -23,6 +23,7 @@ module.exports = [
       "lib/create-util/**",
       "lib/erc4626-tests/**",
       "lib/FreshCryptoLib/**",
+      "lib/halmos-cheatcodes/**",
       "lib/solidity-bytes-utils/**",
       "lib/openzeppelin-contracts/**",
       "echidna-corpus/**",
diff --git a/foundry.toml b/foundry.toml
index 375103a5..9b396007 100644
--- a/foundry.toml
+++ b/foundry.toml
@@ -1,20 +1,20 @@
 ## defaults for all profiles
 [profile.default]
-src = 'src'                                                 # the source directory
-test = 'test'                                               # the test directory
-out = 'out'                                                 # the output directory (for artifacts)
-libs = ['lib']                                              # a list of library directories
+src = "src"                                                 # the source directory
+test = "test"                                               # the test directory
+out = "out"                                                 # the output directory (for artifacts)
+libs = ["lib"]                                              # a list of library directories
 cache = true                                                # whether to cache builds or not
-cache_path = 'cache'                                        # where the cache is stored if enabled
+cache_path = "cache"                                        # where the cache is stored if enabled
 force = false                                               # whether to ignore the cache (clean build)
 fuzz = { runs = 256 }                                       # the number of fuzz runs for tests
 invariant = { runs = 256 }                                  # the number of runs that must execute for each invariant test group
 ffi = true                                                  # whether to enable foreign function interface (ffi) cheatcodes or not
 verbosity = 3                                               # the verbosity of tests
-fs_permissions = [{ access = "read-write", path = "./"}]    # set read-write access to project root
-solc_version = '0.8.25'                                     # override for the solc version
-evm_version = 'cancun'                                      # set the EVM target version
-no_match_path = 'test/tokens/echidna/**/*'                  # only run tests in test directory that do not match the specified glob pattern
+fs_permissions = [{ access = "read-write", path = "./" }]   # set read-write access to project root
+solc_version = "0.8.25"                                     # override for the solc version
+evm_version = "cancun"                                      # set the EVM target version
+no_match_path = "test/**/{echidna,halmos}/**/*"             # only run tests in test directory that do not match the specified glob pattern
 
 ## default overrides for the CI runs
 [profile.ci]
@@ -26,4 +26,9 @@ verbosity = 4                                               # increase the verbo
 ## default overrides for the Echidna tests
 [profile.echidna]
 force = true                                                # always perform a clean build
-evm_version = 'shanghai'                                    # set the EVM target version to `shanghai`
+evm_version = "shanghai"                                    # set the EVM target version to `shanghai`
+
+## default overrides for the Halmos tests
+[profile.halmos]
+force = true                                                # always perform a clean build
+evm_version = "shanghai"                                    # set the EVM target version to `shanghai`
diff --git a/lib/halmos-cheatcodes b/lib/halmos-cheatcodes
new file mode 160000
index 00000000..c0d86550
--- /dev/null
+++ b/lib/halmos-cheatcodes
@@ -0,0 +1,1 @@
+Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5
diff --git a/lib/utils/VyperDeployer.sol b/lib/utils/VyperDeployer.sol
index 8863d3cb..4bb597ae 100644
--- a/lib/utils/VyperDeployer.sol
+++ b/lib/utils/VyperDeployer.sol
@@ -34,8 +34,8 @@ interface _CheatCodes {
  * https://github.com/0xKitsune/Foundry-Vyper/blob/main/lib/utils/VyperDeployer.sol.
  * @dev The Vyper Contract Deployer is a pre-built contract containing functions that
  * use a path, a filename, any ABI-encoded constructor arguments, and optionally the
- * target EVM version, and deploy the corresponding Vyper contract, returning the address
- * that the bytecode was deployed to.
+ * target EVM version and the compiler optimisation mode, and deploy the corresponding
+ * Vyper contract, returning the address that the bytecode was deployed to.
  */
 contract VyperDeployer is Create {
     address private constant HEVM_ADDRESS =
@@ -169,7 +169,7 @@ contract VyperDeployer is Create {
      * @dev Compiles a Vyper contract and returns the address that the contract
      * was deployed to. If the deployment fails, an error is thrown.
      * @notice Function overload of `deployContract` that allows the configuration
-     * of the target EVM version.
+     * of the target EVM version and the compiler optimisation mode.
      * @param path The directory path of the Vyper contract.
      * For example, the path of "utils" is "src/utils/".
      * @param fileName The file name of the Vyper contract.
@@ -177,24 +177,29 @@ contract VyperDeployer is Create {
      * @param evmVersion The EVM version used for compilation.
      * For example, the EVM version for the Cancun-Deneb hard fork is "cancun".
      * You can retrieve all available Vyper EVM versions by invoking `vyper -h`.
+     * @param optimiserMode The optimisation mode used for compilation.
+     * For example, the default optimisation mode since Vyper `0.3.10` is "gas".
+     * You can retrieve all available Vyper optimisation modes by invoking `vyper -h`.
      * @return deployedAddress The address that the contract was deployed to.
      */
     function deployContract(
         string calldata path,
         string calldata fileName,
         string calldata evmVersion,
-        bool /*overloadPlaceholder*/
+        string calldata optimiserMode
     ) public returns (address deployedAddress) {
         /**
          * @dev Create a list of strings with the commands necessary
          * to compile Vyper contracts.
          */
-        string[] memory cmds = new string[](5);
+        string[] memory cmds = new string[](7);
         cmds[0] = "python";
         cmds[1] = "lib/utils/compile.py";
         cmds[2] = string.concat(path, fileName, ".vy");
         cmds[3] = "--evm-version";
         cmds[4] = evmVersion;
+        cmds[5] = "--optimize";
+        cmds[6] = optimiserMode;
 
         /**
          * @dev Compile the Vyper contract and return the bytecode.
@@ -233,7 +238,7 @@ contract VyperDeployer is Create {
      * is thrown.
      * @notice Function overload of `deployContract`, which allows the passing of
      * any ABI-encoded constructor arguments and enables the configuration of the
-     * target EVM version.
+     * target EVM version and the compiler optimisation mode.
      * @param path The directory path of the Vyper contract.
      * For example, the path of "utils" is "src/utils/".
      * @param fileName The file name of the Vyper contract.
@@ -242,6 +247,9 @@ contract VyperDeployer is Create {
      * @param evmVersion The EVM version used for compilation.
      * For example, the EVM version for the Cancun-Deneb hard fork is "cancun".
      * You can retrieve all available Vyper EVM versions by invoking `vyper -h`.
+     * @param optimiserMode The optimisation mode used for compilation.
+     * For example, the default optimisation mode since Vyper `0.3.10` is "gas".
+     * You can retrieve all available Vyper optimisation modes by invoking `vyper -h`.
      * @return deployedAddress The address that the contract was deployed to.
      */
     function deployContract(
@@ -249,18 +257,20 @@ contract VyperDeployer is Create {
         string calldata fileName,
         bytes calldata args,
         string calldata evmVersion,
-        bool /*overloadPlaceholder*/
+        string calldata optimiserMode
     ) public returns (address deployedAddress) {
         /**
          * @dev Create a list of strings with the commands necessary
          * to compile Vyper contracts.
          */
-        string[] memory cmds = new string[](5);
+        string[] memory cmds = new string[](7);
         cmds[0] = "python";
         cmds[1] = "lib/utils/compile.py";
         cmds[2] = string.concat(path, fileName, ".vy");
         cmds[3] = "--evm-version";
         cmds[4] = evmVersion;
+        cmds[5] = "--optimize";
+        cmds[6] = optimiserMode;
 
         /**
          * @dev Compile the Vyper contract and return the bytecode.
diff --git a/pyproject.toml b/pyproject.toml
index cd8eb970..bd4c1862 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -2,15 +2,23 @@
 name = "snekmate"
 version = "0.0.5"
 description = "State-of-the-art, highly opinionated, hyper-optimised, and secure 🐍Vyper smart contract building blocks."
-readme = {file = "README.md", content-type = "text/markdown"}
+readme = { file = "README.md", content-type = "text/markdown" }
 requires-python = ">=3.10"
-license = {text = "AGPL-3.0-only License"}
-keywords = ["security", "library", "ethereum", "smart-contracts", "evm", "vyper", "vyper-contracts"]
+license = { text = "AGPL-3.0-only License" }
+keywords = [
+  "security",
+  "library",
+  "ethereum",
+  "smart-contracts",
+  "evm",
+  "vyper",
+  "vyper-contracts",
+]
 authors = [
-  {name = "Pascal Marco Caversaccio", email = "pascal.caversaccio@hotmail.ch"},
+  { name = "Pascal Marco Caversaccio", email = "pascal.caversaccio@hotmail.ch" },
 ]
 maintainers = [
-  {name = "Pascal Marco Caversaccio", email = "pascal.caversaccio@hotmail.ch"},
+  { name = "Pascal Marco Caversaccio", email = "pascal.caversaccio@hotmail.ch" },
 ]
 classifiers = [
   "Development Status :: 5 - Production/Stable",
diff --git a/remappings.txt b/remappings.txt
index 10734ff7..1bbd5456 100644
--- a/remappings.txt
+++ b/remappings.txt
@@ -7,6 +7,7 @@ forge-std/=lib/forge-std/src/
 erc4626-tests/=lib/erc4626-tests/
 properties/=lib/properties/contracts/
 create-util/=lib/create-util/contracts/
+halmos-cheatcodes/=lib/halmos-cheatcodes/src/
 fresh-crypto-lib=lib/FreshCryptoLib/solidity/src/
 openzeppelin/=lib/openzeppelin-contracts/contracts/
 solidity-bytes-utils/=lib/solidity-bytes-utils/contracts/
diff --git a/src/snekmate/tokens/mocks/erc1155_mock.vy b/src/snekmate/tokens/mocks/erc1155_mock.vy
index fa5763fb..07482836 100644
--- a/src/snekmate/tokens/mocks/erc1155_mock.vy
+++ b/src/snekmate/tokens/mocks/erc1155_mock.vy
@@ -89,3 +89,31 @@ def __init__(base_uri_: String[80]):
     # to the `msg.sender`.
     ow.__init__()
     erc1155.__init__(base_uri_)
+
+
+# @dev Custom implementation of the `external` function `safe_mint`
+# without access restriction and {IERC1155Receiver-onERC1155Received}
+# check to enable the Halmos tests for the no-backdoor and transfer
+# properties.
+@external
+def _customMint(owner: address, id: uint256, amount: uint256):
+    """
+    @dev Creates `amount` tokens of token type `id` and
+         transfers them to `owner`, increasing the total
+         supply.
+    @notice Note that `owner` cannot be the zero address.
+    @param owner The 20-byte owner address.
+    @param id The 32-byte identifier of the token.
+    @param amount The 32-byte token amount to be created.
+    """
+    assert owner != empty(address), "ERC1155Mock: mint to the zero address"
+
+    erc1155._before_token_transfer(empty(address), owner, erc1155._as_singleton_array(id), erc1155._as_singleton_array(amount), b"")
+
+    # In the next line, an overflow is not possible
+    # due to an arithmetic check of the entire token
+    # supply in the function `_before_token_transfer`.
+    erc1155.balanceOf[owner][id] = unsafe_add(erc1155.balanceOf[owner][id], amount)
+    log erc1155.TransferSingle(msg.sender, empty(address), owner, id, amount)
+
+    erc1155._after_token_transfer(empty(address), owner, erc1155._as_singleton_array(id), erc1155._as_singleton_array(amount), b"")


Test patch:
diff --git a/.github/workflows/publish-test-pypi.yml b/.github/workflows/publish-test-pypi.yml
index dc78923e..644f0b02 100644
--- a/.github/workflows/publish-test-pypi.yml
+++ b/.github/workflows/publish-test-pypi.yml
@@ -14,10 +14,10 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-        architecture:
-          - x64
         python_version:
           - 3.12
+        architecture:
+          - x64
 
     steps:
       - name: Checkout
diff --git a/.github/workflows/test-contracts.yml b/.github/workflows/test-contracts.yml
index 94215f5e..9d269965 100644
--- a/.github/workflows/test-contracts.yml
+++ b/.github/workflows/test-contracts.yml
@@ -3,7 +3,7 @@ name: 🕵️‍♂️ Test smart contracts
 on: [push, pull_request, workflow_dispatch]
 
 concurrency:
-  group: ${{github.workflow}}-${{github.ref}}
+  group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
@@ -13,12 +13,14 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-        architecture:
-          - x64
         python_version:
           - 3.12
+        architecture:
+          - x64
         node_version:
           - 20
+        echidna:
+          - "--config test/tokens/echidna/echidna-config.yaml"
 
     steps:
       - name: Checkout
@@ -118,13 +120,11 @@ jobs:
           FOUNDRY_PROFILE: echidna
 
       - name: Run Echidna ERC-20 property tests
-        run: |
-          echidna test/tokens/echidna/ERC20Properties.sol --contract CryticERC20ExternalHarness --config test/tokens/echidna/echidna-config.yaml
+        run: echidna test/tokens/echidna/ERC20Properties.sol --contract CryticERC20ExternalHarness ${{ matrix.echidna }}
         env:
           FOUNDRY_PROFILE: echidna
 
       - name: Run Echidna ERC-721 property tests
-        run: |
-          echidna test/tokens/echidna/ERC721Properties.sol --contract CryticERC721ExternalHarness --config test/tokens/echidna/echidna-config.yaml
+        run: echidna test/tokens/echidna/ERC721Properties.sol --contract CryticERC721ExternalHarness ${{ matrix.echidna }}
         env:
           FOUNDRY_PROFILE: echidna
diff --git a/test/tokens/echidna/ERC20Properties.sol b/test/tokens/echidna/ERC20Properties.sol
index 865ffbf2..07f11b88 100644
--- a/test/tokens/echidna/ERC20Properties.sol
+++ b/test/tokens/echidna/ERC20Properties.sol
@@ -43,7 +43,7 @@ contract CryticERC20ExternalHarness is
                 "erc20_mock",
                 args,
                 "shanghai",
-                true
+                "gas"
             )
         );
     }
diff --git a/test/tokens/echidna/ERC721Properties.sol b/test/tokens/echidna/ERC721Properties.sol
index c78515e0..9d67d721 100644
--- a/test/tokens/echidna/ERC721Properties.sol
+++ b/test/tokens/echidna/ERC721Properties.sol
@@ -42,7 +42,7 @@ contract CryticERC721ExternalHarness is
                 "erc721_mock",
                 args,
                 "shanghai",
-                true
+                "gas"
             )
         );
         mockSafeReceiver = new MockReceiver(true);
diff --git a/test/tokens/echidna/echidna-config.yaml b/test/tokens/echidna/echidna-config.yaml
index 3e1b60f0..4ea03639 100644
--- a/test/tokens/echidna/echidna-config.yaml
+++ b/test/tokens/echidna/echidna-config.yaml
@@ -10,8 +10,8 @@ filterFunctions: # Configure the list of methods to filter.
   [
     "VyperDeployer.deployContract(string,string)",
     "VyperDeployer.deployContract(string,string,bytes)",
-    "VyperDeployer.deployContract(string,string,string,bool)",
-    "VyperDeployer.deployContract(string,string,bytes,string,bool)",
+    "VyperDeployer.deployContract(string,string,string,string)",
+    "VyperDeployer.deployContract(string,string,bytes,string,string)",
   ]
 filterBlacklist: true # Blacklist methods in `filterFunctions`.
 cryticArgs: ["--ignore-compile"] # Disable compilation in `crytic-compile`.
diff --git a/test/tokens/halmos/ERC1155TestHalmos.t.sol b/test/tokens/halmos/ERC1155TestHalmos.t.sol
new file mode 100644
index 00000000..1d44c83e
--- /dev/null
+++ b/test/tokens/halmos/ERC1155TestHalmos.t.sol
@@ -0,0 +1,255 @@
+// SPDX-License-Identifier: WTFPL
+pragma solidity ^0.8.25;
+
+import {Test} from "forge-std/Test.sol";
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
+import {VyperDeployer} from "utils/VyperDeployer.sol";
+
+import {IERC1155} from "openzeppelin/token/ERC1155/IERC1155.sol";
+
+import {IERC1155Extended} from "../interfaces/IERC1155Extended.sol";
+
+/**
+ * @dev Sets the timeout (in milliseconds) for solving assertion
+ * violation conditions; `0` means no timeout.
+ * @notice Halmos currently does not support the new native `assert`
+ * cheatcodes in `forge-std` `v1.8.0` and above.
+ * @custom:halmos --solver-timeout-assertion 0
+ */
+contract ERC1155TestHalmos is Test, SymTest {
+    string private constant _BASE_URI = "https://www.wagmi.xyz/";
+
+    VyperDeployer private vyperDeployer = new VyperDeployer();
+
+    IERC1155 private erc1155;
+    address private token;
+    address[] private holders;
+    uint256[] private tokenIds;
+    uint256[] private amounts;
+
+    function setUp() public {
+        bytes memory args = abi.encode(_BASE_URI);
+        /**
+         * @dev Halmos does not currently work with the latest Vyper jump-table-based
+         * dispatchers: https://github.com/a16z/halmos/issues/253. For Halmos-based tests,
+         * we therefore disable the optimiser. Furthermore, Halmos does not currently
+         * work with the EVM version `cancun`: https://github.com/a16z/halmos/issues/290.
+         * For Halmos-based tests, we therefore use the EVM version `shanghai`.
+         */
+        erc1155 = IERC1155(
+            vyperDeployer.deployContract(
+                "src/snekmate/tokens/mocks/",
+                "erc1155_mock",
+                args,
+                "shanghai",
+                "none"
+            )
+        );
+
+        address deployer = address(vyperDeployer);
+        token = address(erc1155);
+        holders = new address[](3);
+        holders[0] = address(0x1337);
+        holders[1] = address(0x31337);
+        holders[2] = address(0xbA5eD);
+
+        tokenIds = new uint256[](5);
+        tokenIds[0] = 0;
+        tokenIds[1] = 1;
+        tokenIds[2] = 2;
+        tokenIds[3] = 3;
+        tokenIds[4] = 4;
+
+        amounts = new uint256[](5);
+        amounts[0] = 1;
+        amounts[1] = 2;
+        amounts[2] = 10;
+        amounts[3] = 20;
+        amounts[4] = 50;
+
+        vm.startPrank(deployer);
+        for (uint256 i = 0; i < tokenIds.length; i++) {
+            IERC1155Extended(token)._customMint(
+                deployer,
+                tokenIds[i],
+                amounts[i]
+            );
+        }
+        erc1155.safeTransferFrom(
+            deployer,
+            holders[0],
+            tokenIds[0],
+            amounts[0],
+            new bytes(0)
+        );
+        erc1155.safeTransferFrom(
+            deployer,
+            holders[0],
+            tokenIds[1],
+            amounts[1],
+            new bytes(42)
+        );
+        erc1155.safeTransferFrom(
+            deployer,
+            holders[1],
+            tokenIds[2],
+            amounts[2],
+            new bytes(96)
+        );
+        erc1155.safeTransferFrom(
+            deployer,
+            holders[2],
+            tokenIds[3],
+            amounts[3],
+            new bytes(1_024)
+        );
+        vm.stopPrank();
+
+        vm.startPrank(holders[0]);
+        erc1155.setApprovalForAll(holders[2], true);
+        vm.stopPrank();
+
+        vm.startPrank(holders[1]);
+        erc1155.setApprovalForAll(holders[2], true);
+        vm.stopPrank();
+    }
+
+    /**
+     * @dev Currently commented out due to performance and reverting path issues in Halmos.
+     */
+    // function testHalmosAssertNoBackdoor(
+    //     bytes4 selector,
+    //     address caller,
+    //     address other
+    // ) public {
+    //     /**
+    //      * @dev Using a single `assume` with conjunctions would result in the creation of
+    //      * multiple paths, negatively impacting performance.
+    //      */
+    //     vm.assume(caller != other);
+    //     vm.assume(selector != IERC1155Extended._customMint.selector);
+    //     vm.assume(selector != IERC1155Extended.safe_mint.selector);
+    //     vm.assume(selector != IERC1155Extended.safe_mint_batch.selector);
+    //     for (uint256 i = 0; i < holders.length; i++) {
+    //         vm.assume(!erc1155.isApprovedForAll(holders[i], caller));
+    //     }
+
+    //     address[] memory callers;
+    //     address[] memory others;
+    //     for (uint256 i = 0; i < tokenIds.length; i++) {
+    //         callers[i] = caller;
+    //         others[i] = other;
+    //     }
+
+    //     uint256[] memory oldBalanceCaller = erc1155.balanceOfBatch(
+    //         callers,
+    //         tokenIds
+    //     );
+    //     uint256[] memory oldBalanceOther = erc1155.balanceOfBatch(
+    //         others,
+    //         tokenIds
+    //     );
+
+    //     vm.startPrank(caller);
+    //     bool success;
+    //     if (selector == IERC1155.safeTransferFrom.selector) {
+    //         // solhint-disable-next-line avoid-low-level-calls
+    //         (success, ) = token.call(
+    //             abi.encodeWithSelector(
+    //                 selector,
+    //                 svm.createAddress("from"),
+    //                 svm.createAddress("to"),
+    //                 svm.createUint256("tokenId"),
+    //                 svm.createUint256("amount"),
+    //                 svm.createBytes(96, "YOLO")
+    //             )
+    //         );
+    //     } else if (selector == IERC1155.safeBatchTransferFrom.selector) {
+    //         uint256[] memory ids = new uint256[](5);
+    //         uint256[] memory values = new uint256[](5);
+    //         for (uint256 i = 0; i < ids.length; i++) {
+    //             ids[i] = svm.createUint256("ids");
+    //             values[i] = svm.createUint256("values");
+    //         }
+    //         // solhint-disable-next-line avoid-low-level-calls
+    //         (success, ) = token.call(
+    //             abi.encodeWithSelector(
+    //                 selector,
+    //                 svm.createAddress("from"),
+    //                 svm.createAddress("to"),
+    //                 ids,
+    //                 values,
+    //                 svm.createBytes(96, "YOLO")
+    //             )
+    //         );
+    //     } else {
+    //         bytes memory args = svm.createBytes(1_024, "WAGMI");
+    //         // solhint-disable-next-line avoid-low-level-calls
+    //         (success, ) = address(token).call(abi.encodePacked(selector, args));
+    //     }
+    //     vm.assume(success);
+    //     vm.stopPrank();
+
+    //     for (uint256 i = 0; i < tokenIds.length; i++) {
+    //         assert(
+    //             erc1155.balanceOf(caller, tokenIds[i]) <= oldBalanceCaller[i]
+    //         );
+    //         assert(erc1155.balanceOf(other, tokenIds[i]) >= oldBalanceOther[i]);
+    //     }
+    // }
+
+    function testHalmosSafeTransferFrom(
+        address caller,
+        address from,
+        address to,
+        address other
+    ) public {
+        /**
+         * @dev Using a single `assume` with conjunctions would result in the creation of
+         * multiple paths, negatively impacting performance.
+         */
+        vm.assume(other != from);
+        vm.assume(other != to);
+
+        uint256 oldBalanceFrom = erc1155.balanceOf(from, tokenIds[0]);
+        uint256 oldBalanceTo = erc1155.balanceOf(to, tokenIds[0]);
+        uint256 oldBalanceOther = erc1155.balanceOf(other, tokenIds[0]);
+        bool approved = erc1155.isApprovedForAll(from, caller);
+
+        vm.startPrank(caller);
+        if (svm.createBool("1337")) {
+            erc1155.safeTransferFrom(
+                from,
+                to,
+                tokenIds[0],
+                amounts[0],
+                svm.createBytes(96, "YOLO")
+            );
+        } else {
+            erc1155.safeBatchTransferFrom(
+                from,
+                to,
+                tokenIds,
+                amounts,
+                svm.createBytes(96, "YOLO")
+            );
+        }
+        vm.stopPrank();
+
+        (from == caller) ? assert(!approved) : assert(approved);
+
+        uint256 newBalanceFrom = erc1155.balanceOf(from, tokenIds[0]);
+        uint256 newBalanceTo = erc1155.balanceOf(to, tokenIds[0]);
+        uint256 newBalanceOther = erc1155.balanceOf(other, tokenIds[0]);
+
+        if (from != to) {
+            assert(newBalanceFrom == oldBalanceFrom - amounts[0]);
+            assert(newBalanceTo == oldBalanceTo + amounts[0]);
+        } else {
+            assert(newBalanceFrom == oldBalanceFrom);
+            assert(newBalanceTo == oldBalanceTo);
+        }
+
+        assert(newBalanceOther == oldBalanceOther);
+    }
+}
diff --git a/test/tokens/halmos/ERC20TestHalmos.t.sol b/test/tokens/halmos/ERC20TestHalmos.t.sol
new file mode 100644
index 00000000..cd451a94
--- /dev/null
+++ b/test/tokens/halmos/ERC20TestHalmos.t.sol
@@ -0,0 +1,201 @@
+// SPDX-License-Identifier: WTFPL
+pragma solidity ^0.8.25;
+
+import {Test} from "forge-std/Test.sol";
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
+import {VyperDeployer} from "utils/VyperDeployer.sol";
+
+import {IERC20} from "openzeppelin/token/ERC20/IERC20.sol";
+
+/**
+ * @dev Sets the timeout (in milliseconds) for solving assertion
+ * violation conditions; `0` means no timeout.
+ * @notice Halmos currently does not support the new native `assert`
+ * cheatcodes in `forge-std` `v1.8.0` and above.
+ * @custom:halmos --solver-timeout-assertion 0
+ */
+contract ERC20TestHalmos is Test, SymTest {
+    string private constant _NAME = "MyToken";
+    string private constant _SYMBOL = "WAGMI";
+    string private constant _NAME_EIP712 = "MyToken";
+    string private constant _VERSION_EIP712 = "1";
+
+    VyperDeployer private vyperDeployer = new VyperDeployer();
+
+    IERC20 private erc20;
+    address private token;
+    address[] private holders;
+
+    /**
+     * @dev Sets timeout (in milliseconds) for solving branching
+     * conditions; `0` means no timeout.
+     * @custom:halmos --solver-timeout-branching 1000
+     */
+    function setUpSymbolic(uint256 initialSupply_) public {
+        uint8 decimals = uint8(svm.createUint(8, "decimals"));
+        bytes memory args = abi.encode(
+            _NAME,
+            _SYMBOL,
+            decimals,
+            initialSupply_,
+            _NAME_EIP712,
+            _VERSION_EIP712
+        );
+        /**
+         * @dev Halmos does not currently work with the latest Vyper jump-table-based
+         * dispatchers: https://github.com/a16z/halmos/issues/253. For Halmos-based tests,
+         * we therefore disable the optimiser. Furthermore, Halmos does not currently
+         * work with the EVM version `cancun`: https://github.com/a16z/halmos/issues/290.
+         * For Halmos-based tests, we therefore use the EVM version `shanghai`.
+         */
+        erc20 = IERC20(
+            vyperDeployer.deployContract(
+                "src/snekmate/tokens/mocks/",
+                "erc20_mock",
+                args,
+                "shanghai",
+                "none"
+            )
+        );
+
+        address deployer = address(vyperDeployer);
+        token = address(erc20);
+        holders = new address[](3);
+        holders[0] = address(0x1337);
+        holders[1] = address(0x31337);
+        holders[2] = address(0xbA5eD);
+
+        for (uint256 i = 0; i < holders.length; i++) {
+            address account = holders[i];
+            uint256 balance = svm.createUint256("balance");
+            vm.assume(balance <= erc20.balanceOf(deployer));
+
+            vm.startPrank(deployer);
+            erc20.transfer(account, balance);
+            vm.stopPrank();
+
+            for (uint256 j = 0; j < i; j++) {
+                address other = holders[j];
+                uint256 amount = svm.createUint256("amount");
+                vm.startPrank(account);
+                erc20.approve(other, amount);
+                vm.stopPrank();
+            }
+        }
+    }
+
+    /**
+     * @notice Forked and adjusted accordingly from here:
+     * https://github.com/a16z/halmos/blob/main/examples/tokens/ERC20/test/ERC20Test.sol.
+     */
+    function testHalmosAssertNoBackdoor(
+        bytes4 selector,
+        address caller,
+        address other
+    ) public {
+        bytes memory args = svm.createBytes(1_024, "WAGMI");
+        vm.assume(other != caller);
+
+        uint256 oldBalanceOther = erc20.balanceOf(other);
+        uint256 oldAllowance = erc20.allowance(other, caller);
+
+        vm.startPrank(caller);
+        // solhint-disable-next-line avoid-low-level-calls
+        (bool success, ) = token.call(abi.encodePacked(selector, args));
+        vm.assume(success);
+        vm.stopPrank();
+
+        uint256 newBalanceOther = erc20.balanceOf(other);
+
+        if (newBalanceOther < oldBalanceOther) {
+            assert(oldAllowance >= oldBalanceOther - newBalanceOther);
+        }
+    }
+
+    /**
+     * @notice Forked and adjusted accordingly from here:
+     * https://github.com/a16z/halmos/blob/main/examples/tokens/ERC20/test/ERC20Test.sol.
+     */
+    function testHalmosTransfer(
+        address sender,
+        address receiver,
+        address other,
+        uint256 amount
+    ) public {
+        /**
+         * @dev Using a single `assume` with conjunctions would result in the creation of
+         * multiple paths, negatively impacting performance.
+         */
+        vm.assume(other != sender);
+        vm.assume(other != receiver);
+
+        uint256 oldBalanceSender = erc20.balanceOf(sender);
+        uint256 oldBalanceReceiver = erc20.balanceOf(receiver);
+        uint256 oldBalanceOther = erc20.balanceOf(other);
+
+        vm.startPrank(sender);
+        erc20.transfer(receiver, amount);
+        vm.stopPrank();
+
+        uint256 newBalanceSender = erc20.balanceOf(sender);
+        uint256 newBalanceReceiver = erc20.balanceOf(receiver);
+        uint256 newBalanceOther = erc20.balanceOf(other);
+
+        if (sender != receiver) {
+            assert(newBalanceSender == oldBalanceSender - amount);
+            assert(newBalanceReceiver == oldBalanceReceiver + amount);
+        } else {
+            assert(newBalanceSender == oldBalanceSender);
+            assert(newBalanceReceiver == oldBalanceReceiver);
+        }
+
+        assert(newBalanceOther == oldBalanceOther);
+    }
+
+    /**
+     * @notice Forked and adjusted accordingly from here:
+     * https://github.com/a16z/halmos/blob/main/examples/tokens/ERC20/test/ERC20Test.sol.
+     */
+    function testHalmosTransferFrom(
+        address caller,
+        address from,
+        address to,
+        address other,
+        uint256 amount
+    ) public {
+        /**
+         * @dev Using a single `assume` with conjunctions would result in the creation of
+         * multiple paths, negatively impacting performance.
+         */
+        vm.assume(other != from);
+        vm.assume(other != to);
+
+        uint256 oldBalanceFrom = erc20.balanceOf(from);
+        uint256 oldBalanceTo = erc20.balanceOf(to);
+        uint256 oldBalanceOther = erc20.balanceOf(other);
+        uint256 oldAllowance = erc20.allowance(from, caller);
+
+        vm.startPrank(caller);
+        erc20.transferFrom(from, to, amount);
+        vm.stopPrank();
+
+        uint256 newBalanceFrom = erc20.balanceOf(from);
+        uint256 newBalanceTo = erc20.balanceOf(to);
+        uint256 newBalanceOther = erc20.balanceOf(other);
+
+        if (from != to) {
+            assert(newBalanceFrom == oldBalanceFrom - amount);
+            assert(newBalanceTo == oldBalanceTo + amount);
+            assert(oldAllowance >= amount);
+            assert(
+                oldAllowance == type(uint256).max ||
+                    erc20.allowance(from, caller) == oldAllowance - amount
+            );
+        } else {
+            assert(newBalanceFrom == oldBalanceFrom);
+            assert(newBalanceTo == oldBalanceTo);
+        }
+
+        assert(newBalanceOther == oldBalanceOther);
+    }
+}
diff --git a/test/tokens/halmos/ERC721TestHalmos.t.sol b/test/tokens/halmos/ERC721TestHalmos.t.sol
new file mode 100644
index 00000000..870b0fe6
--- /dev/null
+++ b/test/tokens/halmos/ERC721TestHalmos.t.sol
@@ -0,0 +1,217 @@
+// SPDX-License-Identifier: WTFPL
+pragma solidity ^0.8.25;
+
+import {Test} from "forge-std/Test.sol";
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
+import {VyperDeployer} from "utils/VyperDeployer.sol";
+
+import {IERC721} from "openzeppelin/token/ERC721/IERC721.sol";
+
+import {IERC721Extended} from "../interfaces/IERC721Extended.sol";
+
+/**
+ * @dev Sets the timeout (in milliseconds) for solving assertion
+ * violation conditions; `0` means no timeout.
+ * @notice Halmos currently does not support the new native `assert`
+ * cheatcodes in `forge-std` `v1.8.0` and above.
+ * @custom:halmos --solver-timeout-assertion 0
+ */
+contract ERC721TestHalmos is Test, SymTest {
+    string private constant _NAME = "MyNFT";
+    string private constant _SYMBOL = "WAGMI";
+    string private constant _BASE_URI = "https://www.wagmi.xyz/";
+    string private constant _NAME_EIP712 = "MyNFT";
+    string private constant _VERSION_EIP712 = "1";
+
+    VyperDeployer private vyperDeployer = new VyperDeployer();
+
+    IERC721 private erc721;
+    address private token;
+    address[] private holders;
+    uint256[] private tokenIds;
+
+    /**
+     * @dev Sets timeout (in milliseconds) for solving branching
+     * conditions; `0` means no timeout.
+     * @custom:halmos --solver-timeout-branching 1000
+     */
+    function setUp() public {
+        bytes memory args = abi.encode(
+            _NAME,
+            _SYMBOL,
+            _BASE_URI,
+            _NAME_EIP712,
+            _VERSION_EIP712
+        );
+        /**
+         * @dev Halmos does not currently work with the latest Vyper jump-table-based
+         * dispatchers: https://github.com/a16z/halmos/issues/253. For Halmos-based tests,
+         * we therefore disable the optimiser. Furthermore, Halmos does not currently
+         * work with the EVM version `cancun`: https://github.com/a16z/halmos/issues/290.
+         * For Halmos-based tests, we therefore use the EVM version `shanghai`.
+         */
+        erc721 = IERC721(
+            vyperDeployer.deployContract(
+                "src/snekmate/tokens/mocks/",
+                "erc721_mock",
+                args,
+                "shanghai",
+                "none"
+            )
+        );
+
+        address deployer = address(vyperDeployer);
+        token = address(erc721);
+        holders = new address[](3);
+        holders[0] = address(0x1337);
+        holders[1] = address(0x31337);
+        holders[2] = address(0xbA5eD);
+
+        tokenIds = new uint256[](5);
+        tokenIds[0] = 0;
+        tokenIds[1] = 1;
+        tokenIds[2] = 2;
+        tokenIds[3] = 3;
+        tokenIds[4] = 4;
+
+        vm.startPrank(deployer);
+        for (uint256 i = 0; i < tokenIds.length; i++) {
+            IERC721Extended(token)._customMint(deployer, i);
+        }
+        erc721.transferFrom(deployer, holders[0], tokenIds[0]);
+        erc721.transferFrom(deployer, holders[0], tokenIds[1]);
+        erc721.transferFrom(deployer, holders[1], tokenIds[2]);
+        erc721.transferFrom(deployer, holders[2], tokenIds[3]);
+        vm.stopPrank();
+
+        vm.startPrank(holders[0]);
+        erc721.approve(holders[2], tokenIds[0]);
+        vm.stopPrank();
+
+        vm.startPrank(holders[1]);
+        erc721.setApprovalForAll(holders[2], true);
+        vm.stopPrank();
+    }
+
+    /**
+     * @dev Currently commented out due to performance and reverting path issues in Halmos.
+     * @notice Forked and adjusted accordingly from here:
+     * https://github.com/a16z/halmos/blob/main/examples/tokens/ERC721/test/ERC721Test.sol.
+     */
+    // function testHalmosAssertNoBackdoor(
+    //     bytes4 selector,
+    //     address caller,
+    //     address other
+    // ) public {
+    //     /**
+    //      * @dev Using a single `assume` with conjunctions would result in the creation of
+    //      * multiple paths, negatively impacting performance.
+    //      */
+    //     vm.assume(caller != other);
+    //     vm.assume(selector != IERC721Extended._customMint.selector);
+    //     vm.assume(selector != IERC721Extended.safe_mint.selector);
+    //     for (uint256 i = 0; i < holders.length; i++) {
+    //         vm.assume(!erc721.isApprovedForAll(holders[i], caller));
+    //     }
+    //     for (uint256 i = 0; i < tokenIds.length; i++) {
+    //         vm.assume(erc721.getApproved(tokenIds[i]) != caller);
+    //     }
+
+    //     uint256 oldBalanceCaller = erc721.balanceOf(caller);
+    //     uint256 oldBalanceOther = erc721.balanceOf(other);
+
+    //     vm.startPrank(caller);
+    //     bool success;
+    //     if (
+    //         selector ==
+    //         bytes4(keccak256("safeTransferFrom(address,address,uint256,bytes)"))
+    //     ) {
+    //         // solhint-disable-next-line avoid-low-level-calls
+    //         (success, ) = token.call(
+    //             abi.encodeWithSelector(
+    //                 selector,
+    //                 svm.createAddress("from"),
+    //                 svm.createAddress("to"),
+    //                 svm.createUint256("tokenId"),
+    //                 svm.createBytes(96, "YOLO")
+    //             )
+    //         );
+    //     } else {
+    //         bytes memory args = svm.createBytes(1_024, "WAGMI");
+    //         // solhint-disable-next-line avoid-low-level-calls
+    //         (success, ) = address(token).call(abi.encodePacked(selector, args));
+    //     }
+    //     vm.assume(success);
+    //     vm.stopPrank();
+
+    //     uint256 newBalanceCaller = erc721.balanceOf(caller);
+    //     uint256 newBalanceOther = erc721.balanceOf(other);
+
+    //     assert(newBalanceCaller <= oldBalanceCaller);
+    //     assert(newBalanceOther >= oldBalanceOther);
+    // }
+
+    /**
+     * @notice Forked and adjusted accordingly from here:
+     * https://github.com/a16z/halmos/blob/main/examples/tokens/ERC721/test/ERC721Test.sol.
+     */
+    function testHalmosSafeTransferFrom(
+        address caller,
+        address from,
+        address to,
+        address other,
+        uint256 tokenId,
+        uint256 otherTokenId
+    ) public {
+        /**
+         * @dev Using a single `assume` with conjunctions would result in the creation of
+         * multiple paths, negatively impacting performance.
+         */
+        vm.assume(other != from);
+        vm.assume(other != to);
+        vm.assume(otherTokenId != tokenId);
+
+        uint256 oldBalanceFrom = erc721.balanceOf(from);
+        uint256 oldBalanceTo = erc721.balanceOf(to);
+        uint256 oldBalanceOther = erc721.balanceOf(other);
+
+        address oldOwner = erc721.ownerOf(tokenId);
+        address oldOtherTokenOwner = erc721.ownerOf(otherTokenId);
+        bool approved = (caller == oldOwner ||
+            erc721.isApprovedForAll(oldOwner, caller) ||
+            erc721.getApproved(tokenId) == caller);
+
+        vm.startPrank(caller);
+        if (svm.createBool("1337")) {
+            erc721.transferFrom(from, to, tokenId);
+        } else {
+            erc721.safeTransferFrom(
+                from,
+                to,
+                tokenId,
+                svm.createBytes(96, "YOLO")
+            );
+        }
+        vm.stopPrank();
+
+        assert(from == oldOwner);
+        assert(approved);
+        assert(erc721.ownerOf(tokenId) == to);
+        assert(erc721.getApproved(tokenId) == address(0));
+        assert(erc721.ownerOf(otherTokenId) == oldOtherTokenOwner);
+
+        uint256 newBalanceFrom = erc721.balanceOf(from);
+        uint256 newBalanceTo = erc721.balanceOf(to);
+        uint256 newBalanceOther = erc721.balanceOf(other);
+
+        if (from != to) {
+            assert(newBalanceFrom == oldBalanceFrom - 1);
+            assert(newBalanceTo == oldBalanceTo + 1);
+        } else {
+            assert(newBalanceFrom == oldBalanceFrom);
+            assert(newBalanceTo == oldBalanceTo);
+        }
+
+        assert(newBalanceOther == oldBalanceOther);
+    }
+}
diff --git a/test/tokens/interfaces/IERC1155Extended.sol b/test/tokens/interfaces/IERC1155Extended.sol
index 806de8fd..d78e3e76 100644
--- a/test/tokens/interfaces/IERC1155Extended.sol
+++ b/test/tokens/interfaces/IERC1155Extended.sol
@@ -34,6 +34,8 @@ interface IERC1155Extended is IERC1155MetadataURI {
         bytes calldata data
     ) external;
 
+    function _customMint(address owner, uint256 id, uint256 amount) external;
+
     function safe_mint_batch(
         address owner,
         uint256[] calldata ids,
diff --git a/test/tokens/interfaces/IERC721Extended.sol b/test/tokens/interfaces/IERC721Extended.sol
index 61c63db0..43a3d507 100644
--- a/test/tokens/interfaces/IERC721Extended.sol
+++ b/test/tokens/interfaces/IERC721Extended.sol
@@ -27,6 +27,8 @@ interface IERC721Extended is
 
     function safe_mint(address owner, string calldata uri) external;
 
+    function _customMint(address owner, uint256 amount) external;
+
     function set_minter(address minter, bool status) external;
 
     function owner() external view returns (address);
diff --git a/test/utils/halmos/MathTestHalmos.t.sol b/test/utils/halmos/MathTestHalmos.t.sol
new file mode 100644
index 00000000..92aefe83
--- /dev/null
+++ b/test/utils/halmos/MathTestHalmos.t.sol
@@ -0,0 +1,158 @@
+// SPDX-License-Identifier: WTFPL
+pragma solidity ^0.8.25;
+
+import {Test} from "forge-std/Test.sol";
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
+import {VyperDeployer} from "utils/VyperDeployer.sol";
+
+import {Math} from "openzeppelin/utils/math/Math.sol";
+import {FixedPointMathLib} from "solady/utils/FixedPointMathLib.sol";
+
+import {IMath} from "../interfaces/IMath.sol";
+
+/**
+ * @dev Sets the timeout (in milliseconds) for solving assertion
+ * violation conditions; `0` means no timeout.
+ * @notice Halmos currently does not support the new native `assert`
+ * cheatcodes in `forge-std` `v1.8.0` and above.
+ * @custom:halmos --solver-timeout-assertion 0
+ */
+contract MathTestHalmos is Test, SymTest {
+    VyperDeployer private vyperDeployer = new VyperDeployer();
+
+    IMath private math;
+
+    /**
+     * @dev Sets timeout (in milliseconds) for solving branching
+     * conditions; `0` means no timeout.
+     * @custom:halmos --solver-timeout-branching 1000
+     */
+    function setUp() public {
+        /**
+         * @dev Halmos does not currently work with the latest Vyper jump-table-based
+         * dispatchers: https://github.com/a16z/halmos/issues/253. For Halmos-based tests,
+         * we therefore disable the optimiser. Furthermore, Halmos does not currently
+         * work with the EVM version `cancun`: https://github.com/a16z/halmos/issues/290.
+         * For Halmos-based tests, we therefore use the EVM version `shanghai`.
+         */
+        math = IMath(
+            vyperDeployer.deployContract(
+                "src/snekmate/utils/mocks/",
+                "math_mock",
+                "shanghai",
+                "none"
+            )
+        );
+    }
+
+    function testHalmosAssertUint256Average(uint256 x, uint256 y) public view {
+        assert(math.uint256_average(x, y) == Math.average(x, y));
+    }
+
+    function testHalmosAssertInt256Average(int256 x, int256 y) public view {
+        assert(math.int256_average(x, y) == FixedPointMathLib.avg(x, y));
+    }
+
+    function testHalmosAssertCeilDiv(uint256 x, uint256 y) public view {
+        assert(math.ceil_div(x, y) == Math.ceilDiv(x, y));
+    }
+
+    function testHalmosAssertSignum(int256 x) public view {
+        int256 signum;
+        // solhint-disable-next-line no-inline-assembly
+        assembly ("memory-safe") {
+            signum := sub(sgt(x, 0), slt(x, 0))
+        }
+        assert(math.signum(x) == signum);
+    }
+
+    /**
+     * @dev Currently commented out, as the timeout for the Z3 solver does not work for
+     * the queries of this test, where the Z3 solver is constantly running and consumes
+     * a lot of memory, causing the CI to crash due to out of memory.
+     */
+    // function testHalmosAssertMulDiv(
+    //     uint256 x,
+    //     uint256 y,
+    //     uint256 denominator,
+    //     Math.Rounding rounding
+    // ) public view {
+    //     assert(
+    //         math.mul_div(x, y, denominator, Math.unsignedRoundsUp(rounding)) ==
+    //             Math.mulDiv(x, y, denominator, rounding)
+    //     );
+    // }
+
+    function testHalmosAssertLog2(
+        uint256 x,
+        Math.Rounding rounding
+    ) public view {
+        assert(
+            math.log2(x, Math.unsignedRoundsUp(rounding)) ==
+                Math.log2(x, rounding)
+        );
+    }
+
+    function testHalmosAssertLog10(
+        uint256 x,
+        Math.Rounding rounding
+    ) public view {
+        assert(
+            math.log10(x, Math.unsignedRoundsUp(rounding)) ==
+                Math.log10(x, rounding)
+        );
+    }
+
+    function testHalmosAssertLog256(
+        uint256 x,
+        Math.Rounding rounding
+    ) public view {
+        assert(
+            math.log256(x, Math.unsignedRoundsUp(rounding)) ==
+                Math.log256(x, rounding)
+        );
+    }
+
+    /**
+     * @dev Currently commented out, as the timeout for the Z3 solver does not work for
+     * the queries of this test, where the Z3 solver is constantly running and consumes
+     * a lot of memory, causing the CI to crash due to out of memory.
+     */
+    // function testHalmosAssertWadLn(int256 x) public view {
+    //     assert(math.wad_ln(x) == FixedPointMathLib.lnWad(x));
+    // }
+
+    /**
+     * @dev Currently commented out, as the timeout for the Z3 solver does not work for
+     * the queries of this test, where the Z3 solver is constantly running and consumes
+     * a lot of memory, causing the CI to crash due to out of memory.
+     */
+    // function testHalmosAssertWadExp(int256 x) public view {
+    //     assert(math.wad_exp(x) == FixedPointMathLib.expWad(x));
+    // }
+
+    /**
+     * @dev Currently commented out, as the timeout for the Z3 solver does not work for
+     * the queries of this test, where the Z3 solver is constantly running and consumes
+     * a lot of memory, causing the CI to crash due to out of memory.
+     */
+    // function testHalmosAssertCbrt(uint256 x, bool roundup) public view {
+    //     if (!roundup) {
+    //         assert(math.cbrt(x, roundup) == FixedPointMathLib.cbrt(x));
+    //     } else {
+    //         assert(
+    //             math.cbrt(x, roundup) >= FixedPointMathLib.cbrt(x) &&
+    //                 math.cbrt(x, roundup) <= FixedPointMathLib.cbrt(x) + 1
+    //         );
+    //     }
+    // }
+
+    /**
+     * @dev Currently commented out, as the timeout for the Z3 solver does not work for
+     * the queries of this test, where the Z3 solver is constantly running and consumes
+     * a lot of memory, causing the CI to crash due to out of memory.
+     */
+    // function testHalmosAssertWadCbrt(uint256 x) public view {
+    //     assert(math.wad_cbrt(x) == FixedPointMathLib.cbrtWad(x));
+    // }
+}