We present a first-order linear-time temporal logic for reasoning about the evolution of directed graphs. Its semantics is based on the counterpart paradigm, thus allowing our logic to represent the creation, duplication, merging, and deletion of elements of a system as well as how its topology changes over time. Besides presenting a set-based semantics using graphs of graphs as models, we provide a computer-assisted formalisation of these constructions using the proof assistant Agda. We then introduce a positive normal forms presentation, thus simplifying the actual process of verification of properties, and we round up the paper by highlighting the crucial aspects of our formalisation and the practical use of quantified temporal logics in a constructive proof assistant.