diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index da16f1ed4..749f6df7b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -98,38 +98,6 @@ jobs:
       - name: Check unused imports
         run: python3 script/utils/fix_imports.py --check-unused
 
-  # halmos:
-  #   runs-on: ubuntu-latest
-
-  #   steps:
-  #     - name: Checkout
-  #       uses: actions/checkout@v4
-  #       with:
-  #         submodules: recursive
-
-  #     - name: Setup Python
-  #       uses: actions/setup-python@v5
-  #       with:
-  #         python-version: 3.13
-  #         architecture: x64
-
-  #     - 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: Run Halmos symbolic tests
-  #       run: halmos --contract TestMessageLibIdentities --function test
-
   anvil-deploy:
     runs-on: ubuntu-latest
     permissions:
diff --git a/script/fv.yml b/script/fv.yml
new file mode 100644
index 000000000..c5f9a5635
--- /dev/null
+++ b/script/fv.yml
@@ -0,0 +1,43 @@
+name: "FV"
+
+on:
+  push:
+    paths:
+      - src/misc/libraries/**
+      - test/misc/unit/libraries/**
+
+env:
+  FOUNDRY_PROFILE: ci
+
+jobs:
+  halmos:
+    runs-on: ubuntu-latest
+    
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Setup Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: 3.13
+          architecture: x64
+
+      - 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: Run Halmos symbolic tests
+        run: halmos --match-test '^symbolic|^testSymbolic' -vv
diff --git a/test/common/unit/libraries/MessageLib.t.sol b/test/common/unit/libraries/MessageLib.t.sol
index 348c6d971..aa16b2f66 100644
--- a/test/common/unit/libraries/MessageLib.t.sol
+++ b/test/common/unit/libraries/MessageLib.t.sol
@@ -151,7 +151,7 @@ contract TestMessageLibIds is Test {
 contract TestMessageLibIdentities is Test {
     using MessageLib for *;
 
-    function testScheduleUpgrade(bytes32 target) public pure {
+    function testSymbolicScheduleUpgrade(bytes32 target) public pure {
         MessageLib.ScheduleUpgrade memory a = MessageLib.ScheduleUpgrade({target: target});
         MessageLib.ScheduleUpgrade memory b = MessageLib.deserializeScheduleUpgrade(a.serialize());
 
@@ -161,7 +161,7 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), 0);
     }
 
-    function testCancelUpgrade(bytes32 target) public pure {
+    function testSymbolicCancelUpgrade(bytes32 target) public pure {
         MessageLib.CancelUpgrade memory a = MessageLib.CancelUpgrade({target: target});
         MessageLib.CancelUpgrade memory b = MessageLib.deserializeCancelUpgrade(a.serialize());
 
@@ -171,7 +171,7 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), 0);
     }
 
-    function testRecoverTokens(bytes32 target, bytes32 token, uint256 tokenId, bytes32 to, uint256 amount)
+    function testSymbolicRecoverTokens(bytes32 target, bytes32 token, uint256 tokenId, bytes32 to, uint256 amount)
         public
         pure
     {
@@ -189,7 +189,7 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), 0);
     }
 
-    function testRegisterAsset(uint128 assetId, uint8 decimals) public pure {
+    function testSymbolicRegisterAsset(uint128 assetId, uint8 decimals) public pure {
         MessageLib.RegisterAsset memory a = MessageLib.RegisterAsset({assetId: assetId, decimals: decimals});
         MessageLib.RegisterAsset memory b = MessageLib.deserializeRegisterAsset(a.serialize());
 
@@ -200,7 +200,7 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), AssetId.wrap(assetId).centrifugeId());
     }
 
-    function testNotifyPool(uint64 poolId) public pure {
+    function testSymbolicNotifyPool(uint64 poolId) public pure {
         MessageLib.NotifyPool memory a = MessageLib.NotifyPool({poolId: poolId});
         MessageLib.NotifyPool memory b = MessageLib.deserializeNotifyPool(a.serialize());
 
@@ -246,7 +246,10 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), PoolId.wrap(poolId).centrifugeId());
     }
 
-    function testNotifyPricePoolPerShare(uint64 poolId, bytes16 scId, uint128 price, uint64 timestamp) public pure {
+    function testSymbolicNotifyPricePoolPerShare(uint64 poolId, bytes16 scId, uint128 price, uint64 timestamp)
+        public
+        pure
+    {
         MessageLib.NotifyPricePoolPerShare memory a =
             MessageLib.NotifyPricePoolPerShare({poolId: poolId, scId: scId, price: price, timestamp: timestamp});
         MessageLib.NotifyPricePoolPerShare memory b = MessageLib.deserializeNotifyPricePoolPerShare(a.serialize());
@@ -260,10 +263,13 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), PoolId.wrap(poolId).centrifugeId());
     }
 
-    function testNotifyPricePoolPerAsset(uint64 poolId, bytes16 scId, uint128 assetId, uint128 price, uint64 timestamp)
-        public
-        pure
-    {
+    function testSymbolicNotifyPricePoolPerAsset(
+        uint64 poolId,
+        bytes16 scId,
+        uint128 assetId,
+        uint128 price,
+        uint64 timestamp
+    ) public pure {
         MessageLib.NotifyPricePoolPerAsset memory a = MessageLib.NotifyPricePoolPerAsset({
             poolId: poolId,
             scId: scId,
@@ -301,7 +307,7 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), PoolId.wrap(poolId).centrifugeId());
     }
 
-    function testUpdateShareHook(uint64 poolId, bytes16 scId, bytes32 hook) public pure {
+    function testSymbolicUpdateShareHook(uint64 poolId, bytes16 scId, bytes32 hook) public pure {
         MessageLib.UpdateShareHook memory a = MessageLib.UpdateShareHook({poolId: poolId, scId: scId, hook: hook});
         MessageLib.UpdateShareHook memory b = MessageLib.deserializeUpdateShareHook(a.serialize());
 
@@ -314,7 +320,7 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), PoolId.wrap(poolId).centrifugeId());
     }
 
-    function testInitiateTransferShares(
+    function testSymbolicInitiateTransferShares(
         uint64 poolId,
         bytes16 scId,
         uint16 centrifugeId,
@@ -344,7 +350,10 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), 0);
     }
 
-    function testExecuteTransferShares(uint64 poolId, bytes16 scId, bytes32 receiver, uint128 amount) public pure {
+    function testSymbolicExecuteTransferShares(uint64 poolId, bytes16 scId, bytes32 receiver, uint128 amount)
+        public
+        pure
+    {
         MessageLib.ExecuteTransferShares memory a =
             MessageLib.ExecuteTransferShares({poolId: poolId, scId: scId, receiver: receiver, amount: amount});
         MessageLib.ExecuteTransferShares memory b = MessageLib.deserializeExecuteTransferShares(a.serialize());
@@ -430,7 +439,7 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.payload.length, uint8(a.serialize()[a.serialize().messageLength() - a.payload.length - 1]));
     }
 
-    function testUpdateVault(uint64 poolId, bytes16 scId, bytes32 vaultOrFactory, uint128 assetId, uint8 kind)
+    function testSymbolicUpdateVault(uint64 poolId, bytes16 scId, bytes32 vaultOrFactory, uint128 assetId, uint8 kind)
         public
         pure
     {
@@ -454,7 +463,7 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), PoolId.wrap(poolId).centrifugeId());
     }
 
-    function testSetRequestManager(uint64 poolId, bytes16 scId, uint128 assetId, bytes32 manager) public pure {
+    function testSymbolicSetRequestManager(uint64 poolId, bytes16 scId, uint128 assetId, bytes32 manager) public pure {
         MessageLib.SetRequestManager memory a =
             MessageLib.SetRequestManager({poolId: poolId, scId: scId, assetId: assetId, manager: manager});
         MessageLib.SetRequestManager memory b = MessageLib.deserializeSetRequestManager(a.serialize());
@@ -469,7 +478,7 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), PoolId.wrap(poolId).centrifugeId());
     }
 
-    function testUpdateBalanceSheetManager(uint64 poolId, bytes32 who, bool canManage) public pure {
+    function testSymbolicUpdateBalanceSheetManager(uint64 poolId, bytes32 who, bool canManage) public pure {
         MessageLib.UpdateBalanceSheetManager memory a =
             MessageLib.UpdateBalanceSheetManager({poolId: poolId, who: who, canManage: canManage});
         MessageLib.UpdateBalanceSheetManager memory b = MessageLib.deserializeUpdateBalanceSheetManager(a.serialize());
@@ -483,147 +492,7 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), PoolId.wrap(poolId).centrifugeId());
     }
 
-    // function testDepositRequest(uint64 poolId, bytes16 scId, bytes32 investor, uint128 assetId, uint128 amount)
-    //     public
-    //     pure
-    // {
-    //     MessageLib.DepositRequest memory a = MessageLib.DepositRequest({
-    //         poolId: poolId,
-    //         scId: scId,
-    //         investor: investor,
-    //         assetId: assetId,
-    //         amount: amount
-    //     });
-    //     MessageLib.DepositRequest memory b = MessageLib.deserializeDepositRequest(a.serialize());
-
-    //     assertEq(a.poolId, b.poolId);
-    //     assertEq(a.scId, b.scId);
-    //     assertEq(a.investor, b.investor);
-    //     assertEq(a.assetId, b.assetId);
-    //     assertEq(a.amount, b.amount);
-
-    //     assertEq(a.serialize().messageLength(), a.serialize().length);
-    //     assertEq(a.serialize().messagePoolId().raw(), a.poolId);
-    //     assertEq(a.serialize().messageSourceCentrifugeId(), AssetId.wrap(assetId).centrifugeId());
-    // }
-
-    // function testRedeemRequest(uint64 poolId, bytes16 scId, bytes32 investor, uint128 assetId, uint128 amount)
-    //     public
-    //     pure
-    // {
-    //     MessageLib.RedeemRequest memory a =
-    //         MessageLib.RedeemRequest({poolId: poolId, scId: scId, investor: investor, assetId: assetId, amount:
-    // amount});
-    //     MessageLib.RedeemRequest memory b = MessageLib.deserializeRedeemRequest(a.serialize());
-
-    //     assertEq(a.poolId, b.poolId);
-    //     assertEq(a.scId, b.scId);
-    //     assertEq(a.investor, b.investor);
-    //     assertEq(a.assetId, b.assetId);
-    //     assertEq(a.amount, b.amount);
-
-    //     assertEq(a.serialize().messageLength(), a.serialize().length);
-    //     assertEq(a.serialize().messagePoolId().raw(), a.poolId);
-    //     assertEq(a.serialize().messageSourceCentrifugeId(), AssetId.wrap(assetId).centrifugeId());
-    // }
-
-    // function testCancelDepositRequest(uint64 poolId, bytes16 scId, bytes32 investor, uint128 assetId) public pure {
-    //     MessageLib.CancelDepositRequest memory a =
-    //         MessageLib.CancelDepositRequest({poolId: poolId, scId: scId, investor: investor, assetId: assetId});
-    //     MessageLib.CancelDepositRequest memory b = MessageLib.deserializeCancelDepositRequest(a.serialize());
-
-    //     assertEq(a.poolId, b.poolId);
-    //     assertEq(a.scId, b.scId);
-    //     assertEq(a.investor, b.investor);
-    //     assertEq(a.assetId, b.assetId);
-
-    //     assertEq(a.serialize().messageLength(), a.serialize().length);
-    //     assertEq(a.serialize().messagePoolId().raw(), a.poolId);
-    //     assertEq(a.serialize().messageSourceCentrifugeId(), AssetId.wrap(assetId).centrifugeId());
-    // }
-
-    // function testCancelRedeemRequest(uint64 poolId, bytes16 scId, bytes32 investor, uint128 assetId) public pure {
-    //     MessageLib.CancelRedeemRequest memory a =
-    //         MessageLib.CancelRedeemRequest({poolId: poolId, scId: scId, investor: investor, assetId: assetId});
-    //     MessageLib.CancelRedeemRequest memory b = MessageLib.deserializeCancelRedeemRequest(a.serialize());
-
-    //     assertEq(a.poolId, b.poolId);
-    //     assertEq(a.scId, b.scId);
-    //     assertEq(a.investor, b.investor);
-    //     assertEq(a.assetId, b.assetId);
-
-    //     assertEq(a.serialize().messageLength(), a.serialize().length);
-    //     assertEq(a.serialize().messagePoolId().raw(), a.poolId);
-    //     assertEq(a.serialize().messageSourceCentrifugeId(), AssetId.wrap(assetId).centrifugeId());
-    // }
-
-    // function testFulfilledDepositRequest(
-    //     uint64 poolId,
-    //     bytes16 scId,
-    //     bytes32 investor,
-    //     uint128 assetId,
-    //     uint128 fulfilledAssetAmount,
-    //     uint128 fulfilledShareAmount,
-    //     uint128 cancelledAssetAmount
-    // ) public pure {
-    //     MessageLib.FulfilledDepositRequest memory a = MessageLib.FulfilledDepositRequest({
-    //         poolId: poolId,
-    //         scId: scId,
-    //         investor: investor,
-    //         assetId: assetId,
-    //         fulfilledAssetAmount: fulfilledAssetAmount,
-    //         fulfilledShareAmount: fulfilledShareAmount,
-    //         cancelledAssetAmount: cancelledAssetAmount
-    //     });
-    //     MessageLib.FulfilledDepositRequest memory b = MessageLib.deserializeFulfilledDepositRequest(a.serialize());
-
-    //     assertEq(a.poolId, b.poolId);
-    //     assertEq(a.scId, b.scId);
-    //     assertEq(a.investor, b.investor);
-    //     assertEq(a.assetId, b.assetId);
-    //     assertEq(a.fulfilledAssetAmount, b.fulfilledAssetAmount);
-    //     assertEq(a.fulfilledShareAmount, b.fulfilledShareAmount);
-    //     assertEq(a.cancelledAssetAmount, b.cancelledAssetAmount);
-
-    //     assertEq(a.serialize().messageLength(), a.serialize().length);
-    //     assertEq(a.serialize().messagePoolId().raw(), a.poolId);
-    //     assertEq(a.serialize().messageSourceCentrifugeId(), PoolId.wrap(poolId).centrifugeId());
-    // }
-
-    // function testFulfilledRedeemRequest(
-    //     uint64 poolId,
-    //     bytes16 scId,
-    //     bytes32 investor,
-    //     uint128 assetId,
-    //     uint128 fulfilledAssetAmount,
-    //     uint128 fulfilledShareAmount,
-    //     uint128 cancelledShareAmount
-    // ) public pure {
-    //     MessageLib.FulfilledRedeemRequest memory a = MessageLib.FulfilledRedeemRequest({
-    //         poolId: poolId,
-    //         scId: scId,
-    //         investor: investor,
-    //         assetId: assetId,
-    //         fulfilledAssetAmount: fulfilledAssetAmount,
-    //         fulfilledShareAmount: fulfilledShareAmount,
-    //         cancelledShareAmount: cancelledShareAmount
-    //     });
-    //     MessageLib.FulfilledRedeemRequest memory b = MessageLib.deserializeFulfilledRedeemRequest(a.serialize());
-
-    //     assertEq(a.poolId, b.poolId);
-    //     assertEq(a.scId, b.scId);
-    //     assertEq(a.investor, b.investor);
-    //     assertEq(a.assetId, b.assetId);
-    //     assertEq(a.fulfilledAssetAmount, b.fulfilledAssetAmount);
-    //     assertEq(a.fulfilledShareAmount, b.fulfilledShareAmount);
-    //     assertEq(a.cancelledShareAmount, b.cancelledShareAmount);
-
-    //     assertEq(a.serialize().messageLength(), a.serialize().length);
-    //     assertEq(a.serialize().messagePoolId().raw(), a.poolId);
-    //     assertEq(a.serialize().messageSourceCentrifugeId(), PoolId.wrap(poolId).centrifugeId());
-    // }
-
-    function testUpdateHoldingAmount(
+    function testSymbolicUpdateHoldingAmount(
         uint64 poolId,
         bytes16 scId,
         uint128 assetId,
@@ -663,7 +532,7 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), AssetId.wrap(assetId).centrifugeId());
     }
 
-    function testUpdateShares(
+    function testSymbolicUpdateShares(
         uint64 poolId,
         bytes16 scId,
         uint128 shares,
@@ -697,66 +566,10 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), 0);
     }
 
-    // function testApprovedDeposits(
-    //     uint64 poolId,
-    //     bytes16 scId,
-    //     uint128 assetId,
-    //     uint128 assetAmount,
-    //     uint128 pricePoolPerAsset
-    // ) public pure {
-    //     MessageLib.ApprovedDeposits memory a = MessageLib.ApprovedDeposits({
-    //         poolId: poolId,
-    //         scId: scId,
-    //         assetId: assetId,
-    //         assetAmount: assetAmount,
-    //         pricePoolPerAsset: pricePoolPerAsset
-    //     });
-
-    //     MessageLib.ApprovedDeposits memory b = MessageLib.deserializeApprovedDeposits(a.serialize());
-
-    //     assertEq(a.poolId, b.poolId);
-    //     assertEq(a.scId, b.scId);
-    //     assertEq(a.assetId, b.assetId);
-    //     assertEq(a.assetAmount, b.assetAmount);
-    //     assertEq(a.pricePoolPerAsset, b.pricePoolPerAsset);
-
-    //     assertEq(a.serialize().messageLength(), a.serialize().length);
-    //     assertEq(a.serialize().messagePoolId().raw(), a.poolId);
-    //     assertEq(a.serialize().messageSourceCentrifugeId(), PoolId.wrap(poolId).centrifugeId());
-    // }
-
-    // function testRevokedShares(
-    //     uint64 poolId,
-    //     bytes16 scId,
-    //     uint128 assetId,
-    //     uint128 assetAmount,
-    //     uint128 shareAmount,
-    //     uint128 pricePoolPerShare
-    // ) public pure {
-    //     MessageLib.RevokedShares memory a = MessageLib.RevokedShares({
-    //         poolId: poolId,
-    //         scId: scId,
-    //         assetId: assetId,
-    //         assetAmount: assetAmount,
-    //         shareAmount: shareAmount,
-    //         pricePoolPerShare: pricePoolPerShare
-    //     });
-
-    //     MessageLib.RevokedShares memory b = MessageLib.deserializeRevokedShares(a.serialize());
-
-    //     assertEq(a.poolId, b.poolId);
-    //     assertEq(a.scId, b.scId);
-    //     assertEq(a.assetId, b.assetId);
-    //     assertEq(a.assetAmount, b.assetAmount);
-    //     assertEq(a.shareAmount, b.shareAmount);
-    //     assertEq(a.pricePoolPerShare, b.pricePoolPerShare);
-
-    //     assertEq(a.serialize().messageLength(), a.serialize().length);
-    //     assertEq(a.serialize().messagePoolId().raw(), a.poolId);
-    //     assertEq(a.serialize().messageSourceCentrifugeId(), PoolId.wrap(poolId).centrifugeId());
-    // }
-
-    function testMaxAssetPriceAge(uint64 poolId, bytes16 scId, uint128 assetId, uint64 maxPriceAge) public pure {
+    function testSymbolicMaxAssetPriceAge(uint64 poolId, bytes16 scId, uint128 assetId, uint64 maxPriceAge)
+        public
+        pure
+    {
         MessageLib.MaxAssetPriceAge memory a =
             MessageLib.MaxAssetPriceAge({poolId: poolId, scId: scId, assetId: assetId, maxPriceAge: maxPriceAge});
         MessageLib.MaxAssetPriceAge memory b = MessageLib.deserializeMaxAssetPriceAge(a.serialize());
@@ -771,7 +584,7 @@ contract TestMessageLibIdentities is Test {
         assertEq(a.serialize().messageSourceCentrifugeId(), PoolId.wrap(poolId).centrifugeId());
     }
 
-    function testMaxSharePriceAge(uint64 poolId, bytes16 scId, uint64 maxPriceAge) public pure {
+    function testSymbolicMaxSharePriceAge(uint64 poolId, bytes16 scId, uint64 maxPriceAge) public pure {
         MessageLib.MaxSharePriceAge memory a =
             MessageLib.MaxSharePriceAge({poolId: poolId, scId: scId, maxPriceAge: maxPriceAge});
         MessageLib.MaxSharePriceAge memory b = MessageLib.deserializeMaxSharePriceAge(a.serialize());
diff --git a/test/misc/unit/libraries/ArrayLib.t.sol b/test/misc/unit/libraries/ArrayLib.t.sol
index 2645d7d61..030c76476 100644
--- a/test/misc/unit/libraries/ArrayLib.t.sol
+++ b/test/misc/unit/libraries/ArrayLib.t.sol
@@ -10,14 +10,14 @@ contract ArrayLibTest is Test {
     uint16[8] initialArray;
     uint16[8] decreasedArray;
 
-    function testCountNonZeroValues(uint8 numNonZeroes) public view {
+    function testSymbolicCountNonZeroValues(uint8 numNonZeroes) public view {
         numNonZeroes = uint8(bound(numNonZeroes, 0, 8));
         uint16[8] memory arr = _randomArray(numNonZeroes);
 
         assertEq(ArrayLib.countNonZeroValues(arr), numNonZeroes);
     }
 
-    function testDecreaseFirstNValues(uint8 numValuesToDecrease) public {
+    function testSymbolicDecreaseFirstNValues(uint8 numValuesToDecrease) public {
         numValuesToDecrease = uint8(bound(numValuesToDecrease, 0, 8));
 
         initialArray = _randomArray(8);
@@ -29,7 +29,7 @@ contract ArrayLibTest is Test {
         assertEq(_count(initialArray) - _count(decreasedArray), _min(numNonZeroes, numValuesToDecrease));
     }
 
-    function testIsEmpty(uint8 numNonZeroes) public view {
+    function testSymbolicIsEmpty(uint8 numNonZeroes) public view {
         numNonZeroes = uint8(bound(numNonZeroes, 0, 8));
         uint16[8] memory arr = _randomArray(numNonZeroes);
 
diff --git a/test/misc/unit/libraries/BytesLib.t.sol b/test/misc/unit/libraries/BytesLib.t.sol
index 42adaa5de..2459c5481 100644
--- a/test/misc/unit/libraries/BytesLib.t.sol
+++ b/test/misc/unit/libraries/BytesLib.t.sol
@@ -6,7 +6,7 @@ import {BytesLib} from "../../../../src/misc/libraries/BytesLib.sol";
 import "forge-std/Test.sol";
 
 contract BytesLibTest is Test {
-    function testSlice(bytes memory data, bytes memory randomStart, bytes memory randomEnd) public pure {
+    function testSymbolicSlice(bytes memory data, bytes memory randomStart, bytes memory randomEnd) public pure {
         bytes memory value = bytes.concat(bytes.concat(randomStart, abi.encodePacked(data)), randomEnd);
         assertEq(BytesLib.slice(value, randomStart.length, data.length), data);
     }
@@ -30,42 +30,42 @@ contract BytesLibTest is Test {
         assertEq(got, expected, "!bytes");
     }
 
-    function testToAddress(address addr, bytes memory randomStart, bytes memory randomEnd) public pure {
+    function testSymbolicToAddress(address addr, bytes memory randomStart, bytes memory randomEnd) public pure {
         bytes memory value = bytes.concat(bytes.concat(randomStart, abi.encodePacked(addr)), randomEnd);
         assertEq(BytesLib.toAddress(value, randomStart.length), addr);
     }
 
-    function testToUint8(uint8 number, bytes memory randomStart, bytes memory randomEnd) public pure {
+    function testSymbolicToUint8(uint8 number, bytes memory randomStart, bytes memory randomEnd) public pure {
         bytes memory value = bytes.concat(bytes.concat(randomStart, abi.encodePacked(number)), randomEnd);
         assertEq(BytesLib.toUint8(value, randomStart.length), number);
     }
 
-    function testToUint16(uint16 number, bytes memory randomStart, bytes memory randomEnd) public pure {
+    function testSymbolicToUint16(uint16 number, bytes memory randomStart, bytes memory randomEnd) public pure {
         bytes memory value = bytes.concat(bytes.concat(randomStart, abi.encodePacked(number)), randomEnd);
         assertEq(BytesLib.toUint16(value, randomStart.length), number);
     }
 
-    function testToUint32(uint32 number, bytes memory randomStart, bytes memory randomEnd) public pure {
+    function testSymbolicToUint32(uint32 number, bytes memory randomStart, bytes memory randomEnd) public pure {
         bytes memory value = bytes.concat(bytes.concat(randomStart, abi.encodePacked(number)), randomEnd);
         assertEq(BytesLib.toUint32(value, randomStart.length), number);
     }
 
-    function testToUint64(uint64 number, bytes memory randomStart, bytes memory randomEnd) public pure {
+    function testSymbolicToUint64(uint64 number, bytes memory randomStart, bytes memory randomEnd) public pure {
         bytes memory value = bytes.concat(bytes.concat(randomStart, abi.encodePacked(number)), randomEnd);
         assertEq(BytesLib.toUint64(value, randomStart.length), number);
     }
 
-    function testToUint128(uint128 number, bytes memory randomStart, bytes memory randomEnd) public pure {
+    function testSymbolicToUint128(uint128 number, bytes memory randomStart, bytes memory randomEnd) public pure {
         bytes memory value = bytes.concat(bytes.concat(randomStart, abi.encodePacked(number)), randomEnd);
         assertEq(BytesLib.toUint128(value, randomStart.length), number);
     }
 
-    function testToBytes32(bytes32 data, bytes memory randomStart, bytes memory randomEnd) public pure {
+    function testSymbolicToBytes32(bytes32 data, bytes memory randomStart, bytes memory randomEnd) public pure {
         bytes memory value = bytes.concat(bytes.concat(randomStart, abi.encodePacked(data)), randomEnd);
         assertEq(BytesLib.toBytes32(value, randomStart.length), data);
     }
 
-    function testToBytes16(bytes16 data, bytes memory randomStart, bytes memory randomEnd) public pure {
+    function testSymbolicToBytes16(bytes16 data, bytes memory randomStart, bytes memory randomEnd) public pure {
         bytes memory value = bytes.concat(bytes.concat(randomStart, abi.encodePacked(data)), randomEnd);
         assertEq(BytesLib.toBytes16(value, randomStart.length), data);
     }
diff --git a/test/misc/unit/libraries/CastLib.t.sol b/test/misc/unit/libraries/CastLib.t.sol
index 832dd3539..52b9b0957 100644
--- a/test/misc/unit/libraries/CastLib.t.sol
+++ b/test/misc/unit/libraries/CastLib.t.sol
@@ -6,7 +6,7 @@ import {CastLib} from "../../../../src/misc/libraries/CastLib.sol";
 import "forge-std/Test.sol";
 
 contract CastLibTest is Test {
-    function testToAddress(address addr) public pure {
+    function testSymbolicToAddress(address addr) public pure {
         assertEq(CastLib.toAddress(bytes32(bytes20(addr))), addr);
     }
 
diff --git a/test/misc/unit/libraries/D18.t.sol b/test/misc/unit/libraries/D18.t.sol
index 1aa50be95..bc1177836 100644
--- a/test/misc/unit/libraries/D18.t.sol
+++ b/test/misc/unit/libraries/D18.t.sol
@@ -7,22 +7,22 @@ import "../../../../src/misc/libraries/MathLib.sol";
 import "forge-std/Test.sol";
 
 contract D18Test is Test {
-    function testFuzzAdd(uint128 a, uint128 b) public pure {
+    function testSymbolicAdd(uint128 a, uint128 b) public pure {
         vm.assume(a <= type(uint128).max / 2);
         vm.assume(b <= type(uint128).max / 2);
 
         D18 c = d18(a) + d18(b);
-        assertEqDecimal(c.raw(), a + b, 18);
+        assertEq(c.raw(), a + b);
     }
 
-    function testFuzzSub(uint128 a, uint128 b) public pure {
+    function testSymbolicSub(uint128 a, uint128 b) public pure {
         vm.assume(a >= b);
 
         D18 c = d18(a) - d18(b);
-        assertEqDecimal(c.raw(), a - b, 18);
+        assertEq(c.raw(), a - b);
     }
 
-    function testMulUint128() public pure {
+    function testSymbolicMulUint128() public pure {
         D18 factor = d18(1_500_000_000_000_000_000); // 1.5
         uint128 value = 4_000_000_000_000_000;
 
@@ -30,7 +30,7 @@ contract D18Test is Test {
         assertEq(factor.mulUint128(value, MathLib.Rounding.Up), 6_000_000_000_000_000);
     }
 
-    function testFuzzMulUInt128(uint128 a, uint128 b) public pure {
+    function testSymbolicMulUInt128(uint128 a, uint128 b) public pure {
         a = uint128(bound(a, 1, type(uint128).max));
         b = uint128(bound(b, 0, type(uint128).max / a));
 
@@ -40,7 +40,7 @@ contract D18Test is Test {
         assertEq(cUp, MathLib.mulDiv(a, b, 1e18));
     }
 
-    function testRoundingUint128(uint128 a) public pure {
+    function testSymbolicRoundingUint128(uint128 a) public pure {
         a = uint128(bound(a, 0, type(uint128).max / 1e18));
         D18 oneHundredPercent = d18(1e18);
 
@@ -48,7 +48,7 @@ contract D18Test is Test {
         assertEq(oneHundredPercent.mulUint128(a, MathLib.Rounding.Up), a);
     }
 
-    function testMulUint256() public pure {
+    function testSymbolicMulUint256() public pure {
         D18 factor = d18(1_500_000_000_000_000_000); // 1.5
         uint256 value = 4_000_000_000_000_000_000_000_000;
 
@@ -56,7 +56,7 @@ contract D18Test is Test {
         assertEq(factor.mulUint256(value, MathLib.Rounding.Up), 6_000_000_000_000_000_000_000_000);
     }
 
-    function testFuzzMulUInt256(uint128 a, uint256 b) public pure {
+    function testSymbolicMulUInt256(uint128 a, uint256 b) public pure {
         a = uint128(bound(a, 1, type(uint128).max));
         b = uint256(bound(b, 0, type(uint256).max / a));
 
@@ -66,7 +66,7 @@ contract D18Test is Test {
         assertEq(cUp, MathLib.mulDiv(a, b, 1e18));
     }
 
-    function testRoundingUint256(uint256 a) public pure {
+    function testSymbolicRoundingUint256(uint256 a) public pure {
         a = bound(a, 0, type(uint256).max / 1e18);
         D18 oneHundredPercent = d18(1e18);
 
@@ -74,7 +74,7 @@ contract D18Test is Test {
         assertEq(oneHundredPercent.mulUint256(a, MathLib.Rounding.Up), a);
     }
 
-    function testReciprocalMulInt128() public pure {
+    function testSymbolicReciprocalMulInt128() public pure {
         D18 divisor = d18(2e18);
         uint128 multiplier = 1e20;
 
@@ -82,7 +82,7 @@ contract D18Test is Test {
         assertEq(divisor.reciprocalMulUint128(multiplier, MathLib.Rounding.Up), 5e19);
     }
 
-    function testFuzzReciprocalMulInt128(uint128 divisor_, uint128 multiplier) public pure {
+    function testSymbolicReciprocalMulInt128(uint128 divisor_, uint128 multiplier) public pure {
         D18 divisor = d18(uint128(bound(divisor_, 1e4, 1e20)));
         multiplier = uint128(bound(multiplier, 0, type(uint128).max / 1e18));
 
@@ -93,7 +93,7 @@ contract D18Test is Test {
         assertEq(divisor.reciprocalMulUint128(multiplier, MathLib.Rounding.Up), expectedUp);
     }
 
-    function testReciprocalMulInt256() public pure {
+    function testSymbolicReciprocalMulInt256() public pure {
         D18 divisor = d18(2e18);
         uint256 multiplier = 1e20;
 
@@ -101,7 +101,7 @@ contract D18Test is Test {
         assertEq(divisor.reciprocalMulUint256(multiplier, MathLib.Rounding.Up), 5e19);
     }
 
-    function testFuzzReciprocalMulInt256(uint128 divisor_, uint256 multiplier) public pure {
+    function testSymbolicReciprocalMulInt256(uint128 divisor_, uint256 multiplier) public pure {
         D18 divisor = d18(uint128(bound(divisor_, 1e4, 1e20)));
         multiplier = bound(multiplier, 0, type(uint256).max / 1e18);
 
@@ -112,28 +112,28 @@ contract D18Test is Test {
         assertEq(divisor.reciprocalMulUint256(multiplier, MathLib.Rounding.Up), expectedUp);
     }
 
-    function testMulD18() public pure {
+    function testSymbolicMulD18() public pure {
         D18 left = d18(50e18);
         D18 right = d18(2e19);
 
         assertEq(mulD18(left, right).raw(), 100e19);
     }
 
-    function testFuzzMulD18(uint128 left_, uint128 right_) public pure {
+    function testSymbolicMulD18(uint128 left_, uint128 right_) public pure {
         D18 left = d18(uint128(bound(left_, 1, type(uint128).max)));
         D18 right = d18(uint128(bound(right_, 0, type(uint128).max / left.raw())));
 
         assertEq(mulD18(left, right).raw(), left.raw() * right.raw() / 1e18);
     }
 
-    function testDivD18() public pure {
+    function testSymbolicDivD18() public pure {
         D18 numerator = d18(50e18);
         D18 denominator = d18(2e19);
 
         assertEq(divD18(numerator, denominator).raw(), 25e17);
     }
 
-    function testFuzzDivD18(uint128 numerator_, uint128 denominator_) public pure {
+    function testSymbolicDivD18(uint128 numerator_, uint128 denominator_) public pure {
         D18 numerator = d18(uint128(bound(numerator_, 1, 1e20)));
         D18 denominator = d18(uint128(bound(denominator_, 1, 1e20)));
 
@@ -147,19 +147,19 @@ contract D18Test is Test {
         assert(!eq(a, d18(5235)));
     }
 
-    function testRawD18() public pure {
+    function testSymbolicRawD18() public pure {
         uint128 a_ = 3245252;
         D18 a = d18(a_);
 
         assertEq(raw(a), a_);
     }
 
-    function testIsZero() public pure {
+    function testSymbolicIsZero() public pure {
         assertEq(d18(0).isZero(), true);
         assertEq(d18(123).isZero(), false);
     }
 
-    function testIsNotZero() public pure {
+    function testSymbolicIsNotZero() public pure {
         assertEq(d18(0).isNotZero(), false);
         assertEq(d18(123).isNotZero(), true);
     }
@@ -167,7 +167,7 @@ contract D18Test is Test {
 
 contract D18ReciprocalTest is Test {
     /// @dev Fuzz test reciprocal function ensuring accurate calculation and round-trip multiplication.
-    function testFuzzReciprocal(uint128 val) public pure {
+    function testReciprocal(uint128 val) public pure {
         // Avoid division-by-zero, keep input reasonable
         val = uint128(bound(val, 1, type(uint128).max / 1e18));
         D18 input = D18.wrap(val);
@@ -182,7 +182,7 @@ contract D18ReciprocalTest is Test {
     }
 
     /// @dev Explicitly test edge case for reciprocal(1e18) == 1e18
-    function testReciprocalOne() public pure {
+    function testSymbolicReciprocalOne() public pure {
         D18 one = D18.wrap(1e18);
         D18 result = one.reciprocal();
         assertEq(result.raw(), 1e18, "Reciprocal of 1e18 should be 1e18");
diff --git a/test/misc/unit/libraries/MathLib.t.sol b/test/misc/unit/libraries/MathLib.t.sol
index 1022cf491..822a07e0f 100644
--- a/test/misc/unit/libraries/MathLib.t.sol
+++ b/test/misc/unit/libraries/MathLib.t.sol
@@ -8,7 +8,7 @@ import "forge-std/Test.sol";
 contract MathLibTest is Test {
     using MathLib for uint256;
 
-    function testRpow() public pure {
+    function testSymbolicRpow() public pure {
         uint256 base = 10 ** 27;
         uint256 x = 2 * 10 ** 27;
         uint256 n = 3;
@@ -19,7 +19,7 @@ contract MathLibTest is Test {
         assertEq(result, expected, "Incorrect rpow calculation");
     }
 
-    function testMulDivDown(uint256 x, uint256 y, uint256 denominator) public pure {
+    function testSymbolicMulDivDown(uint256 x, uint256 y, uint256 denominator) public pure {
         // Ignore cases where x * y overflows or denominator is 0.
         unchecked {
             if (denominator == 0 || (x != 0 && (x * y) / x != y)) return;
@@ -29,12 +29,12 @@ contract MathLibTest is Test {
     }
 
     /// forge-config: default.allow_internal_expect_revert = true
-    function testMulDivDownZeroDenominator(uint256 x, uint256 y) public {
+    function testSymbolicMulDivDownZeroDenominator(uint256 x, uint256 y) public {
         vm.expectRevert();
         MathLib.mulDiv(x, y, 0, MathLib.Rounding.Down);
     }
 
-    function testMulDivUp(uint256 x, uint256 y, uint256 denominator) public pure {
+    function testSymbolicMulDivUp(uint256 x, uint256 y, uint256 denominator) public pure {
         denominator = bound(denominator, 1, type(uint256).max - 1);
         y = bound(y, 1, type(uint256).max);
         x = bound(x, 0, (type(uint256).max - denominator - 1) / y);
@@ -43,7 +43,7 @@ contract MathLibTest is Test {
     }
 
     /// forge-config: default.allow_internal_expect_revert = true
-    function testMulDivUpUnderverflow(uint256 x, uint256 y) public {
+    function testSymbolicMulDivUpUnderverflow(uint256 x, uint256 y) public {
         vm.assume(x > 0 && y > 0);
 
         vm.expectRevert();
@@ -51,7 +51,7 @@ contract MathLibTest is Test {
     }
 
     /// forge-config: default.allow_internal_expect_revert = true
-    function testMulDivUpZeroDenominator(uint256 x, uint256 y) public {
+    function testSymbolicMulDivUpZeroDenominator(uint256 x, uint256 y) public {
         vm.expectRevert();
         MathLib.mulDiv(x, y, 0, MathLib.Rounding.Up);
     }
@@ -63,7 +63,7 @@ contract MathLibTest is Test {
     }
 
     /// forge-config: default.allow_internal_expect_revert = true
-    function testToUint128Overflow(uint128 x) public {
+    function testSymbolicToUint128Overflow(uint128 x) public {
         vm.assume(x > 0);
         vm.expectRevert(MathLib.Uint128_Overflow.selector);
         MathLib.toUint128(uint256(type(uint128).max) + x);
@@ -76,45 +76,45 @@ contract MathLibTest is Test {
     }
 
     /// forge-config: default.allow_internal_expect_revert = true
-    function testToUint8Overflow(uint256 x) public {
+    function testSymbolicToUint8Overflow(uint256 x) public {
         vm.assume(x > type(uint8).max);
         vm.expectRevert(MathLib.Uint8_Overflow.selector);
         MathLib.toUint8(x);
     }
 
-    function testToUint32(uint256 x) public pure {
+    function testSymbolicToUint32(uint256 x) public pure {
         x = bound(x, 0, type(uint32).max);
 
         assertEq(x, uint256(MathLib.toUint32(x)));
     }
 
     /// forge-config: default.allow_internal_expect_revert = true
-    function testToUint32Overflow(uint256 x) public {
+    function testSymbolicToUint32Overflow(uint256 x) public {
         vm.assume(x > type(uint32).max);
         vm.expectRevert(MathLib.Uint32_Overflow.selector);
         MathLib.toUint32(x);
     }
 
-    function testToUint64(uint256 x) public pure {
+    function testSymbolicToUint64(uint256 x) public pure {
         x = bound(x, 0, type(uint64).max);
 
         assertEq(x, uint256(MathLib.toUint64(x)));
     }
 
     /// forge-config: default.allow_internal_expect_revert = true
-    function testToUint64Overflow(uint256 x) public {
+    function testSymbolicToUint64Overflow(uint256 x) public {
         vm.assume(x > type(uint64).max);
         vm.expectRevert(MathLib.Uint64_Overflow.selector);
         MathLib.toUint64(x);
     }
 
-    function testMin(uint256 x, uint256 y) public pure {
+    function testSymbolicMin(uint256 x, uint256 y) public pure {
         vm.assume(x > 0);
         y = uint256(bound(y, 0, x - 1));
         assertEq(MathLib.min(x, y), y);
     }
 
-    function testMax(uint256 x, uint256 y) public pure {
+    function testSymbolicMax(uint256 x, uint256 y) public pure {
         vm.assume(x > 0);
         y = uint256(bound(y, 0, x - 1));
         assertEq(MathLib.max(x, y), x);
diff --git a/test/misc/unit/libraries/MerkleProofLib.t.sol b/test/misc/unit/libraries/MerkleProofLib.t.sol
index c4c67bc5f..7f89f01bd 100644
--- a/test/misc/unit/libraries/MerkleProofLib.t.sol
+++ b/test/misc/unit/libraries/MerkleProofLib.t.sol
@@ -7,18 +7,18 @@ import "forge-std/Test.sol";
 
 /// @author Modified from https://github.com/transmissions11/solmate/blob/main/src/test/MerkleProofLib.t.sol
 contract MerkleProofLibTest is Test {
-    function testVerifyEmptyMerkleProofSuppliedLeafAndRootSame() public view {
+    function testSymbolicVerifyEmptyMerkleProofSuppliedLeafAndRootSame() public view {
         bytes32[] memory proof;
         assertEq(this.verify(proof, 0x00, 0x00), true);
     }
 
-    function testVerifyEmptyMerkleProofSuppliedLeafAndRootDifferent() public view {
+    function testSymbolicVerifyEmptyMerkleProofSuppliedLeafAndRootDifferent() public view {
         bytes32[] memory proof;
         bytes32 leaf = "a";
         assertEq(this.verify(proof, 0x00, leaf), false);
     }
 
-    function testValidProofSupplied() public view {
+    function testSymbolicValidProofSupplied() public view {
         // Merkle tree created from leaves ['a', 'b', 'c'].
         // Leaf is 'a'.
         bytes32[] memory proof = new bytes32[](2);
@@ -29,7 +29,7 @@ contract MerkleProofLibTest is Test {
         assertEq(this.verify(proof, root, leaf), true);
     }
 
-    function testVerifyInvalidProofSupplied() public view {
+    function testSymbolicVerifyInvalidProofSupplied() public view {
         // Merkle tree created from leaves ['a', 'b', 'c'].
         // Leaf is 'a'.
         // Proof is same as testValidProofSupplied but last byte of first element is modified.