> Those who understand law know that formal verifiers cannot replace a judge, because every facet of law (the writing of it, the interpretation of it, the application of it, and the enforcement of it) has to account for all the vagueries of human existence.

Not the vagueries of human existence, only vagueries of law specified in natural language.

> No formal verifier can account for definitions that need to expand as the scope of human endeavor expands.

No formal verifier is expected to account for definitions, the democracy shapes the law, and the law would first need to be rewritten as definitional axioms in the database of axioms, theorems & proofs. The verifier is just a minimalistic algorithm performing substitution maps on sequences of tokens. This is intentionally minimalistic to minimize the error / attack surface on the verifier itself.

(Currently only error hardening has happened for metamath verifiers, so obviously we would want formal proofs of the absence of 0-days in the verifier)

> No formal verifier can determine mens rea.

It's up to the democratic population while formalizing, to either formally define intent (which presumably goes nowhere), or to pragmatically accept that in the absence of external traces of intent the only thing society can do is define action-reaction patterns, not intention-reaction patterns, but again, that's not the formal verifier, but the database of axioms, definitions (and theorems and proof)

> No formal verifier can determine if something is obscene.

The same, if democracy by referring to a concept of "obscene" chooses to place itself in the position of needing to first define "obscene" in the database of axioms and definitions. But no formal verifier needs to determine this, the verifier just checks a proof in a due process fashion.

> No formal verifier can determine someone's mental competence.

The formal (not natural langue) law could specify how to assess mental competence in a secure non-malleable way (if the democracy decides it needs that). I'm not a dictator, it's not up to me to propose the exact definitions. The formal verifier is not the place to handle these issues, those should reside in the database of axioms and definitions.

> No formal verifier can cover all mitigating factors.

> No formal verifier can apply mercy where mercy is needed.

"but the machine will never man-splain like a human could"

"the machine can only mech-splain a bit at best"

Some of the very weakest arguments against formal verification in law. Like being anti due process.