Watch this 29-minute conference talk from CPP 2025 where researchers from Rice University present their Coq formalization of regular expressions with lookaround capabilities. Learn about their purely functional algorithm for matching expressions with lookarounds that runs in linear time relative to both the regular expression size and input string length. The presentation covers the verification of correctness for this algorithm and includes experimental results supporting their complexity analysis. This is reportedly the first formalization of a linear-time matching algorithm for regular expressions with lookarounds, making it a significant contribution to the field. The talk explores concepts including lookbehind, lookahead, NFAs, and regex implementation techniques, presented at the ACM SIGPLAN and SIGLOG sponsored CPP (Certified Programs and Proofs) conference.