-
-
It shows the day 46, 166, 82 timeline with the red 16-day gap, the policy's quote next to the law's quote, 5 fails, and "Reviewed: upheld".
-
Scale: 25 policies, 64 hospitals, 90 proved, 8 of 42 confirmed, and the hospital-by-check grid (dashed cells are disputed).
-
Factory does which job, and the accuracy table (Ultra 90%, Super 84%, Nano 72%) with cost per document.
-
An $8,412 bill crossed out and $0 in its place, the apply-by date, Colorado's $233/month cap.
-
Every Nemotron call has its time, tokens and cost, then Z3's verdicts: $0.0451 and 53 s in total.
Inspiration
I'm an interpreter, and I see a lot of hospital bills. I've watched families pay bills their hospital's own policy could have cut, because nobody told them. The CFPB cites at least $2.7 billion billed to patients who were eligible for financial assistance.
Colorado law (Hospital Discounted Care, HB21-1198) promises discounts to every resident at or below 250% of the poverty line, caps payment plans at 4% of monthly income, and bars collection lawsuits for 182 days. Federal 501(r) adds its own windows for nonprofit hospitals. But every hospital writes its own 10–40 page policy, and nobody checks those policies against the law, household by household. I wanted to see if a language model plus a theorem prover could.
What it does
The audit. Waive reads 25 Colorado charity-care policies covering 64 hospitals and checks each one against Colorado law and 501(r). A pass is a proof about the encoded rules. A fail comes with the exact household, or the exact day, where the written policy falls short, next to the policy's own sentence and the law's.
Example: at Children's Hospital Colorado, if the first bill goes out on day 46, the written timeline allows extraordinary collection actions (lawsuits, garnishment) from day 166. Colorado bars them until day 182. That's a 16-day gap, and the same case fails in all five independent Nemotron 3 Super readings.
Across the state, Z3 proved 90 requirements for the encoded rules and found 42 counterexamples. Only 8 are confirmed by at least three of five Super readings; on review, 5 held up and 3 needed caveats. Disputed findings stay on the page, labelled, for a person to check.
The patient side. Upload a bill photo. Nemotron 3.5 Super VL reads it, and Z3 checks the household against the hospital's audited policy: "yes for sure", "yes if …" (naming the missing fact), or "no". It shows the policy's sentence, the apply-by date and a guaranteed discount range, and builds an application packet with a short Spanish summary. The hospital still makes the decision; Waive says what the policy as written promises.
How I built it
| Job | Model on Nebius Token Factory |
|---|---|
| Write each policy as logic, every clause tied to a verbatim quote | Nemotron 3 Ultra (550B) |
| Check each quote supports its clause; five independent second readings | Nemotron 3 Super (120B) |
| Pick the hospital's own document from Tavily search results | Nemotron 3 Nano (30B) |
| Read a bill photo | Nemotron 3.5 Super VL |
| Short Spanish summary in the packet | Nemotron 3.5 Lightning |
| Every legal decision | Z3, no model |
- Find: Tavily search, then Nemotron 3 Nano picks the hospital's official document.
- Formalise: Nemotron 3 Ultra turns the policy into a formal model (rules in CNF over household facts, deadlines with their start dates, payment-plan terms) through a JSON schema.
- Check the translation: plain code verifies every quote is really in the policy; Z3 rejects rules that can never fire and OR-for-AND slips; Nemotron 3 Super checks each quote actually says what its clause claims.
- Second opinions: Super formalises each policy five more times, independently.
- Prove: Z3 runs 10 legal checks per model over a symbolic household (1–12 people, income up to $1M) and a symbolic first-bill day (up to day 400). A counterexample is "confirmed" only if the exact same household or day also fails in at least 3 of the 5 Super models.
Income as a share of the poverty line stays linear for Z3:
$$100 \cdot \text{income} \le k \cdot \big(15{,}960 + 5{,}680 \cdot (\text{size} - 1)\big)$$
Two checks use self-composition: two households that differ only in savings, or only in whether they applied for Medicaid, must be treated the same. MaxSMT picks the most ordinary household that still fails, so counterexamples read like real families.
Evaluation: I wrote reference models by hand for five documents. Audit verdicts agreeing with the references: Nano 72%, Super 84%, Ultra 90%. Where Ultra and Super agree (84% of checks), agreement rises to 95%. Five documents is a small set: these are directions, not precise rates.
The whole build, including every evaluation run and five Super runs per policy, cost about $3 in Token Factory calls. One policy end to end, live, takes about 53 seconds and $0.045.
Stack: Python, FastAPI, Z3, the OpenAI-compatible client against Token Factory, Tavily, pypdf, ReportLab, plain HTML/CSS/JS. Hosted on a small Hetzner server; the code is open source (MIT).
Challenges I ran into
- Real quotes, wrong claims. Most translation errors weren't invented text; they were a real sentence used for the wrong rule (a "reapply every six months" rule read as the application window). That's why the meaning check exists, and why a finding that rests on a missing rule is marked inconclusive when any rule was dropped.
- A model's own lost rule can look like a gap. If a Super reading lost rules in checking, its "fails too" could be its own mistake. Those votes now count as "unable to confirm".
- Letting the model judge didn't work. I tried letting Ultra settle each disputed finding by rereading the policy. It agreed with my references on 0 of 6 decided cases and tended to dismiss findings the text supports. Legal verdicts stay with Z3.
- Reproducibility. Running all audits in one process shifted which counterexample Z3 reported. Each document now runs in a fresh process, and two runs give identical output.
Accomplishments that I'm proud of
- Every finding shows the policy's words and the law's words side by side, and anyone can press "Re-verify with Z3 now" on the live site.
- Waive publishes its doubts: disputed and inconclusive findings are shown, not hidden.
- Nemotron found three clauses my own hand-written Children's reference had missed; I corrected the reference and noted it.
What I learned
Ultra is the best single reader, but the most useful signal is agreement between two models. A second model works best as a confidence check, not as an editor: letting Ultra rewrite its model from the cases where the two disagreed cost four times as much and scored lower. Keep language with the model and logic with the prover.
Limitations
Waive checks written policies, not what hospitals actually do: a counterexample means "the policy as written doesn't guarantee this", not "the hospital breaks the law". Nemotron's translation into logic can be wrong; every finding shows its quotes so a person can check. Only Colorado and federal 501(r). This isn't legal advice.
What's next for Waive
More states, a review by patient advocates and lawyers outside the project, and a version advocates can run on a new policy the day a hospital publishes it.
Log in or sign up for Devpost to join the conversation.