Does an AI exist that can write software based on a formal specification?
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.