Skip to content
This repository has been archived by the owner on Apr 18, 2023. It is now read-only.

Issues: makerdao/mkr-mcd-spec

44 Open 49 Closed
44 Open 49 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Course part 3
#269 opened Mar 21, 2022 by 0xverif
5 of 6 tasks
Get Vat proofs running on the summarizer
#267 opened Feb 28, 2022 by 0xverif
7 of 12 tasks
Reverification Effort for KDSS proofs
#266 opened Feb 24, 2022 by 0xverif
2 tasks
1
Implement and test simple properties
#265 opened Feb 24, 2022 by 0xverif
1 task
Taxonomy of high-level properties relevant for CDP lending protocols (start focusing on simpler properties such as ESM)
#263 opened Feb 14, 2022 by 0xverif
1 of 2 tasks
@0xverif
High-level model property proofs
#262 opened Feb 11, 2022 by 0xverif
3 tasks
@0xverif
Educational Content
#261 opened Feb 11, 2022 by ehildenb
1 of 4 tasks
@0xverif
KProve Web applied to the Vat proofs in the KEVM regression test suite
#260 opened Feb 11, 2022 by 0xverif
1 of 7 tasks
Summarizer on Maker Contracts
#259 opened Feb 11, 2022 by 0xverif
1
Make it possible to use abstract storage state over KEVM
#251 opened Jun 30, 2021 by ehildenb
1
@0xverif
Look at #mkCall and #mkCreate in KEVM for doing calls
#247 opened Jun 15, 2021 by ehildenb
@0xverif
Subsort all step types in mkr-mcd-spec
#246 opened Jun 15, 2021 by ehildenb
1
@0xverif
Setup KLab to handle immutables (for update to Liq-2.0 branch)
#235 opened Mar 10, 2021 by ehildenb Update K-DSS
@kmbarry1
Experiment with simple mkr-mcd-spec specifications
#233 opened Mar 10, 2021 by ehildenb High-level property verification
Specify and prove some of the properties in the mathematical model defined in #229
#232 opened Mar 9, 2021 by WilfredTA
Act Specifications for liquidations 2.0
#231 opened Mar 9, 2021 by WilfredTA
@kmbarry1 @WilfredTA
Attempt making a model in CadCAD of the Vat
#230 opened Mar 2, 2021 by ehildenb
High-level english + Math model of the MKR system
#229 opened Feb 23, 2021 by ehildenb High-level property verification
@kmbarry1 @WilfredTA
1
Ship a docker image with KEVM pre-installed
#228 opened Feb 17, 2021 by ehildenb Improve Accessibility to Tooling
High-level design of refinement proofs between mkr-mcd-spec and KEVM+DSS
#222 opened Jan 27, 2021 by ehildenb High-level property verification
Modularize proof structure to one contract per file (for more modular proof generation/discharge)
#221 opened Jan 27, 2021 by ehildenb Improve Accessibility to Tooling
Setup CI server for K-DSS proofs
#220 opened Jan 27, 2021 by ehildenb Improve Accessibility to Tooling
Setup auto-generation of "proven" theorems in repo for quicker starting on later proofs
#219 opened Jan 27, 2021 by ehildenb Improve Accessibility to Tooling
Classify properties we want to express
#218 opened Jan 27, 2021 by WilfredTA High-level property verification
@WilfredTA
K Performance Improvements enhancement New feature or request
#217 opened Jan 27, 2021 by WilfredTA Update K-DSS
ProTip! What’s not been updated in a month: updated:<2024-08-20.