We propose a framework for "probabilistic functional testing."The success of a test data set generated according to our method guarantees a certain level of confidence into the correctness of the system under test, as a function of two parameters.One is an estimate of the reliability, and the other is an estimate of the risk that the vendor takes when (s)he notifies this reliability percentage to the client.These results are based on the theory of "formula testing~' developed in the article.We also present a first prototype of a tool which assists test case generation according to this theory.Lastly, we illustrate our method on a small formal specification.