In this paper, we present a case study on modeling and verification of Spiking Neural Networks (SNN) using Satisfiability Modulo Theory (SMT) solvers. SNN are special neural networks that have great similarity in their architecture and operation with the human brain. These networks have shown similar performance when compared to traditional networks with a comparatively lesser energy requirement. We discuss different properties of SNNs and their functioning. We then use Z3, a popular SMT solver to encode the network and it’s properties. Specifically, we use the theory of Linear Real Arithmetic (LRA). Finally, we present a framework for verification and adversarial robustness analysis that are shown to work on the IRIS and MNIST benchmarks.