I wasn't recoiling at the fact that you use formal methods, actually. I know it's too late for this comment to be seen, but let me actually point out where my "opposites" are by marking up your comments with my version in [brackets]. Admittedly I'm filling in gaps with my own assumptions about what you mean, and you might agree with me more than I think.
> Software engineering can only exist with an incredible amount of discipline. [exploration, creativity, iteration, and discussion are more important than discipline, otherwise you'll be very disciplined in building the wrong thing. This applies at every point of the software lifecycle, not just the beginning!]
> We routinely start new implementations in excel [start as you mean to continue. If you prefer Excel over your programming toolset, you should focus on improving your programming toolset. Excel might help with quick mockups and proofs-of-concept, but should not be the basis of your formal design. Your code should!] and perform formal normalization checks over models before writing any code [you should strive to make your code itself the formal document. Code isn't the output of the design, it's the actual design document itself. Instead of separately "proving" things about your code, write your code as you would write the proof].
> You can get away without having a strong type system [why are you trying to take the "formal" part out of your code and into some other document? Apply your rigor and discipline to the code itself, not some other design document! Strong type systems help you do this.] as long as your tables and relations are clean. [the database is "just" a persistence layer and you're locking yourself into a brittle design if its schema permeates the rest of your codebase. This is probably why you include so much upfront design in your process: you're making way too many early decisions at the database level.] This stuff is so powerful.
> Figuring out how to funnel your domain instances into a SQL db [everyone seems to assume you need to build your application entirely around a relational database. Build your application around what you want to be able to do, and keep your DB as a storage layer!] and writing all your complex logic in terms of basic queries [write your complex logic in code as close as you can to how you would write a requirements document. Simple queries are great but they're the output of a good middle-tier, not a primary representation.] is how you can build an ecosystem in which determinism [huh? "Determinism" is an unexpected word there. You shouldn't struggle with determinism if you use immutability everywhere you can, except maybe in advanced UI use cases] and formal proofs of correctness are possible [again: you should strive to write your code as close to a "formal proof" as you possibly can, instead of treating the proof as a separate step].
> For me, software engineering is about correctness for the business end. There is certainly still a layer of craftsmanship below the engineering realm which enables all the magic. This is where things like performance and reliability live. Interacting with the outside world is an icky thing, and the specific implementation always depends on the use case. [all agreed here]
Look: iterative/Agile methods might appeal to "cowboy coders" who eschew discipline and formal methods, and that gives them a reputation for being associated with "move fast and break things". But they are not inherently less formal than traditional/waterfall "big up front design" methods. The big difference is not a question of "how disciplined should you be?", but rather "where does the discipline go?" Traditional/waterfall methods say "the discipline goes at the start of the project, in big design documents that are separate from the code. Then, later, you code". Iterative/Agile methods say "no, the discipline is maintained throughout the entire project lifecycle and is integrated into how we plan and write the code and manage the ongoing evolution of the project."