Current models of the immune system have proven capable of reproducing the dynamics of the immune system response. However, they lack of formalisms (including semantics) to understand general laws of immune system behaviour. This paper introduces a process algebra with which we can model the immune system and make this model subjected to formal verification. We shall discuss how to use the model in order to formalise important properties of immune systems and then outline the sorts of mechanisms that are required to formally verify them.