Formal analysis of BCT

Summary
Formal analysis of BCT