Theorem-prover based testing combines testing and verification: tests are derived from a formal specification (or model, i.e., it is a model-based testing technique) proof techniques. HOL-TestGen is a theorem-prover based testing environment on top of Isabelle.
The main result of our work in the area of theorem-prover based testing  is the HOL-TestGen  system. HOL-TestGen is jointly developed by the Software Assurance & Security Research Team at the University of Sheffield, UK and the Verified Algorithms, Languages and Systems team at the LRI (CNRS and University of Paris-Sud), France.
As a unique feature, HOL-TestGen supports the end-to-end life-cycle of formal system testing and verification: from a formal specification that can be formally verified, to formally verified specification transformation (model-transformation), to abstract test case generation, concrete test data generation, to the generation and execution of test scrips that test a real system under test.
HOL-TestGen has been used in large case studies in various application domains, including conformance testing of security properties (e.g., firewall policies  and health-care-specific access control systems ).
1. Brucker, A. D. and Wolff, B. “On Theorem Prover-Based Testing” Formal Aspects of Computing 25, no. 5 (2013): 683–721. doi:10.1007/s00165-012-0222-y, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-theorem-prover-2012
2. Brucker, A. D. and Wolff, B.“: An Interactive Test-Case Generation Framework” Fundamental approaches to software engineering (fase09) (2009): 417–420. doi:10.1007/978-3-642-00593-0_28, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2009
3. Brucker, A. D., Brügger, L., and Wolff, B. “Formal Firewall Conformance Testing: An Application of Test and Proof Techniques” Software Testing, Verification & Reliability (STVR) 25, no. 1 (2015): 34–71. doi:10.1002/stvr.1544, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-formal-fw-testing-2014
4. Brucker, A. D., Brügger, L., Kearney, P., and Wolff, B. “An Approach to Modular and Testable Security Models of Real-World Health-Care Applications” ACM symposium on access control models and technologies (sacmat) (2011): 133–142. doi:10.1145/1998441.1998461, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-model-based-2011
5. Brucker, A. D., Brügger, L., and Wolff, B. “/Fw: An Environment for Specification-Based Firewall Conformance Testing” International colloquium on theoretical aspects of computing (ictac) (2013): 112–121. doi:10.1007/978-3-642-39718-9_7, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-fw-2013