Events

When governments deploy AI in tax administration, regulatory compliance, or citizen-facing legal systems, correctness isn't optional - it's a constitutional expectation. Yet today's LLMs offer fluency without guarantees, making them fundamentally unsuitable as the sole basis for governance infrastructure.

We present work on combining LLMs with Lean 4, the proof assistant, to build verifiably correct representations of legal statutes. Our approach establishes 1:1 correspondence between natural-language law and machine-checkable code, enabling provable correctness of rule application, automatic contradiction detection across large statute bodies, and fully auditable, deterministic outputs. We share early interesting results from formalizing provisions of the Indian Income Tax Act 2025 and argue that "Verified AI" is an essential requirement for legitimate digital governance.