Dağıtık sistemlerin geliştirilmesinde TLA+ ve P gibi formal metotlar, özellikle büyük ölçekli sistemlerde ve dağıtık protokollerde oldukça değerli araçlar olarak öne çıkmaktadır. Endüstride bu araçlar genellikle tam doğrulama için değil, mühendislerin özellikle karmaşık veya hataya açık olduğunu düşündüğü etkileşimler ve protokoller üzerinde yoğunlaşmak için kullanılır. Formal spesifikasyonlar, son tasarımlardaki hataları bulmaktan, tasarım alanının keşfini hızlandırmaya ve uygulanan protokolün kesin dokümantasyonu olarak hizmet etmeye kadar çeşitli roller üstlenir. Genellikle bu spesifikasyonların doğrulanması veya model kontrolü, güvenlik (safety) ve canlılık (liveness) üzerine odaklanır; çünkü veri bozulması ve kaybı gibi güvenlik ihlalleri, dağıtık sistemlerdeki en ciddi sorunlar arasında kabul edilir.
Ancak güvenlik ve canlılık, daha büyük resmin sadece küçük bir parçasıdır. Tasarımcıların karşılaştığı birçok soru, bu metotlarla yeterince ele alınamaz, çünkü bunlar güvenlik, canlılık ve ilgili özelliklerin kapsamı dışındadır. Müşterilerin bekleyebileceği ortalama ve uç durum gecikmesi ne olacak? Bu hizmeti çalıştırmanın maliyeti ne kadar olacak? Bu maliyetler farklı kullanım modelleri ve yük boyutlarıyla (veri boyutu, verim, işlem oranları vb.) nasıl ölçeklenecek? Bu hizmet için ne tür donanıma ihtiyacımız var ve ne kadar? Tasarım, ağ gecikmesine veya paket kaybına ne kadar duyarlı? Kullanılabilirlik ve dayanıklılık kopya sayısıyla nasıl ölçeklenir? Sistem aşırı yük altında nasıl davranacak gibi sorular formal metotlarla doğrudan yanıtlanamaz.
Bu tür soruları prototipleme, kapalı form modelleme ve simülasyonlarla ele alıyoruz. Prototipleme ve bu prototipleri kıyaslama değerli olsa da, keşif aşamasında çok pahalı ve yavaştır. Kapalı form modelleme faydalıdır ancak sistemler karmaşıklaştığında zorlaşır ve sonuçların geçerliliğini azaltabilecek varsayımlar gerektirebilir. Monte Carlo ve Markov Zinciri Monte Carlo simülasyonları ise en faydalı araçlar arasındadır. İyi simülasyonlar da prototipler gibi yoğun geliştirme çabası gerektirir ve dağıtık sistemlerde sistem özelliklerini simüle etmek için yaygın olarak uygulanabilir araç eksikliği vardır. Yazar, hem formal modelleri hem de bu operasyonel soruları ele alabilecek entegre araçlara olan ihtiyacını dile getirmektedir.
Makale, dağıtık sistem tasarımında formal metotların kritik güvenlik ve canlılık sorunlarını çözerken, performans, maliyet ve ölçeklenebilirlik gibi önemli operasyonel endişeleri göz ardı ettiğini vurguluyor.