This chapter considers the complexities engineers encounter when designing, building and deploying cloud-native software and examples of the models that engineers can use to help control the complexity. The chapter begins by reviewing the causes of complexity in cloud software. It also also discusses problems inherent in all distributed systems. The chapter describes operational and analytical models, including those that use first-order logic, temporal logic, graph theory, and state machines. It presents an example of a graph model that can be used to detect potential deadlocks, and a modified example that detects dependencies among modules and specifies a startup sequence. The chapter then considers TLA+, a modeling system based on temporal logic. It presents an example of a TLA+ specification for proxy communication, a pattern that appears in many cloud systems. It shows an example output from a TLA+ model checker. The chapter explains that because a mathematical model that uses logic resembles a mathematical proof more than an algorithm, the use of such models may introduce additional complexity in the software design process.