rndquu

This task is not ready because we first need to update UI to follow the diamond contracts deploy

> > This task is not ready because we first need to update UI to follow the diamond contracts deploy > > @rndquu is there an update on this? @molecula451...

> * [Add UI diamond hook #731](https://github.com/ubiquity/ubiquity-dollar/issues/731) appears to be completed! The UI is still broken so the current issue is still blocked I will add new UI related tasks...

> Hi rndqnuu there is another potential monitor solution available at mainnet, https://cyvers.ai/ Updated description

The `isRedeemPaused` works pretty much the same way as `collateralEnabled` ([one](https://github.com/sherlock-audit/2023-12-ubiquity/blob/d9c39e8dfd5601e7e8db2e4b3390e7d8dff42a8e/ubiquity-dollar/packages/contracts/src/dollar/libraries/LibUbiquityPool.sol#L410-L413), [two](https://github.com/sherlock-audit/2023-12-ubiquity/blob/d9c39e8dfd5601e7e8db2e4b3390e7d8dff42a8e/ubiquity-dollar/packages/contracts/src/dollar/libraries/LibUbiquityPool.sol#L481-L484)). So if some user requested collateral via [redeemDollar()](https://github.com/sherlock-audit/2023-12-ubiquity/blob/d9c39e8dfd5601e7e8db2e4b3390e7d8dff42a8e/ubiquity-dollar/packages/contracts/src/dollar/libraries/LibUbiquityPool.sol#L399) but hasn't [collected](https://github.com/sherlock-audit/2023-12-ubiquity/blob/d9c39e8dfd5601e7e8db2e4b3390e7d8dff42a8e/ubiquity-dollar/packages/contracts/src/dollar/libraries/LibUbiquityPool.sol#L476) it (because the protocol paused redeems) then...

> I heard great things about Certora. If you search the ubiquity org for me writing the term "Certora" you can see that I listed a security checklist with a...

> I heard great things about Certora. If you search the ubiquity org for me writing the term "Certora" you can see that I listed a security checklist with a...

> They asked me to schedule a call with them. I am under the impression that we can bring on one of their engineers to implement things. > > If...

> Still an active issue? Yes

@alexandr-masl Basically we have 2 invariants that should be proved ([one](https://github.com/ubiquity/ubiquity-dollar/blob/20799bedf5ee4d40d2863653f7bc2fe68a2ce3fa/packages/contracts/test/invariant/diamond/facets/UbiquityPoolFacet.invariant.t.sol#L177), [two](https://github.com/ubiquity/ubiquity-dollar/blob/20799bedf5ee4d40d2863653f7bc2fe68a2ce3fa/packages/contracts/test/invariant/diamond/facets/UbiquityPoolFacet.invariant.t.sol#L195)). In some cases formal verification is not possible if there're too many code paths to prove. Not sure...