Model checking, a formal approach to determining whether an abstract model of a system has some desired property, is useful in assessing the dependability of extremely complex agent-based systems. Model checking requires figuring out how systems are modeled, how dependability properties are expressed, and how to automatically determine whether the model has such properties. Using this approach on complex agent-based systems is often considered infeasible, but abstraction techniques can help reduce the level of complexity. Model checking is useful not only for finding flaws in an undependable system but also for determining whether a system meets its dependability objectives. In particular, you can use model checking to focus system testing such that it provides more return for a given level of investment in testing. The application of model checking to UltraLog, a large, complex agent-based system, has demonstrated its usefulness.