Given that the chief benefit of Cardano Smart Contracts over Ethereum Smart Contracts is formal verification (and thus its implied validity, security, and robustness), is there a non-trivial example of the formal verification of a Smart Contract? Please provide a link... Thanks!
3
-
Unfortunately, it speaks volumes that this question has not been answered. That can be interpreted in two ways - 1. it is a difficult question (granted). 2. There is not a good answer available. :(– Michael DacontaCommented Sep 20, 2021 at 0:09
-
I believe you may find what you are looking for in this video on Formal Verification by Prof. Grigoru Rosu at around 1h17m into the video. youtu.be/ip9ihbMI07U?t=4628– MDeCommented Oct 22, 2021 at 10:31
-
I watched that video at the time specified and it does NOT show a canonical example of smart contract verification. This question has now been unanswered for a month... Is this a case where the theory is nice but has not been proven in a real-world scenario?– Michael DacontaCommented Oct 30, 2021 at 1:53
Add a comment
|
1 Answer
I tried to start a conversation about this here, remains to be seen whether I'll be successful in generating dialogue. But outside of Cardano internals like Ouroboros or the plutus metatheory, the task of formally verifying contracts and dapps built on top of / with those artefacts doesn't appear to me to have a unified solution we can point to yet.
I will update here if my team is successful, we have ideas, but we feel on our own.
-
Very much interested what you guys might come up with. Perhaps, if you have at hand, you could share the details how it's being done for any of internals, like Ouroboros? Commented Dec 3, 2021 at 8:20