If TLA+ really does let you prove your program is bugless, then maybe it is something to look into for cars, airplanes, medicine, etc. For the rest of us, who still wrestle with complexity but probably would't accidentally kill someone, here are some simpler aids:

1. Don't put a computer there. My microwave doesn't need to be digital. It needs two dials, time and power. My mother's washing machine can be controlled by smartphone. How useful is that, since you can't load it by phone? Computerized light switches are another example of something that sounds nifty, but the complexity outweighs the benefit by a thousand to one. Plus, you need the exercise. Get up and just hit the light switch. I question whether a car needs any computer at all, especially if the car is electric, ironically. My ignorance will allow that maybe a computer can mix air and gas better than a purely mechanical fuel-injection system. But since an electric motor is simpler, this advantage disappears.

Don't get me wrong. I like computers. But I think computation should be gathered instead of spread all over the place. I like my smartphone and my laptop (pure computers). And I would prefer a car from the 1960s (pure mechanics). I don't like the hybrids --- today's complicated, hackable, beeping nannymobiles.

2. Give more time for refactoring. It's an embarrassingly unflashy point, but I think refactoring is important. Don't rush software out. Let programmers refine it. Maybe even force them to, beyond their natural tendencies, like the schoolteacher telling a pupil to revise once again.

It is unflashy, but it makes a big difference. I've revised programs down to a tenth their size (no, not by using one-letter variables and that sort of thing, but by finding more efficient ideas), made them run a hundred times faster on the same hardware, all while adding features and improving safety.

(See the advice about "going deep" instead of "high" or "wide" by Hacker News member bane: https://news.ycombinator.com/item?id=8902739)

3. Data-driven programming. I'll just quote some really smart people:

"Show me your flowcharts and conceal your tables, and I shall continue to be mystified. Show me your tables, and I won’t usually need your flowcharts; they’ll be obvious. --- Fred Brooks, The Mythical Man-Month

"If you've chosen the right data structures and organized things well, the algorithms will almost always be self-evident. Data structures, not algorithms, are central to programming." --- Rob Pike (https://www.lysator.liu.se/c/pikestyle.html)

"I will, in fact, claim that the difference between a bad programmer and a good one is whether he considers his code or his data structures more important. Bad programmers worry about the code. Good programmers worry about data structures and their relationships." --- Linus Torvalds (https://lwn.net/Articles/193245/)

"Even the simplest procedural logic is hard for humans to verify, but quite complex data structures are fairly easy to model and reason about. To see this, compare the expressiveness and explanatory power of a diagram of (say) a fifty-node pointer tree with a flowchart of a fifty-line program. Or, compare an array initializer expressing a conversion table with an equivalent switch statement. The difference in transparency and clarity is dramatic. . . .

"Data is more tractable than program logic. It follows that where you see a choice between complexity in data structures and complexity in code, choose the former. More: in evolving a design, you should actively seek ways to shift complexity from code to data. --- Eric Raymond, The Art of Unix Programming (http://www.faqs.org/docs/artu/ch01s06.html#id2878263). See also ch. 9 (http://www.faqs.org/docs/artu/generationchapter.html)