Formal Methods & Verifiable AI
Project MEDHA — Mathematical Engine for Domain-specific Higher-order Autoformalisation
A neuro-symbolic Small Language Model (SLM) for translating natural language into Lean 4 formal specifications, enabling verification-native autonomy for mission-critical domains such as finance, semiconductors, and robotics.
Overview
A neuro-symbolic Small Language Model (SLM) for translating natural language into Lean 4 formal specifications, enabling verification-native autonomy for mission-critical domains such as finance, semiconductors, and robotics.
Details
Project MEDHA proposes the development of a Sovereign Autoformalization Model (SAM), a domain-specific neuro-symbolic SLM optimized for converting natural language mathematics, policies, and specifications into formally verified Lean 4 code.
Unlike probabilistic LLMs, MEDHA is designed around deterministic verification through a generation–verification loop, where a symbolic theorem prover continuously validates and repairs generated formalizations until correctness is achieved.
The initiative aims to establish India’s sovereign infrastructure for verification-native AI systems across mission-critical sectors including quantitative finance, semiconductor design, robotics, and scientific computing.
Current work
- Building a high-speed autoformalization pipeline for Lean 4 theorem proving.
- Developing neural-symbolic generation and verification loops using compiler feedback.
- Extending Mathlib into domain-specific libraries such as FinanceLib and PhysicsLib.
- Formal verification of trading algorithms and regulatory compliance systems.
- Verification-native architectures for robotics and semiconductor correctness.
- Exploring artificial mathematician systems for education and scientific reasoning.
Research themes
- Autoformalisation and theorem proving
- Neuro-symbolic AI systems
- Verifiable superintelligence
- Formal methods for finance
- Lean 4 and dependent type theory
- Deterministic AI infrastructure
- Sovereign AI systems
Vision
MEDHA seeks to move beyond stochastic AI generation toward formally verified intelligence systems capable of operating safely in high-stakes environments. By combining mathematical logic, formal verification, and domain-specific reasoning, the project aims to create foundational infrastructure for trustworthy autonomous systems.