Hi all,

Only one year after this message, I found interest in building a blockchain and smart contracts in OCaml. May I know how far is the EVM formalisation in Coq?

There aren't many materials / blockchain implementations in OCaml but I found some interesting links:

https://github.com/LaurentMazare/btc-ocaml

http://www.liquidity-lang.org/

https://github.com/tezos/tezos

https://github.com/pirapira/eth-isabelle

https://github.com/pirapira/ethereum-formal-verification-overview

I would like to know more if anyone has more information.

Thanks,
Viet

On 10 October 2016 at 15:00, Van Chan Ngo <chan.ngo2203@gmail.com> wrote:
Hi Arthur,

It is interesting to implement blockchains in functional language like OCaml. I am happy to hear more about this project.

FYI, a related work, we are in progress to formalize the Ethereum Virtual Machine (EVM, the running environment of smart contracts) in Coq.

Best,
-Chan


On Oct 5, 2016, at 11:59 PM, Arthur Breitman <arthurb@tezos.com> wrote:

If you find this intriguing and enjoy working in OCaml, please reach out: we're hiring! If you lean on the academic side and have experience with formal verification, reach out as well! We'd be interested in proving the correctness of some aspects of the protocol or sponsoring research in the field in general (within our modest means).





--
Kind regards,
Viet