The Dutch tax authority has developed RegelSpraak a controlled natural language for defining tax rules that is also formally specified and compilable to several targets.
There is a video of the team presenting how they built the DSL for tax rules in the JetBrains MPS language workbench from the MPS conference.