Qnarre · axiomatic legal verifier
⌜Every element,
formally checked.⌟
Upload a complaint or filing. Pick a statutory framework. Predicate sub-agents read the natural language; the Lean4 kernel reads only their Booleans. The output is a traceable proof, not a chat. The kernel verifies the inference, never the inputs — the trace shows exactly which predicate or axiom to challenge.
Try the sample complaint →How it works
01
UPLOAD
Paste or upload a complaint, draft motion, answer, or opposition. Bind entities to roles.
02
AGENT STREAM
Predicate sub-agents read the natural language; each returns a Boolean with an evidence quote and a USC citation.
03
REPORT
⊢ §1962(c) from stated predicates · not a finding any claim is true · element checklist · Lean trace.
Frameworks