Does an AI (or software) exist that can automatically write software based on a formal specification of the software?
I think that the answer to your question is yes. In the article New A.I. application can write its own code, the authors state
Computer scientists have created a deep-learning, software-coding application that can help human programmers navigate the growing multitude of often-undocumented application programming interfaces, or APIs.
Designing applications that can program computers is a long-sought grail of the branch of computer science called artificial intelligence (AI). The new application, called Bayou, came out of an initiative aimed at extracting knowledge from online source code repositories like GitHub. Users can try it out at askbayou.com.
The paper Neural Sketch Learning for Conditional Program Generation may also be useful.
There's Neural Program Synthesis, which can be used to generate a piece of code. Please, have a look at the article Neural Program Synthesis by Microsoft for an overview of the field.
The other answers cover modern work on this, but it's not even a new topic!
Koza's work in 1992 led to whole sub-fields doing this. The techniques are widely used, robust, and well understood. They're just very computationally expensive. Enough so that most of the time you're better off just hiring a programmer to do it.