This has me wondering about converting law into source code, running it through something like Coq or Agda and finding logical contradictions that need resolution.

Not sure that would be feasible (e.g. if those languages would even be capable of doing such a thing), or how much computing power you'd need to churn through however many thousands of pages of something like the US Code and process that all.