Formal methods in a startup?

I've been studying formal specification and verification methods (Lamport's TLA+/TLC) recently. It's a very interesting (very theoretical) subject, but I wonder about its practicality.

Are there any known potentially useful applications to startups? Most seem to rush into coding without specifying the behaviors of the system they're developing to stay agile. I don't know of any that employ sufficiently complex algorithms where verifiable correctness is sufficiently critical, but I'm new to the field.