MrChico

Verification of set up process / authorization exhaustiveness

8

The security of dss relies heavily on the fact certain functions are only callable by certain interface contracts. So far, all of our specs have only assumed certain addresses have...

The reachability proofs of [dss.md](dss.md) can be thought of as axiomatically defining the theory `k-dss` that is the dapp that is MCD. We are working with two standard models (we...

When it comes to ensuring global properties of the system, we can by induction prove global "accounting invariants" using the `ensures` clause and `requires` clauses. I imagine a procedure that...

Generalize registry

2

The registry makes a lot of assumptions on the structure of ilks, their adapters and liquidation methods. This makes it difficult to register non-standard ilks and their adapters, such as...

No way to cancel orders in the new UI

1

Hey, I would like to cancel an order placed to the senior tranche, before a successful solution has been submitted. The contracts admit this but the frontend does not allow...

Add psm

2

My research suggests it's at 0x0A59649758aa4d66E25f08Dd01271e891fe52199 but I would like to get confirmation here