VerifyThis is a program verification competition, whose 2015 edition took place as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2015) on April 12th, 2015 in London, UK. It is the 4th event in the VerifyThis competition series.

The best team award goes to the team Why3: Jean-Christophe Filliâtre and Guillaume Melquiond.

One of the two distinguished user-assistance tool feature goes to Why3 for the lemma library (as demonstrated by its use in the competition).