Dafny, kodun doğruluğunu kanıtlamaya odaklanmış, doğrulama bilincine sahip bir programlama dilidir. Yerel olarak spesifikasyonları kaydetme desteği sunar ve statik bir program doğrulayıcı ile donatılmıştır. Sofistike otomatik akıl yürütmeyi tanıdık programlama deyimleri ve araçlarıyla birleştirerek, geliştiricilere spesifikasyonlara göre kanıtlanabilir şekilde doğru kod yazma yeteneği verir. Bu yaklaşım, testler sırasında gözden kaçabilecek maliyetli geç aşama hatalarını azaltarak titiz doğrulamayı geliştirmenin ayrılmaz bir parçası haline getirir.
Dafny, C#, Java, JavaScript, Go ve Python gibi yaygın geliştirme ortamlarına derlenebilir, böylece mevcut iş akışlarına kolayca entegre olabilir. Dilin ekosistemi oldukça kapsamlıdır; doğrulama motorunun yanı sıra çeşitli derleyiciler, popüler yazılım geliştirme IDE'leri için eklentiler, LSP tabanlı bir Dil Sunucusu, bir kod biçimlendirici, referans kılavuzu, eğitimler ve endüstriyel projelerden gelen birikmiş uzmanlığı içerir.
Dafny, matematiksel ve sınırlı tam sayılar, gerçel sayılar, bit-vektörler, sınıflar, iteratörler, diziler, demetler, jenerik tipler, iyileştirme ve kalıtım gibi yaygın programlama kavramlarını destekler. Ayrıca metotlara sahip olabilen ve desen eşleştirme için uygun endüktif veri tipleri, tembel sınırsız veri tipleri, alt küme tipleri (sınırlı tam sayılar için), lambda ifadeleri ve fonksiyonel programlama deyimleri ile değişmez ve değişebilir veri yapıları sunar. Yazılım hakkında matematiksel kanıtlar için de kapsamlı bir araç kutusu sağlar; buna sınırlı ve sınırsız niceleyiciler, hesaplamalı kanıtlar ve lemmaları kullanma/kanıtlama yeteneği, ön ve son koşullar, sonlandırma koşulları, döngü değişmezleri ve okuma/yazma spesifikasyonları dahildir.
Geliştiricilerin yazılımlarının doğruluğunu matematiksel olarak kanıtlamalarına olanak tanıyarak, üretimdeki hataları önemli ölçüde azaltmayı hedefler.