‏اسپکیولا؛ باگ‌یابی خودکار با TLA+

Specula یه سیستم ایجنتیه که کل مسیر باگ‌یابی صوری رو خودکار می‌کنه: از روی کد و تاریخچهٔ کامیت‌ها مشخصات TLA+ می‌نویسه، با trace validation چک می‌کنه که مدل با رفتار واقعی کد جور دربیاد، بعد مدل رو مدل‌چک می‌کنه تا باگ‌های همزمانی پیدا شن، و آخرش با یه تست یکپارچگی همون باگ رو تو خود کد بازتولید می‌کنه. نویسندهٔ این مرور می‌گه ۲۶ سال بعد از مقالهٔ Daikon، دیدن این حجم از خودکارسازی «دکمه‌ای» واقعاً غافلگیرکننده‌ست.

تو ارزیابی، Specula روی برش‌هایی از ۴۸ سیستم توزیع‌شده و همزمان اجرا شده — از MongoDB و Etcd تا SONiC مایکروسافت، libgomp و ra در RabbitMQ، در مجموع ۷ زبان — و ۲۴۹ باگ پیدا کرده که ۲۰۷تاش جدید بوده. هر سیستم بین ۱.۴ تا ۹.۸ ساعت طول کشیده با میانهٔ ۵۷ دلار هزینهٔ توکن. تو یه مقایسهٔ مستقیم روی ۵ سیستم، Specula ‏۶۲ باگ پیدا کرده، Claude Code خام فقط ۲ تا و نسخهٔ مجهز به ابزارها و MCP رسمی TLA+ فقط ۳ تا.

به گفتهٔ نویسنده، نوآوری اصلی از دو نیروی مخالفه که همدیگه رو تیز می‌کنن: trace validation مشخصات رو به سمت کد می‌کشه و model checking پس می‌زنه. اگه فقط نیروی اول باشه، ایجنت تقلب می‌کنه — گاردها رو شل می‌کنه و آپدیت‌های مخصوص همون لاگ رو هاردکد می‌کنه تا اجرا جور دربیاد. تو Kudu-Raft دقیقاً همین اتفاق افتاده و مسیر accept فالوئر جوری «تعمیر» شده که بلافاصله نقض State Machine Safety لوش داده.

اما نویسنده یه ایراد بنیادی‌تر هم می‌گیره: وقتی خود کد منبع حقیقت باشه، مشخصات از همون‌جایی درمیاد که باگ‌ها توش زندگی می‌کنن. ۸۷٪ اینوریانت‌ها از کد و کامنت‌ها میان و فقط ۲۰٪ از مستندات؛ تازه فقط ۲۱.۱٪ اینوریانت‌ها سطح-پروتکل‌ان و بقیه سطح-کد. یعنی سپر ضدتقلب روی یک‌پنجم اینوریانت‌ها سواره و خود ایجنت تصمیم می‌گیره کدوم یک‌پنجم — چیزی که به نظر نویسنده هیچ‌کس چکش نمی‌کنه.

یه نکتهٔ عملی دیگه اینه که مدل زیرین خیلی فرق می‌کنه: با Opus-4.8 ‏۶۲ باگ، با Sonnet-4.6 فقط ۱۰ تا (۵۹ دلار به‌ازای هر باگ به‌جای ۱۶ دلار) و با Haiku-4.5 هیچی. جالب اینکه Haiku هنوز ۹۵٪ سینتکس TLA+ رو درست می‌نویسه ولی تو کیفیت اینوریانت‌ها فقط ۱۷٪ می‌گیره. نویسنده آخرش می‌گه Specula از سخت‌ترین بخش یعنی ترکیب‌پذیری فاصله گرفته و برای هر ماژول یه مدل جدا می‌سازه، درحالی‌که خطاهای واقعاً ترسناک تو سیستم‌های توزیع‌شده همون‌هایی‌ان که از مرز سرویس‌ها رد می‌شن.

نکات کلیدی:

• Specula از روی کد، مشخصات TLA+ می‌سازه و با ترکیب trace validation و model checking باگ پیدا می‌کنه
• ۲۴۹ باگ روی ۴۸ سیستم متن‌باز و ۷ زبان، که ۲۰۷تاش تازه بوده
• میانهٔ ۵۷ دلار و ۱.۴ تا ۹.۸ ساعت برای هر سیستم
• فقط ۲۱.۱٪ اینوریانت‌ها سطح-پروتکل‌ان؛ بقیه از خود کد استخراج می‌شن
• کیفیت خروجی به‌شدت به مدل وابسته‌ست: Opus ۶۲ باگ، Sonnet ۱۰ تا، Haiku صفر
• ترکیب‌پذیری و خطاهای بین‌سرویسی هنوز پوشش داده نشده