Formal verification of complex software systems such as distributed communication protocols and cyber-physical systems has historically been a significant challenge. Due to fantastic advances in verification engines based on model checkers, static analyzers, proof assistants, and SMT solvers, formal verification is now being adopted in many industrial-scale software development pipelines. However, the pervasive adoption of AI-based components and AI-based programming assistants brings with it new challenges in scalability, program comprehension, and complexity that formal verification tools will have to tackle. In this talk, we will look at verification problems from two very different domains: (1) safety of dynamical systems that use neural networks as controllers, and (2) safety proofs for distributed protocols with asynchronous, message-passing based synchronization. We will present an abstract framework for data-driven and learning-based methods to address these problems. For dynamical systems safety, we show that verification is possible even when we do not have a formal model of the environment/plant dynamics using statistical methods that can give provable (albeit probabilistic) guarantees. For reasoning about distributed systems, we show that we can learn invariants for the system by just reasoning over global traces of the system and without verifying intermediate candidate invariants. Both approaches share the essence of being able to reason in a data-driven fashion assisted by tools from machine learning and AI. The presented methods hope to expand the scope and scalability of formal analysis but may lose out on the hard guarantees that formal tools offer. Nevertheless, the value of these statistical methods is in their utility to system designers and empirical results that may bootstrap more rigorous formal analysis.