Many cyber-physical systems (CPSs), including avionics, automotive, robotics, etc., are virtually synchronous distributed control systems with interconnected physical environments. Such CPSs are notoriously hard to verify, due to their combination of nontrivial continuous dynamics, network delays, imprecise local clocks, asynchronous communication, etc. This talk presents effective approaches to design and verify virtually synchronous CPSs, based on automatic formal analysis and model-based software engineering methods. First, the Hybrid PALS pattern reduces the complexity of designing and verifying virtually synchronous CPSs. Second, Synchronous AADL allows engineers to easily design and verify synchronous models within the industrial modeling standard AADL. Third, model checking and SMT-based methods automatically analyze synchronous models based on their formal semantics.