We propose the trace modality, a concept to uniformly express a wide range of program verification problems. To demonstrate its usefulness, we formalize several program verification problems in it: Functional Verification, Information Flow Analysis, Temporal Model Checking, Program Synthesis, Correct Compilation, and Program Evolution. To reason about the trace modality, we translate programs and specifications to regular symbolic traces and construct simulation relations on first-order symbolic automata. The idea with this uniform representation is that it helps to identify synergy potential—theoretically and practically—between so far separate verification approaches.