You are right about about "2." and part of "3.". For "2." yes, the smart contracts are indeed simpler (small code, gas limits, closed systems). So we can skip some major hurdles that more general techniques need -- case in point the FB abstract interpretation framework Sparta here yesterday. For "3." we use Z3 (as should everybody :)!) but the target language for synthesis is Solidity. [ Hope you didn't mean Solidity is a DSL, coz that would be a generous interpretation of that word. ]
The initial spec is another smart contract (call it IN), so code and not a formal constraint. We synthesize another smart contract (call it OUT), such that the combination (IN + OUT) behaves well. See work on synthesizing program inverters for the background ideas (http://saurabh-srivastava.com/pubs/pldi11-pins.pdf)