Le projet B-in-Dedukti vise à implémenter la théorie mathématique du langage de spécification formelle B dans l'assistant de preuve Dedukti. Cela permet de traduire des preuves de correctitude formelles réalisées dans l'assistant de preuve Atelier B vers Dedukti, facilitant ainsi l'interopérabilité entre différents outils de preuve formelle.