What I keep running into is that teams know the work is informal at the edge, but systems are designed as if formality can be enforced at capture time. In practice, that just pushes the work elsewhere.
In your experience, where does that mismatch hurt the most: audits, safety reviews, customer disputes, or something else?
Computing and formal mathematics rely on exhaustive case analysis and binary logic. And even with The Excluded Middle, there are unprovable statements.
There are at least two incompatible ternary truth tables (hello there SQL NULL) in formal logic. Then there is fuzzy logic, but that is also a formalization.
(NP-complete problems and uncomputable problems in binary logic are another sore point.)
And for informal systems the best people have found so far is hypothesis testing, which is to say that only the rejection of hypothesis based on measurements works, but not confirming a hypothesis.
Turtles and blech all the way down.
What I keep seeing operationally is that teams are forced to act before hypotheses can be tested or falsified. For example, inspections completed, assets redeployed, and customers responded to. Only later are they asked to prove correctness.
When that gap shows up for you, what was the concrete trigger? An audit, a customer dispute, a safety review, or something else?