diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec
index ad833cbf1..45c535187 100644
--- a/certora/specs/Health.spec
+++ b/certora/specs/Health.spec
@@ -46,6 +46,68 @@ function summaryMin(uint256 a, uint256 b) returns uint256 {
     return a < b ? a : b;
 }
 
+// Check that without accruing interest, no interaction can put an healthy account into an unhealthy one.
+// This rule times out for liquidate, repay and borrow.
+rule stayHealthy(env e, method f, calldataarg data)
+filtered {
+    f -> !f.isView &&
+    f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector &&
+    f.selector != sig:repay(MorphoHarness.MarketParams, uint256, uint256, address, bytes).selector &&
+    f.selector != sig:borrow(MorphoHarness.MarketParams, uint256, uint256, address, address).selector
+}
+{
+    MorphoHarness.MarketParams marketParams;
+    MorphoHarness.Id id = libId(marketParams);
+    address user;
+
+    // Assume that the position is healthy before the interaction.
+    require isHealthy(marketParams, user);
+    // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec.
+    require marketParams.lltv < 10^18;
+    // Assumption to ensure that no interest is accumulated.
+    require lastUpdate(id) == e.block.timestamp;
+
+    priceChanged = false;
+    f(e, data);
+
+    // Safe require because of the invariant sumBorrowSharesCorrect.
+    require borrowShares(id, user) <= totalBorrowShares(id);
+
+    bool stillHealthy = isHealthy(marketParams, user);
+    assert !priceChanged => stillHealthy;
+}
+
+// Check that users cannot lose collateral by unauthorized parties except in case of an unhealthy position.
+rule healthyUserCannotLoseCollateral(env e, method f, calldataarg data)
+filtered { f -> !f.isView }
+{
+    MorphoHarness.MarketParams marketParams;
+    MorphoHarness.Id id = libId(marketParams);
+    address user;
+
+    // Assume that the e.msg.sender is not authorized.
+    require !isAuthorized(user, e.msg.sender);
+    require user != e.msg.sender;
+    // Assumption to ensure that no interest is accumulated.
+    require lastUpdate(id) == e.block.timestamp;
+    // Assume that the user is healthy.
+    require isHealthy(marketParams, user);
+
+    mathint collateralBefore = collateral(id, user);
+
+    priceChanged = false;
+    f(e, data);
+
+    mathint collateralAfter = collateral(id, user);
+
+    assert !priceChanged => collateralAfter >= collateralBefore;
+}
+
+// Check that users without collateral also have no debt.
+// This invariant ensures that bad debt realization cannot be bypassed.
+invariant alwaysCollateralized(MorphoHarness.Id id, address borrower)
+    borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0;
+
 // Checks that passing a seized amount input to liquidate leads to repaid shares S and repaid amount A such that liquidating instead with shares S also repays the amount A.
 rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) {
     MorphoHarness.Id id = libId(marketParams);