In the twenty-five years since its invention, model checking has evolved into a powerful framework for the analysis of computer hardware and software. The integration of model checkers into the industrial development chain has raised new methodological questions about model checking, including the use of model checkers to analyze underspecified or unknown systems and the truthfulness of positive verification results. In this paper, we survey recent technical approaches to these questions – temporal logic query solving and vacuity detection – both of which transcend the classical picture of model checking. We focus on temporal logic queries with unique strongest solutions, describe fragments of CTL and LTL query languages with this property, a symbolic query solving algorithm for CTL, and an application of query solving to vacuity detection.