Smart Contract verification Framework in Coq

[ataraxiaceleste]

Bas Spitters and Danil Annenkov of Concordium have proposed a novel way of embedding functional smart contract languages into the Coq proof assistant using meta-programming techniques.

Their framework allows for developing the meta-theory of smart contract languages using the deep embedding and provides a convenient way for reasoning about concrete contracts using the shallow embedding. They mainly propose an approach that allows to make a connection between the two embeddings in a form of a soundness theorem.

As an instance of their approach they develop an embedding of the Oak smart contract language in Coq and verify several important properties of a crowdfunding contract.

They claim that they have developed techniques that are applicable to all functional smart contract languages thorough this.

I know that this can be a technically heavy subject.But wondering if any researchers or any other blockchain projects have gone down this route?

[1714852920]

1714852920

[1714852920]

1714852920

[Yogee]

I have no idea what this Coq proof is all about. For starters, can you provide a basic explanation? Maybe provide links too for further reading. 

I know that this can be a technically heavy subject.But wondering if any researchers or any other blockchain projects have gone down this route?

I don't see a lot of technical discussions in this particular board (Altcoin Discussion). Your topic will most likely be ignored and buried here in an hour. I think you have a better chance of getting answers and visibility if you transfer this to the Service Discussion for Altcoins https://bitcointalk.org/index.php?board=198.0 You can find the option to move topic at the bottom left.

[legendsneednotags]

Is this what was being referred to? https://www.cs.au.dk/~spitters/meta.pdf

[ataraxiaceleste]

Is this what was being referred to? https://www.cs.au.dk/~spitters/meta.pdf

Yes correct! This is exactly what I am referring to.

[ataraxiaceleste]

I have no idea what this Coq proof is all about. For starters, can you provide a basic explanation? Maybe provide links too for further reading. 

I know that this can be a technically heavy subject.But wondering if any researchers or any other blockchain projects have gone down this route?

I don't see a lot of technical discussions in this particular board (Altcoin Discussion). Your topic will most likely be ignored and buried here in an hour. I think you have a better chance of getting answers and visibility if you transfer this to the Service Discussion for Altcoins https://bitcointalk.org/index.php?board=198.0 You can find the option to move topic at the bottom left.

The person above posted the link it's exactly that what I'm referring to. I am trying to get a better understanding as well. Would love it f someone experienced and technical can probably share some knowledge on this. I am not looking to provide any service hence, I did not post it in the Service Discussion. I am just trying to pick brain about this research and would like to understand from smart folks who might know better than me and enlighten me.