Where are the machine-checked proofs?

Developers
1

Hi Cardano folks,

Where can I find formal, machine-checked, proofs of Cardano’s properties?
E.g. I heard that parts of Daedalus have now been formally verified, but I don’t see anything that looks like a proof (e.g. something in Agda, Coq, etc.) in the GitHub project.

Sorry if this is a newb question - I just joined the forum today!

Edit: Charles posted some links here.

6 Likes
2

Obviously was not a newb Question :wink:
Charles does not answer all developer questions that arise, I hope he directed you to what you were looking for. :+1:

1 Like
3

Good stuff hope to get your thoughts after you read them.

4

https://www.reddit.com/r/cardano/comments/a4q8y8/where_are_the_formal_machinechecked_proofs/ebgto8q/

https://bitbucket.org/wkawin/ouroboros

https://cardanodocs.com/technical/formal-specification-for-a-cardano-wallet/

UPD:

Ah, sorry, didn’t notice you have already linked the Reddit answer )

2 Likes