We describe the Arís system for creating new formal specifications for source code by transferring existing specifications to similar implementations. We show the code graphs underlying its operation, graph matching supports retrieval, and pattern completion enables transfer of specifications to new implementations. A theorem prover formally verifies the new specifications.