There exist voluntary paths towards formal verifiers as judges: arbitrage.
Parties can agree to some contract and settle any potential future issues in a predetermined specific court of their choice.
Tech companies might prefer the legal certainty formal verification systems provide vis-a-vis human-run courts.
As their use expands, the necessary definitions and normative axioms evolve, until normal companies and then normal people start using it.
The act of formalization from natural language law to metamath database, could probably be done by swarms of agents, resulting in multiple competing formalizations from which competing human subfactions select and promote.