diff --git a/contracts/facade/facets/ReadFacet.sol b/contracts/facade/facets/ReadFacet.sol
index be038cf30..75a2f3a68 100644
--- a/contracts/facade/facets/ReadFacet.sol
+++ b/contracts/facade/facets/ReadFacet.sol
@@ -68,7 +68,10 @@ contract ReadFacet {
             uint192 mid = (low + high) / 2;
 
             // {UoA} = {tok} * {UoA/Tok}
-            depositsUoA[i] = shiftl_toFix(deposits[i], -int8(asset.erc20Decimals()), CEIL).mul(mid);
+            depositsUoA[i] = shiftl_toFix(deposits[i], -int8(asset.erc20Decimals()), CEIL).mul(
+                mid,
+                CEIL
+            );
         }
     }
 
@@ -355,7 +358,7 @@ contract ReadFacet {
                 uint192 avg = (low + high) / 2;
 
                 // {UoA} = {UoA} + {tok}
-                uoaNeeded += needed.mul(avg);
+                uoaNeeded += needed.mul(avg, CEIL);
 
                 // {UoA} = {UoA} + {tok} * {UoA/tok}
                 uoaHeldInBaskets += fixMin(needed, asset.bal(address(bm))).mul(avg);
diff --git a/contracts/libraries/Fixed.sol b/contracts/libraries/Fixed.sol
index 699f64572..f8550007f 100644
--- a/contracts/libraries/Fixed.sol
+++ b/contracts/libraries/Fixed.sol
@@ -250,7 +250,7 @@ library FixLib {
     /// @return x * y
     // as-ints: x * y/1e18  [division using ROUND, not FLOOR]
     function mul(uint192 x, uint192 y) internal pure returns (uint192) {
-        return mul(x, y, ROUND);
+        return mul(x, y, FLOOR);
     }
 
     /// Multiply this uint192 by a uint192
@@ -547,6 +547,7 @@ library FixLib {
         RoundingMode rounding
     ) internal pure returns (uint192) {
         if (a == 0) return 0;
+        if (a == FIX_MAX) return FIX_MAX;
         if (b == 0) return FIX_MAX;
 
         uint256 raw = _divrnd(FIX_ONE_256 * a, uint256(b), rounding);
@@ -591,6 +592,10 @@ library FixLib {
             r *= 2 - c_256 * r;
             result_256 = lo * r;
 
+            if (result_256 >= FIX_MAX) {
+                return FIX_MAX;
+            }
+
             // Apply rounding
             if (rounding == CEIL) {
                 if (mm != 0) result_256 += 1;
diff --git a/contracts/p0/BackingManager.sol b/contracts/p0/BackingManager.sol
index 752c94cca..2efc92896 100644
--- a/contracts/p0/BackingManager.sol
+++ b/contracts/p0/BackingManager.sol
@@ -176,7 +176,8 @@ contract BackingManagerP0 is TradingP0, IBackingManager {
             }
         }
 
-        uint192 needed = main.rToken().basketsNeeded().mul(FIX_ONE.plus(backingBuffer)); // {BU}
+        // {BU}
+        uint192 needed = main.rToken().basketsNeeded().mul(FIX_ONE.plus(backingBuffer), CEIL);
 
         // Handout excess assets above what is needed, including any newly minted RToken
         RevenueTotals memory totals = main.distributor().totals();
diff --git a/contracts/p0/mixins/TradingLib.sol b/contracts/p0/mixins/TradingLib.sol
index deea59f83..3b7482bcc 100644
--- a/contracts/p0/mixins/TradingLib.sol
+++ b/contracts/p0/mixins/TradingLib.sol
@@ -74,7 +74,7 @@ library TradingLibP0 {
 
         // Calculate equivalent buyAmount within [0, FIX_MAX]
         // {buyTok} = {sellTok} * {1} * {UoA/sellTok} / {UoA/buyTok}
-        uint192 b = s.mul(FIX_ONE.minus(maxTradeSlippage)).safeMulDiv(
+        uint192 b = s.mul(FIX_ONE.minus(maxTradeSlippage), CEIL).safeMulDiv(
             trade.prices.sellLow,
             trade.prices.buyHigh,
             CEIL
diff --git a/contracts/p1/BackingManager.sol b/contracts/p1/BackingManager.sol
index c2ddf852d..1bdca04b0 100644
--- a/contracts/p1/BackingManager.sol
+++ b/contracts/p1/BackingManager.sol
@@ -222,7 +222,7 @@ contract BackingManagerP1 is TradingP1, IBackingManager {
             rToken.mint(baskets - rToken.basketsNeeded());
         }
 
-        uint192 needed = rToken.basketsNeeded().mul(FIX_ONE + backingBuffer); // {BU}
+        uint192 needed = rToken.basketsNeeded().mul(FIX_ONE + backingBuffer, CEIL); // {BU}
 
         // At this point, even though basketsNeeded may have changed, we are:
         // - We're fully collateralized
diff --git a/contracts/p1/mixins/TradeLib.sol b/contracts/p1/mixins/TradeLib.sol
index eab2df2c7..e66ca3911 100644
--- a/contracts/p1/mixins/TradeLib.sol
+++ b/contracts/p1/mixins/TradeLib.sol
@@ -73,7 +73,7 @@ library TradeLib {
 
         // Calculate equivalent buyAmount within [0, FIX_MAX]
         // {buyTok} = {sellTok} * {1} * {UoA/sellTok} / {UoA/buyTok}
-        uint192 b = s.mul(FIX_ONE.minus(maxTradeSlippage)).safeMulDiv(
+        uint192 b = s.mul(FIX_ONE.minus(maxTradeSlippage), CEIL).safeMulDiv(
             trade.prices.sellLow,
             trade.prices.buyHigh,
             CEIL
diff --git a/test/Recollateralization.test.ts b/test/Recollateralization.test.ts
index 023ab8406..962185af3 100644
--- a/test/Recollateralization.test.ts
+++ b/test/Recollateralization.test.ts
@@ -2770,7 +2770,7 @@ describe(`Recollateralization - P${IMPLEMENTATION}`, () => {
           await advanceTime(config.batchAuctionLength.add(100).toString())
 
           // Run auctions - will end current, and will open a new auction to buy the remaining backup tokens
-          const buyAmtBidRSR: BigNumber = issueAmount.div(2).add(1) // other half to buy
+          const buyAmtBidRSR: BigNumber = issueAmount.div(2).add(2) // other half to buy
           await expectEvents(facadeTest.runAuctionsForAllTraders(rToken.address), [
             {
               contract: backingManager,
@@ -2805,7 +2805,7 @@ describe(`Recollateralization - P${IMPLEMENTATION}`, () => {
 
           const t = await getTrade(backingManager, rsr.address)
           const sellAmtRSR = await t.initBal()
-          expect(await toMinBuyAmt(sellAmtRSR, fp('1'), fp('1'))).to.equal(buyAmtBidRSR.add(1))
+          expect(await toMinBuyAmt(sellAmtRSR, fp('1'), fp('1'))).to.equal(buyAmtBidRSR)
 
           // Should have seized RSR
           expect(await rsr.balanceOf(stRSR.address)).to.equal(stakeAmount.sub(sellAmtRSR)) // Sent to market (auction)
@@ -2841,19 +2841,19 @@ describe(`Recollateralization - P${IMPLEMENTATION}`, () => {
           expect(await basketHandler.status()).to.equal(CollateralStatus.SOUND)
           expect(await basketHandler.fullyCollateralized()).to.equal(true)
           expect(await facadeTest.callStatic.totalAssetValue(rToken.address)).to.equal(
-            issueAmount.add(1)
+            issueAmount.add(2)
           )
           expect(await token0.balanceOf(backingManager.address)).to.equal(0)
           expect(await backupToken1.balanceOf(backingManager.address)).to.equal(issueAmount.div(2))
           expect(await backupToken2.balanceOf(backingManager.address)).to.equal(
-            issueAmount.div(2).add(1)
+            issueAmount.div(2).add(2)
           )
           expect(await rToken.totalSupply()).to.equal(issueAmount)
 
           // Check backing changed
           await expectCurrentBacking({
             tokens: newTokens,
-            quantities: [issueAmount.div(2), issueAmount.div(2).add(1)],
+            quantities: [issueAmount.div(2), issueAmount.div(2).add(2)],
           })
 
           // Check price in USD of the current RToken - Remains the same
@@ -2935,7 +2935,7 @@ describe(`Recollateralization - P${IMPLEMENTATION}`, () => {
 
           // Run auctions - will end current, and will open a new auction to sell RSR for collateral
           // 50e18 Tokens left to buy - Sets Buy amount as independent value
-          const buyAmtBidRSR: BigNumber = sellAmt.div(2).add(1)
+          const buyAmtBidRSR: BigNumber = sellAmt.div(2).add(2)
           await expectEvents(facadeTest.runAuctionsForAllTraders(rToken.address), [
             {
               contract: backingManager,
@@ -2964,7 +2964,7 @@ describe(`Recollateralization - P${IMPLEMENTATION}`, () => {
 
           const t = await getTrade(backingManager, rsr.address)
           const sellAmtRSR = await t.initBal()
-          expect(await toMinBuyAmt(sellAmtRSR, fp('1'), fp('1'))).to.equal(buyAmtBidRSR.add(1))
+          expect(await toMinBuyAmt(sellAmtRSR, fp('1'), fp('1'))).to.equal(buyAmtBidRSR)
 
           // Check state
           expect(await basketHandler.status()).to.equal(CollateralStatus.SOUND)
@@ -3045,11 +3045,11 @@ describe(`Recollateralization - P${IMPLEMENTATION}`, () => {
           expect(await basketHandler.status()).to.equal(CollateralStatus.SOUND)
           expect(await basketHandler.fullyCollateralized()).to.equal(true)
           expect(await facadeTest.callStatic.totalAssetValue(rToken.address)).to.equal(
-            issueAmount.add(1) // 1 attoTokens accumulated
+            issueAmount.add(2) // 2 attoTokens accumulated
           )
           expect(await token0.balanceOf(backingManager.address)).to.equal(0)
-          expect(await backupToken1.balanceOf(backingManager.address)).to.equal(issueAmount.add(1))
-          expect(await rToken.totalSupply()).to.equal(issueAmount.add(1)) // free minting
+          expect(await backupToken1.balanceOf(backingManager.address)).to.equal(issueAmount.add(2))
+          expect(await rToken.totalSupply()).to.equal(issueAmount.add(2)) // free minting
 
           // Check price in USD of the current RToken - Remains the same
           await expectRTokenPrice(rTokenAsset.address, fp('1'), ORACLE_ERROR)
diff --git a/test/integration/mainnet-test/IssuancePremium.test.ts b/test/integration/mainnet-test/IssuancePremium.test.ts
index 47da79ca6..88f8482ef 100644
--- a/test/integration/mainnet-test/IssuancePremium.test.ts
+++ b/test/integration/mainnet-test/IssuancePremium.test.ts
@@ -242,7 +242,7 @@ describeFork(`ETH+ Issuance Premium - Mainnet Forking P${IMPLEMENTATION}`, funct
     const rETHChange = newQs[2].sub(oldQs[2]).mul(fp('1')).div(oldQs[2])
     expect(sfrxETHChange).to.be.closeTo(fp('0.0012'), fp('1e-4')) // sFraxETH +0.12%
     expect(wstETHChange).to.be.closeTo(fp('0.0001'), fp('1e-4')) // wstETH +0.01%
-    expect(rETHChange).to.be.equal(0) // rETH no change
+    expect(rETHChange).to.be.lte(3) // rETH no change
   })
 
   it('from 4.0.0 to 4.0.0 at-peg', async () => {
diff --git a/test/libraries/Fixed.fuzz.test.ts b/test/libraries/Fixed.fuzz.test.ts
index 550b8e662..948332c36 100644
--- a/test/libraries/Fixed.fuzz.test.ts
+++ b/test/libraries/Fixed.fuzz.test.ts
@@ -260,7 +260,7 @@ describe('FixLib Fuzzing', () => {
     await binaryOp(
       [192, 192, 192],
       caller.mul,
-      (x, y) => div(x * y, SCALE, RoundingMode.ROUND),
+      (x, y) => div(x * y, SCALE, RoundingMode.FLOOR),
       null
     )
   })
diff --git a/test/libraries/Fixed.test.ts b/test/libraries/Fixed.test.ts
index 00114889a..ea1528087 100644
--- a/test/libraries/Fixed.test.ts
+++ b/test/libraries/Fixed.test.ts
@@ -504,7 +504,7 @@ describe('In FixLib,', () => {
       const table = commutes.flatMap(([a, b, c]) => [[a, b, c]])
       for (const [a, b, c] of table) {
         expect(await caller.mul(fp(a), fp(b)), `mul(fp(${a}), fp(${b}))`).to.equal(fp(c))
-        expect(await caller.safeMul(fp(a), fp(b), ROUND), `safeMul(fp(${a}), fp(${b}))`).to.equal(
+        expect(await caller.safeMul(fp(a), fp(b), FLOOR), `safeMul(fp(${a}), fp(${b}))`).to.equal(
           fp(c)
         )
       }
@@ -513,13 +513,14 @@ describe('In FixLib,', () => {
     function mulTest(x: string, y: string, result: string) {
       it(`mul(${x}, ${y}) == ${result}`, async () => {
         expect(await caller.mul(fp(x), fp(y))).to.equal(fp(result))
-        expect(await caller.safeMul(fp(x), fp(y), ROUND)).to.equal(fp(result))
+        expect(await caller.safeMul(fp(x), fp(y), FLOOR)).to.equal(fp(result))
       })
     }
 
-    mulTest('0.5e-9', '1e-9', '1e-18')
     mulTest('0.49e-9', '1e-9', '0')
-    mulTest('1.5e-9', '4.5e-8', '68e-18')
+    mulTest('0.9999999999e-9', '1e-9', '0')
+    mulTest('1e-9', '1e-9', '1e-18')
+    mulTest('1.5e-9', '4.5e-8', '67e-18')
 
     it('correctly multiplies at the extremes of its range', async () => {
       const table = [
@@ -531,8 +532,8 @@ describe('In FixLib,', () => {
       for (const [a, b, c] of table) {
         expect(await caller.mul(a, b), `mul(${a}, ${b})`).to.equal(c)
         expect(await caller.mul(b, a), `mul(${b}, ${a})`).to.equal(c)
-        expect(await caller.safeMul(a, b, ROUND), `safeMul(${b}, ${a})`).to.equal(c)
-        expect(await caller.safeMul(b, a, ROUND), `safeMul(${b}, ${a})`).to.equal(c)
+        expect(await caller.safeMul(a, b, FLOOR), `safeMul(${b}, ${a})`).to.equal(c)
+        expect(await caller.safeMul(b, a, FLOOR), `safeMul(${b}, ${a})`).to.equal(c)
       }
     })
 
@@ -626,7 +627,11 @@ describe('In FixLib,', () => {
 
       for (const [a, b, c] of table) {
         expect(await caller.div(a, b), `div((${a}, ${b})`).to.equal(c)
-        expect(await caller.safeDiv_(a, b, FLOOR), `safeDiv_((${a}, ${b}, FLOOR)`).to.equal(c)
+
+        const safeResult = a === MAX_UINT192 ? MAX_UINT192 : c
+        expect(await caller.safeDiv_(a, b, FLOOR), `safeDiv_((${a}, ${b}, FLOOR)`).to.equal(
+          safeResult
+        )
       }
     })
     it('correctly rounds', async () => {
@@ -1195,4 +1200,18 @@ describe('In FixLib,', () => {
       expect(hi).to.equal(bn(0))
     })
   })
+
+  describe('Certora Regression Tests', () => {
+    it('safeMulDiv() may return 0 instead of FIX_MAX', async () => {
+      const xa = 2n ** 191n + 1n
+      const xb = 2n ** 192n - 2n
+      const xc = 2n ** 127n
+
+      expect(await caller.safeMulDiv(xa, xb, xc, CEIL)).to.equal(MAX_UINT192)
+    })
+
+    it('safeDiv() does not correctly propagate the FIX_MAX value', async () => {
+      expect(await caller.safeDiv(MAX_UINT192, bn('2e18'), ROUND)).to.equal(MAX_UINT192)
+    })
+  })
 })