Decision-making algorithms could be very complicated and thus pose difficulty for humans to reason whether they guarantee conditional independence. Computers verification could come to rescue. In this project, we try to develop a logic that can express conditional independence and apply it to verification. We define Non-Commutative Bunched Implications (NCBI), which extends the standard logic of bunched implications with a non-commutative conjunction, $\triangleright$. In the extended abstract, we provide a Kripke resource model of NCBI and show how to assert conditional independence in a Kripke resource monoid on Markov kernels. This current work is a part of the larger plan of developing a program logic that will use NCBI as its underlying assertion logic.