Actually, on the runtime-side I don't think we get any benefit to use generate_proof() and verify_proof() to prove the bad vote. It is enough to show the bad vote mmr_root is different than the on-chain one.

Using verify_leaves_proof() even requires us to have the leaves, so it just adds complexity for no benefit.

Please correct me if I'm wrong, but I don't think checking misbehaviour at the voting level is sufficient (nor even necessary). What ultimately matters for attacking the bridge is the signatures on the payload (and here equivocating against what's finalised via GRANDPA).
Going through the voting process to aggregate this payload using substrate's p2p layer is convenient, but not necessary to construct this payload: an attacking majority can also coordinate this externally without relying on Polkadot's gossiping.

My intuition so far is that we should be checking the signatures in the payload updating the smart contract's MMRRoot (https://github.com/Snowfork/snowbridge/blob/main/core/packages/contracts/src/BeefyClient.sol).
Just my current thoughts - will update after thinking about this more deeply.

That’s right, the important part here is offering the pallet::call so that relayers can submit proofs of misbehavior on the source chain when detecting invalid justifications posted to target chain.

The BEEFY voter gossip fisherman is just nice-to-have.

This issue tracks the machinery we need to have in place on Polkadot side to be able to accept a “invalid-fork-vote” proof of some sort, verify it on-chain and initiate slashing if valid.

Separate work (bridge repo) needs to go in the relayers (or maybe even dedicated fishermen) that follow both sides of the bridge and look for source_chain.header_at(target_chain.best_source_header_number()).hash() != target_chain.best_source_header_hash(). If that happens, they can get the offending justification that caused it from transactions, build “invalid-fork-vote” proof and post it to Polkadot.