IMO the solution might be to write our own resolver that we can reason carefully about and prove works in a way that is amenable to this system