It's been ~a decade since I was knowledgeable in SpaceX software development details, but at least then, they were not the kind of shop that emphasized rigor and formality. Their culture is oriented toward rapid implementation & test, pragmatism, and empiricism. That has its pluses and minuses.

My personal view is that more of the industry, including SpaceX, should be moving toward engineering things to be more correct-by-construction, including formal modeling & verification as you mention.

As one example, I don't hear most aerospace firms talking about SeL4 for their flight computer RTOSes. For another, you might be surprised (frightened?) by how many vehicles implement their flight software as big single address space executables written in C (sometimes C++) despite running on modern superscalar processors with MMUs. Even static analysis in some of these codebases is relatively recent - they are heavily dependent on functional testing for safety.