Welcome to evm-dafny Discussions!

[DavePearce]

👋 Welcome!

We’re using Discussions as a place to connect with other members of our community. We hope that you:

• Ask questions you’re wondering about.
• Share ideas.
• Engage with other community members.
• Welcome others and are open-minded. Remember that this is a community we
  build together 💪.

To get started, comment below with an introduction of yourself and tell us about what you do with this community.

[gaxiiiiiiiiiiii]

Hello everyone,

I have been writing Coq as a hobby and have a keen interest in Crypto. I had the opportunity to contribute, albeit briefly, to a project that involved verifying the Tezos Blockchain using Coq. In that project, I wrote a few proofs for basic functions.

I've always thought that formal verification in Ethereum would be exciting, which is why I find the evm-dafny project remarkable! However, I have no experience in smart contract development and only started learning Dafny last month. So, I plan to learn both Dafny and EVM through my exploration of evm-dafny.

My experience with Coq, especially in writing simple mathematical proofs, could be beneficial. For instance, I have recently made a pull request related to the Pow function.

Looking forward to contributing and learning with you all. Thank you.

[DavePearce]

Hey @gaxiiiiiiiiiiii, welcome to DafnyEVM! We are certainly keen to see formal verification of smart contracts become a routine thing, and the DafnyEVM is one step in this direction. However, there remains a lot to be done in terms of making an easy-to-use system. We are doing our best to figure out strategies and approaches here. You can see some example proofs using the DafnyEVM here and here.