I remember this talk! The speaker recommended doing this with the tax code because it was one of the most mechanical -- very little inherent ambiguity, there's just a lot of surface area to cover, so it's a great candidate for actually applying formal methods to.
You'll probably remember me being there, I was the nerdy guy.
Oh wait, everyone was a nerdy person!
I was starstruck enough just sitting next to Daniel Friedman ^_^;