A living edition of Bhartṛhari's Vākyapadīya: Devanagari mūla, IAST, an original English translation and commentary — and, verse by verse, machine-checked adequacy proofs in Lean 4. A verified badge means the translation's reading provably satisfies a contract whose every axiom quotes the commentary verbatim, and rival misreadings are refuted by compiled theorems.
Honesty boundary: Lean verifies the internal coherence of the formalization — that the accepted reading satisfies the contract and rivals do not. Whether the contract is faithful to Bhartṛhari is a human-auditable question; every axiom carries its verbatim citation for exactly that audit.