diff --git a/certora/specs/RewardsStreamerMP.spec b/certora/specs/RewardsStreamerMP.spec index 366cab2..cefbfc5 100644 --- a/certora/specs/RewardsStreamerMP.spec +++ b/certora/specs/RewardsStreamerMP.spec @@ -38,3 +38,6 @@ invariant sumOfBalancesIsTotalStaked() invariant accountMPLessEqualAccountMaxMP(address account) to_mathint(getAccountMP(account)) <= to_mathint(getAccountMaxMP(account)); +invariant accountMPGreaterEqualAccountStakedBalance(address account) + to_mathint(getAccountMP(account)) >= to_mathint(getAccountStakedBalance(account)); +