diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 10623d9..f4c8470 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -20,21 +20,8 @@ "icon": "lucide-file", "title": "Initial Questions" } - }, - { - "id": "846cc9fc78006404", - "type": "leaf", - "state": { - "type": "release-notes", - "state": { - "currentVersion": "1.8.7" - }, - "icon": "lucide-book-up", - "title": "Release Notes 1.8.7" - } } - ], - "currentTab": 1 + ] } ], "direction": "vertical" @@ -212,7 +199,7 @@ "omnisearch:Omnisearch": false } }, - "active": "846cc9fc78006404", + "active": "fcc28e70ad8acbd2", "lastOpenFiles": [ "Software Engineering/TA Meeting 1.md", "Extracurricular/Misc/Plan.md", diff --git a/Software Engineering/Initial Questions.md b/Software Engineering/Initial Questions.md index 543e034..ac51577 100644 --- a/Software Engineering/Initial Questions.md +++ b/Software Engineering/Initial Questions.md @@ -7,12 +7,17 @@ - What is the expected level of background in Coq or formal methods? - Can you explain the process by which a smart contract's safety properties will be validated formally? - Are there any existing case studies or example proofs we might refer to for a better understanding of the expected output? -- How much of the formal verification process will be based on axioms versus fully constructive proofs? + - Define the contract verification criteria ### Project scope clarifications - Among the seven smart contracts being verified, which ones do you expect us to work on, and why those? - Which technologies are we going to be introduced to, if any? Will we have access to guides for Coq and Solidity? - How do you envision the high-level Coq framework integrating with existing Solidity projects? -- Could you elaborate on the notion of “high-level primitives” (e.g., identity, item, property) and how flexible they need to be for different types of contracts? -- "real numbers and integer approximations"? + + +### Optional + +- How much of the formal verification process will be based on axioms versus fully constructive proofs? +- Could you elaborate on the notion of “high-level primitives” (e.g., identity, item, property) and how flexible they need to be for different types of contracts? +- "real numbers and integer approximations"? \ No newline at end of file