"فرمال کاربردی"
دیروز با یکی از دوستان سیستم کار داشتم صحبت می‌کردم و ۲ تا سوال داشت. یکی اینکه : مثلا الان اگه یک سیستم کانکارنت با چندین دیتابیس و کانکشن های مختلف همزمان روی یک ترد داشته باشیم ( مورد واقعی ) چطور میتونیم وریفایش کنیم؟ از کجا باید شروع کنیم؟ چیزی هست که فرآیند رو سریع کنه یا باید از ابتدا برناممون رو مدل سازی کنیم؟ دوم اینکه : یا راه درستی که میشه استفاده کرد اینه که از همون ابتدا verified توسعه بدیم برناممون رو؟

جوابی که من بهش دادم رو برای شما هم قرار میدم:

ببین جواب هر دو سوالت رو با هم میدم. اول از همه تو میتونی برنامه رو طوری توسعه بدی که از همون اول verified باشه، منتهی با هر زبان برنامه‌نویسی نمیشه این کار رو کرد. برای همین ممکنه خیلی جاها دستمون بسته باشه مثلا شرکت میگه که تو باید با زبان Go این سرویس‌ها رو بنویسی و خب ما هیچ فریمورکی نداریم که بتونیم به واسطه‌اش کد Go رو طوری تولید کنیم که verified شده باشه. منتهی خب اگر دست آدم باز باشه و بخواد یه سیستمی رو پیاده کنه بهتره که verified شده انجامش بده مثل همین پروژه‌هایی که بچه‌های MIT انجام میدن. چندتا مثال برات می‌نویسم:

DeepSpec / Sel4 / CompCert / Ironclad / IronFleet / CertiKOS / Formula-V / SCION / Barrelfish OS / ...

با چه زبان‌هایی این کارا رو میکنن:
Dafny - Boogie - Why3 - Coq - Isabelle/HOL - F* - Verus - Idris - Agda - Raven - SPARK - ...

اما خب همه‌ی سیستم‌ها که با این زبان‌ها نوشته نشدن و ممکنه ما یه سیستم مثل اونی که تو گفتی داشته باشیم و بخوایم وریفایش کنیم. چند تا کار میشه کرد. یکیش اینه که اون کد رو مثلا transpile کنی به یکی از زبان‌ها بالا. یکی دیگه‌اش اینه که سعی کنی رفتار برنامه‌ات رو مدل کنی. این کار رو باید با استفاده از زبان‌های فرمال انجام بدی و میتونی از هر یک از ابزارهای زیر استفاده کنی
TLA+ / Ivy / P / CIVL / JKind / SPIN
نکته اینه که اگر مدل سازی کنی، میتونی باگ‌های دیزاین و پروتکلی و الگوریتمی سیستم رو در بیاری. ولی چون خود کد رو verify نمی‌کنی ممکنه که کدت هنوز باگ داشته باشه.

برای وریفای کردن کد اومدن کلی تکنیک و و ابزار توسعه دادن. مثلا JMC که من روش کار میکنم برای وریفای کردن Java است. برخی از این ابزارها مبتنی بر روش‌های کلاسیک verification توسعه یافتن مثل symbolic model checking و Abstract Interpretation و CEGAR.

از بین این روش‌های کلاسیک میشه به اینا اشاره کرد :
CBMC (C) / JBMC (Java) / EBMC (Verilog) / Kani (Rust) / Viper (multi-lang) / CPAChecker (‌C) / Ultimate (C) / JayHorn (Java) / Farma-C (C) / Java Pathfinder (Java) / CN (C) / Nagini (Python) / Prusti (Rust) / BRiCk (C++) / coq-of-rust (Rust) / VerCors (multi-lang) / Verify Rust std lib / Verifast (multi-lang) / DSCheck (OCaml) / Rumur (C) / TriCera (C) / Eldarica (multi-lang) / Stateright (Rust)

منتهی نکته‌ای که وجود داره اینه که اکثر این ابزارها بخاطر محدودیت‌ها و سختی‌هایی که تصمیم پذیری روش‌های کلاسیک دارن، در مواجهه با کیس‌های real-world کم میارن. روش نوینی که برای verification کدها امروزه نشون داده که بسیار promising هستش stateless model checking نام داره که سعی کردم توی این پست توضیحش بدم. در این پست‌ هم لیست smc های موجود برای زبان‌های مختلف رو به همراه توانایی‌ها و محدودیت‌هاشون آوردم.