A place for talking about the Ethereum Virtual Machine on Farcaster.

Where are we at with formal verification of Solidity code? Any new state of the art resources?

Paging @karma, who works on https://github.com/a16z/halmos.

From my perspective as a dev, it's getting easier to use them in real projects alongside fuzz and unit tests. A few newer tools:

Halmos: https://github.com/a16z/halmos
Kontrol: https://docs.runtimeverification.com/kontrol/
Certora: https://docs.certora.com/

/// echo.xyz ///
math && econ && cryptography

I'm eth newbie..just learning
(working on @farcaster)

terminally.online

Awesome, thanks for the resources! I'm doing some formal verification work for zk proofs and I wanted to see how far I can get with Solidity as well. This looks like a good place to start

happy to help if you run into issues with halmos. You should feel right at home if you're already used to writing foundry tests

There is also hevm, which is actively developed by the EF