Stepwise refinement is crucial in software development, but typical refinement relations like stable failures refinement and failures-divergences refinement have drawbacks in how they deal with divergences. Mauw and Voorhoeve’s impossible futures preorder has more pleasing properties, yet lacks a practical verification algorithm. This paper presents a novel algorithm for checking impossible futures refinement, enhanced by antichains and further optimisations.