EVM-Dafny
I have just known this project which seems to have quite clear and nice architecture.
Evm-dafny enables us to be free from bugs by implementing EVM semantics via Dafny langauge.
Elaboration of verification part is thrown to the Dafny language and we can thank both synthetic verification and analytic verification when we write contract using EVM-Dafny. I would like to try it.
Has anyone already tried it ?
There are some posts around EVM-Dafny language.