Formal specification provides a uniquely readable description of various aspects of a system, including its temporal behavior. This facilitates testing and sometimes also automatic verification of the system against the given specification. We present a logic-based formalism for specifying learning-enabled autonomous systems, which involve components based on neural networks. The formalism applies temporal logic with predicates for characterizing events and uses universal quantification to allow enumeration of objects. While we have applied the formalism successfully to two complex use cases, several limitations such as monitorability or lack of quantitative satisfaction also reveal further improvement potential.