I was trying to see if there is a way to fix this- "no tax code can close all loop holes", and my first thought was Formal methods- and lo and behold Google points me to http://snapl.org/2015/abstracts/hsu.pdf

It sure looks promising. But still wondering if it has been applied in practice.