We view through a verification lens the evolution of program specifications---from partial and total correctness, through safety and liveness properties, and culminating with hyperproperties. The exposition will include a new approach to verifying a large class of hyperproperties. That approach involves describing systems and their properties in the temporal logic TLA. The reduction of hyperproperties to TLA properties generalizes self-composition to a class of hyperproperties that includes all those we have seen to express security conditions and to express properties of programs.
*Joint work both with M. Clarkson and with L. Lamport is being described.