Systems

Current

• Profound-Intuitionistic, aka Profint, is an interactive theorem prover for first-order intuitionistic logic that is designed around expressive direct manipulation based interactions. It runs in your browser and produces proofs for a variety of backend verifiers, including Coq, Lean, and Isabelle/HOL.

  • K. Chaudhuri, P. Donato, L. Massacci and B. Werner. Certifying Proof-By-Linking. Technical Report. 2022. HAL
  • K. Chaudhuri. Subformula Linking for Intuitionistic Logic with Application to Type Theory. International Confernce on Automated Deduction (CADE). LNCS 12699, pp. 200–216. 2021. DOI HAL
  • K. Chaudhuri. Subformula Linking as an Interaction Method. Conference on Interactive Theorem Proving (ITP-04), Rennes, France. LNCS 7998, pp. 386–401. July 2013. DOI

• The Abella interactive theorem prover, which is well suited for formalizing the meta-theory of deductive systems. You can run Abella in your browser in addition to a separate tool.

  • D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur, A. Tiu and Y. Wang. Abella A System for Reasoning about Relational Specifications. journal of Formalized Reasoning. Volume 7(2). 2014. DOI

• The Distributed Assertion Management Framework (DAMF) is a proposal for a heterogeneous network of reasoning agents to exchange and reuse assertions while cryptographically tracking provenance and trust. There is a DAMF-aware branch of Abella

  • F. Al Wardani, K. Chaudhuri and D. Miller. About Trust and Proof: An experimental framework for heterogeneous verification. The Practice of Formal Methods: Essays in Honour of Cliff Jones, Part II. LNCS 14871, pp. 162–183. 2024. DOI HAL
  • F. Al Wardani, K. Chaudhuri and D. Miller. Formal Reasoning using Distributed Assertions. International Symposium on Frontiers of Combining Systems (FroCoS). LNCS 14279, pp. 176–194. 2023. DOI HAL
  • F. Al Wardani, K. Chaudhuri and D. Miller. Distributing and trusting proof checking a preliminary report. Technical Report. 2023. HAL

• The Maetning (dis)prover for first-order intuitionistic logic, that is well suited to finding a reason for a non-theorem to be false.

  • T. Brock-Nannestad and K. Chaudhuri. Disproving Using the Inverse Method by Iterated Refinement of Finite Approximations. Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-24), Wrocław, Poland. LNCS 9323, pp. 153–168. September 2015. DOI

Older

• The Sympli family of theorem provers for linear logic which I wrote during my PhD. Written in Standard ML. (BSD 2-clause license.)

• The TLA+ Proof System, a suite of tools for reasoning about Leslie Lamport’s Temporal Logic of Actions. I built the Proof Manager component of this system during 2007-2008. Written in OCaml and Java. ©Microsoft and Inria