BlueMatt wrote a pretty extensive agreement testing framework and discovered several corner cases that were not previously known. He's generally of the opinion that achieving a correct reimplementation is more or less intractable. His approach made progress, especially in unearthing weird behaviours, but doesn't result in great confidence of soundness; and doesn't show an implementation free of its own buts not related to non-obvious behavior in Bitcoin Core.  Our strategy in Bitcoin Core as of late has been toward compartmentalizing and simplifying in order to make code reuse more reasonable; and also get things structured to be more agreeable to approaches that would possibly make formal analysis more realistic, but thats a long term effort.