Die Verifikation von Software, also das Beweisen von Eigenschaften auf Basis des Programmcodes hat in den vergangenen Jahren signifikante Fortschritte gemacht. Insbesondere die Automatisierung von Beweisen erlaubt mittlerweile eine Softwareverifikation ohne tiefgreifende Wissen in formalen Methoden. Die ist ein Übersichtsvortrag über das Spektrum von verifizierbaren Programmiersprachen und Theorembeweisern. Es wird versucht, Idris, F*, Coq, Lean, Why3, Liquid Haskell und weitere zu kategorisieren und anhand von Beispielen Stärken und Schwächen der Ansätze aufzuzeigen.