Thanks Van Chan for sharing. I also found a solution that automatically computes the gas used by breaking down into basic computations. They are Zen Protocol: https://www.zenprotocol.com . They use F* that is very closely related to OCaml/F# to achieve their goal. So if you want to find upper-bound for EVM, I think their whitepaper is a good start. Regards, Viet On 26 December 2017 at 14:03, Van Chan Ngo wrote: > Hi Viet, > > I did not work on the formalization of EVM a while ago due to other work > (automatic resource bound analysis for probabilistic programs > https://channgo2203.github.io/pdfs/cmutr02.pdf) > The following is the implementation (not completed) on Github. > https://github.com/channgo2203/fevm > > However, we are working on the other aspect of EVM code analysis. We want > to statically infer an upper-bound on the amount of gas > consumption for all inputs (input arguments and storage configurations). > This analysis is based on our previous research on resource bound > analysis for both imperative and functional programs. > > We translate EVM byte-code into a kind of control flow graph (CFG). > However, due to the unstructured and low level of EVM, I suppose it is > more convenient to infer upper-bound on gas consumption at Solidity source > code provided that we have a good gas consumption model for > Solidity language constructs. > > Best, > -Van Chan > > > > > On Mon, Dec 25, 2017 at 8:28 AM, Viet Le wrote: > >> 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 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 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 >> > > -- Kind regards, Viet