Abstract: 
The most efficient known primality tests are
probabilistic in the sense that they use
randomness and may, with some probability, mistakenly classify a
composite number as prime – but never a prime number as
composite. Examples of this are the Miller–Rabin test, the
Solovay–Strassen test, and (in most cases) Fermat's
test. This entry defines these three tests and
proves their correctness. It also develops some of the
numbertheoretic foundations, such as Carmichael numbers and the
Jacobi symbol with an efficient executable algorithm to compute
it. 
BibTeX: 
@article{Probabilistic_Prime_TestsAFP,
author = {Daniel Stüwe and Manuel Eberl},
title = {Probabilistic Primality Testing},
journal = {Archive of Formal Proofs},
month = feb,
year = 2019,
note = {\url{https://isaafp.org/entries/Probabilistic_Prime_Tests.html},
Formal proof development},
ISSN = {2150914x},
}
