Possibly could be this:

https://www.youtube.com/watch?v=EshxZVMURt4

https://popl18.sigplan.org/details/POPL-2018-papers/3/Formal...

The city is Los Angeles, though the content doesn't seem to match precisely what was mentioned.

I found this via a Google search for `conference convert legal phrases into code "theorem" bug`, which returned the following paper:

https://hal.inria.fr/hal-03159939v2/document

I then checked the citations of that paper for anything matching.

Yes, it's the POPL talk. Thanks for digging it up for me. I had a nice conversation with her after her talk about her work.

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 ^_^;