My question now is whether to put time into Halmos or Certora? Which one will "win" in the Dev community? Halmos seems easier to use & learn, but at the cost of depth & breadth of features compared to Certora.

Bankless citizen. Dev retooling for web3 with focus on Solidity and smart contract auditing.

Is this the case with Halmos vs. Certora? I think it might be an 80/20 thing. If Halmos can give you 80% of what the average FVer needs, the ease of use wins out - with only most advanced going to Certora.

I'm currently leaning Halmos. I see it as similar choice to fuzzing with Foundry vs. Echidna. I haven't dove into Echidna to see what it adds beyond Foundry. The reason I haven't is that it's so easy to fuzz from forge directly. I likely won't look at Echidna until I hit a wall.