Formal verification on Huff

[clarus]

Hello,

How can we help apply formal verification on the Huff language? Is the verification of the weierstrudel smart contract a good starting point? Would the huff-rs compiler itself benefit from a formal verification of its code? Thanks.

Guillaume Claret for https://formal.land/

[Philogy]

My current approach to formally verifying Huff code bases such as METH is by leveraging hevm to verify a spec written in Solidity: https://github.com/Philogy/meth-weth/blob/main/test/fv/METH.fv.sol As of this writing hevm is missing some features (such as symbolic pranks) but dxo (hevm dev) has told me these features are coming soon™️.