I wrote Rob Pike's simple regex from the "Practice of Programming" in Ada/SPARK and it blew my mind that I actually managed to prove an absence of runtime error (guaranteed no overflow or out of bounds).
I have my copy of "Practice of Programming" about to be delivered. Is your regex implementation available somewhere?
edit: if you feel like sharing your code and experience there, I'm pretty sure some people would be interested.
The amazing thing to me is that Ada code can call SPARK code just fine, and there's crates of SPARK code in Alire that you can use. It's a huge boost of confidence in the quality of a library that you're using when it has some form of verification.