We won't be formally verifying millions of LOC anytime soon, don't get your hopes that high up. ...but we will be modelling those 5-10kLOC modules across multi

We won't be formally verifying millions of LOC anytime soon, don't get your hopes that high up. ...but we will be modelling those 5-10kLOC modules across multiple services doing critical business logic or distributed transactions. This has been unthinkable a couple months ago and today is a read-only-Friday experiment away (try it with a frontier model and you'll be surprised).