Explore a comprehensive tutorial on Vehicle, a functional DSL for specifying neural network properties. Learn how to write high-level specifications that work seamlessly with training and verification tools, independent of specific neural network platforms. Discover techniques for expressing various specifications, compiling them into Tensorflow graphs for loss functions, generating queries for network verifiers, and cross-compiling to Agda. Gain insights into the Vehicle specification language and type system, and participate in hands-on exercises to reinforce your understanding. Delve into technical challenges and outstanding problems in neural network verification, and understand how Vehicle addresses the need for verifiably safe machine learning components in critically safe software.