They're pretty hard to learn. Formal methods are relatively abstract and the feedback loop is a lot less obvious--in TLA+/PlusCal, you aren't writing instructions, you're defining state spaces and relationships between/across them. Since it's not something you generally use often, it also gets rusty quickly. In a lot of dev jobs, it's just not worth the cost.