Hi Pieter,
Let's take a step back first. If we believe that malicious hardware
wallets are big enough of a concern, then signing is only part of the
problem. The other issue is key generation. The PRG from which the seed
is derived can be malicious, e.g., just H(k_OO,counter) for a key k_OO
chosen by the hardware manufacturer. I haven't seen an argument why
attacks during the signing model should more realistic than attacks
during key generation, so I'd be very hesitant to deploy anti-covert
channel singing protocols without deploying protocols for key
generation that are secure in the same attacker model.
Public keys are deterministic and can be spot checked. In fact, AFAIU if hardened HD key derivations are not used, then spot checking is very easy.
While spot checking isn't ideal, my original concern with the synthetic none standard proposal was that it is inherently non-deterministic and cannot ever be spot checked. This is why anti-covert signing protocols are so important if we are going to use synthetic nonces.