Could it be that formal methods are exactly the solution to "wrangling clarity into requirements from messy humans"? Business people and programmers could work closely together to incrementally build a list of formal requirements with the help of proof assistants. So that both parties can know clearly what are known to be ambiguous and what can be implemented immediately at every stage of discussion. Update the formal list of requirements whenever anyone has a breakthrough. Investigate into possible inconsistency early on with the help of proof assistants. Enforce project-wide constraints for every update to the list of requirements. Cooperate to make more and more informal stuff formal to reduce misunderstanding.

Formal methods can help with exploration and cooperation.