Towards provably correct system synthesis and extension