Dissent

Find the formalization errors nobody is looking for.

Downstream SMT verification proves properties of the formalization you handed it. It is therefore structurally unable to notice the failure that dominates autoformalization in practice: the model is internally impeccable and encodes the wrong reading of the words. Rigour, aimed at the wrong object.

Dissent points the solver somewhere else. It produces N independent formalizations of the same clause and searches for an input on which they disagree — then minimizes that input until it is a fact pattern a person can check by hand, re-executes it outside the solver, and traces it back to the phrase responsible. Its output is never “this clause is correct”. It is only ever “here is where the readings split”, or “these readings were proved to agree, under these assumptions”.

Not legal advice. It does not give legal advice and it does not certify that any clause has been interpreted correctly. Its only output about a clause is either "independent formalizations of this clause disagree, here is where and here is a fact pattern that separates them" or "independent formalizations of this clause were proved to agree under the assumptions listed in this report". Neither statement is a legal conclusion. All contract text used in development is synthetic.

This is the static build of the Space. Every result below was produced by the real z3 pipeline and is precomputed here, because hosting a live Gradio Space requires a paid Hugging Face account and z3 is not available in the browser. The interactive “paste your own clause” app ships in this repository as app.py — run it locally with python app.py, or switch this Space to the Gradio SDK by setting sdk: gradio and app_file: app.py in the README frontmatter.

The downstream verification passed. The formalization is still wrong. — Both panels are true of the same formalization at the same time. The case is selected by the benchmark, not chosen by hand.

100%seeded ambiguities detected
(n=15)

0%false positives on watertight clauses
(n=13)

100%disputed phrase in the top-3 spans

92%of misformalizations missed by downstream SMT verification

41%missed by self-verification at a matched false-positive rate

1.33variables per counterexample (mean)

Explore the run

All 28 synthetic clauses, 15 of which need a human. Pick one: the disputed phrase is highlighted, and the numbers that split the readings are below it.

Benchmark

Three conditions on the same run. (A) single formalization + self-verification. (B) single formalization + downstream SMT verification. (C) Dissent.

condition	detection rate	false-positive rate	misformalizations missed
(A) self-verification, at a matched false-positive rate	46.7%	0.0%	41%
(A) same, at maximum sensitivity	100.0%	92.3%	—
(B) downstream SMT verification	4.0%	0.0%	92%
(C) Dissent	100.0%	0.0%	0%

detection versus false positives — (A) is shown as a curve because it has a sensitivity knob; a single bar for it would be the chart author's choice rather than a measurement.

what each condition misses — 39 genuine misformalizations, measured across every (clause, single-formalization) choice.

triage efficiency — Left: measured. Right: a projection, because the corpus is deliberately about half seeded-ambiguous so the rates are measurable, not because documents are.

witness minimality — Each counterexample is reduced to the variables that are individually necessary, snapped to round contractual values, and re-executed outside the solver.

Run it yourself

pip install -e .
dissent audit contract.txt --n 5      # your document, as a review queue
python app.py                         # the interactive version, locally
python benchmarks/run.py --n 5        # reproduce every number above

Honest limitations

Synthetic by construction. These rates describe behaviour on this corpus and are not a guarantee on any real agreement.
Condition (A) is a model, not a measurement of any LLM. It is reported as a curve across its entire sensitivity range precisely so the comparison does not hinge on a chosen operating point.
The corpus is ~54% ambiguous by design, to make both rates measurable. That is not a prevalence estimate.
“Proved equivalent” always means “under these axioms”, and the axioms are shown with every clause.
Dissent does not resolve ambiguity. It locates it. Choosing the intended reading is a human decision, and it stays one.