search

makerdao / k-dss

formal verification of multicollateral dai in the K framework
GNU Affero General Public License v3.0
14 stars 11 forks source link

Spotter proofs #6

Closed kmbarry1 closed 5 years ago

kmbarry1 commented 5 years ago

Exhaustive spec coverage for Spotter contract.

gbalabasquer commented 5 years ago

If they are passing, I'd say let's merge it directly.

kmbarry1 commented 5 years ago

They pass, at least on my machine :), so I will go ahead and merge.