yul-semantics
mentioned above in some regards. Check it out here https://github.com/mmalvarez/Yul-Isabelle
Tomorrow Algorand is hosting a live webinar on implementing the world’s first CBDC. I have submitted a few questions and will be attending. This is a great way to spend your quarantine :)
Register and submit questions here: https://register.gotowebinar.com/register/5273854108710515471
xvwx
@leo put together a very nice overview here: https://github.com/leonardoalt/ethereum_formal_verification_overview
xvwx
in terms of tools deployed in the wild, I would say that the k framework has seen the most usage
BLOCKHASH
for randomness (related to eth1+eth2 merge research) and had the idea of looking for bytecode where the blockhash is subsequently hashed to an int. anyone know if there's a rigorous way to do this search?
We integrated hevm's symbolic execution features into its unit testing framework. This lets you formally verify properties directly in Solidity, using almost exactly the same syntax as writing a property based test.
More details here: https://fv.ethereum.org/2020/12/11/symbolic-execution-with-ds-test/#setting-up-the-environment
ETH2-RESEARCH
section. Enjoy!