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