ProVerif
A symbolic cryptographic-protocol verifier developed by Bruno Blanchet (2001–). Takes protocols specified in (a variant of) the applied π-calculus and verifies properties — secrecy, authentication, observational equivalence — under the Dolev-Yao threat model. Internally translates protocol + query into Horn clauses and applies resolution. Used in industrial analyses of TLS, Signal, JFK, and many other protocols. Companion to Tamarin (which uses multi-set rewriting and is more flexible but more interactive).