<p>I tried to start a conversation about this <a href="https://github.com/input-output-hk/plutus/issues/4180" rel="nofollow noreferrer">here</a>, 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 <em>on top</em> of / with those artefacts doesn't appear to me to have a unified solution we can point to yet.</p>
<p>I will update here if my team is successful, we have ideas, but we feel on our own.</p>

CC BY-SA 4.0
2021-12-03T08:20:08.897Z
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?
andycandy
CC BY-SA 4.0
2021-11-02T18:27:45.503Z
2021-11-02T18:27:45.503Z
Quinn Dougherty
<p>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!</p>

CC BY-SA 4.0
2021-09-20T00:09:06.007Z
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 Daconta
CC BY-SA 4.0
2021-10-22T10:31:55.200Z
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. https://youtu.be/ip9ihbMI07U?t=4628
MDe
CC BY-SA 4.0
2021-10-30T01:53:42.237Z
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 Daconta
<smart-contract><haskell><security><plutustx>
Canonical example of Smart Contract Verification?
# Canonical example of Smart Contract Verification?

(Asked by: username_0 on 2021-09-03)

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!

**Tags:** smart-contract, haskell, security, plutustx
> **Comments:**
> **username_0**: 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.  :(  
> **username_1**: 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. https://youtu.be/ip9ihbMI07U?t=4628  
> **username_0**: 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?  

---

## 1 answers

### Answer by username_2 on 2021-11-02. Score: 1

I tried to start a conversation about this [here](https://github.com/input-output-hk/plutus/issues/4180), 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.

> **Comments:**
> **username_3**: 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?  

---

