user2503: 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!

user4107: 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.

2503: <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>
 4107: <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>
