Can you speak more on why ‘making them actually consistent in production is a completely different story’?
Curious because I’ve been learning TLA+ recently and interested to more know about cases where an algorithm has been proven but actual an implementation of it fails.
Advice from someone who had a similar choice and went the startup route: choose the Google option. It will not only open doors for you for all your future jobs, but you can invest the money now and create a nice start for yourself.
There will never be any shortage of interesting startups to work for in the future.