I suppose a trojan designed for a specific compiler is hard enough to make. Having it hijack a model checker as well, in order to conceal itself from resulting

I suppose a trojan designed for a specific compiler is hard enough to make. Having it hijack a model checker as well, in order to conceal itself from resulting models, would be a giant leap more difficult. So, you are still risking it if you have nation-state adversaries, but not if they are script kiddies.