We describe recent work on the Aris system that creates and verifies new formal specifications for pre-existing source code. We describe Aris in terms of the abductive reasoning system that suggest possible specifications and then uses an existing deductive verifier to evaluate these creations. This paper focuses on the abduction system that creates new formal specifications by leveraging a small set of inspiring artefacts to augment a subset of candidate problems. This employs knowledge graphs to represent the raw data (i.e., source code), discovering latent similarities between graphs using a graph-matching process. Results are presented for the C# programming language with novel creations and its sister language called Code Contracts. We outline ampliative creativity, whereby newly created artefacts drive subsequent creative episodes beyond the initially perceived limitations. We also outline some recent work towards transferring specifications between the C# and Java programming languages.