There is a growing trend toward human-cyber-physical systems (h-CPS), where systems collaborate or interact with human operators to harness complementary strengths of humans and autonomy. Examples include self-driving cars that need the occasional driver intervention, and industrial robots that work beside or cooperatively with people. The societal impact of h-CPS, however, is contingent on ensuring safety and reliability. Several high-profile incidents have shown that unsafe h-CPS can lead to catastrophic outcomes. Formal methods enable the model-based design of safety-critical systems with mathematically rigorous guarantees. However, the research area of formal methods for h-CPS is still in its infancy. The goal of this research is to expand formal methods toward the joint modeling and formal analysis of CPS and human-autonomy interactions, accounting for the uncertainty and variability of human behaviors, intentions, and preferences.