search

pirapira / eth-isabelle

A Lem formalization of EVM and some Isabelle/HOL proofs
Other
237 stars 42 forks source link

Test the EVM using Coq to OCaml extraction #410

Open pirapira opened 7 years ago

pirapira commented 7 years ago

Currently, the tests are performed with Lem to OCaml extraction. However, using Coq-to-OCaml extraction, a more direct test can be performed on the Coq extraction.