In this paper we pursue two targets. First, showing that counterfactual computation can be rigorously formalised as a quantum computation. Second, presenting a new counterfactual protocol which improve previous protocols. Counterfactual computation makes use of quantum mechanics’ peculiarities to infer the outcome of a quantum computation without running that computation. In this paper, we first cast the definition of counterfactual protocol in the quantum programming language qGCL, thereby showing that counterfactual computation is an example of quantum computation. Next, we formalise in qGCL a probabilistic extension of counterfactual protocol for decision problems (whose result is either 0 or 1). If p$_{G}^{r}$denotes for protocol G the probability of obtaining result r “for free” (i.e. without running the quantum computer), then we show that for any probabilistic protocol p$_{G}^{\rm 0}$+ p$_{G}^{\rm 1}$≤ 1 (as for non-probabilistic protocols). Finally, we present a probabilistic protocol K which satisfies p$_{K}^{\rm 0}$+p$_{K}^{\rm 1}$=1, thus being optimal. Furthermore, the result is attained with a single insertion of the quantum computer, while it has been shown that a non-probabilistic protocol would obtain the result only in the limit (i.e. with an infinite number of insertions).