@Alistair I think I found one solution.
First, for simplicity, we move away from epoch-less Casper and move back to epochs. Epoch-less was only an improvement because of IMD-related arguments, and without them it only provides a ~20% gain in finality time at considerable cost in complexity, so it may not even be worthwhile.
Now, here is what we do. Let N be the slot in which a client learns that some chain has been justified at a slot more recent than the current head chain’s last-justified-slot. When the client’s clock hits slot N + k, such a chain’s LMD score is bumped up by min(\frac{k}{EPOCH\_LENGTH}, 1).
This allows us to argue as follows. Because on average, the attacker can only flip the winner of the “highest justified epoch” rule once per epoch, eventually there will be a period of one epoch during which the attacker cannot flip the winner. During this period, whatever the chain that was head at the start of the period will have 100% support in the LMD fork choice. Hence, there will be a period of one more epoch until any other chain can take over, and during this period the chain can get justified.
The more general class of solutions here basically has to do with adding some sort of “temporary stickiness” to the LMD fork choice, sticky enough to allow a head to be justified but temporary enough to allow the FFG plausible liveness proofs to still work.