چویوئه سان (Chuyue Sun)، پژوهشگر دانشگاه استنفورد، به همراه همکاران دانشمند خود ابزاری بر پایه هوش مصنوعی توسعه داد که توانست یک پروژه پیچیده مهندسی را در کمتر از نصف روز و با هزینه‌ای کمتر از ۵۰۰ دلار تکمیل کند؛ در حالی که انجام دستی همان کار توسط سه مهندس برجسته و مجرب نیازمند پنج ماه کار تمام‌وقت بود. این صرفه‌جویی خارق‌العاده در زمان و هزینه که در مقاله‌ای پژوهشی منتشر شده، توجه جامعه جهانی فناوری را به حوزه‌ای کهن و در عین حال دشوار از علوم کامپیوتر و ریاضیات به نام «اعتبارسنجی صوری» (Formal Verification) معطوف کرده است.
برای دهه‌ها، مهندسان نرم‌افزار این رؤیا را در سر می‌پروراندند که با استفاده از قضایای ریاضی اثبات کنند یک برنامه کامپیوتری کاملاً بدون باگ است. این فرایند تاریخی همیشه فوق‌العاده طولانی، گران و ملال‌آور بود؛ زیرا مهندسان باید گزاره‌های بی‌نهایت دقیقی از اهداف نرم‌افزار می‌نوشتند و خطوط کد را به معادلات ریاضی قابل‌اثبات ترجمه می‌کردند. در عمل، اکثر شرکت‌ها تنها به اجرای تست‌های واحد و یکپارچه‌سازی متداول بسنده می‌کردند و اعتبارسنجی صوری فقط به پروژه‌های مرگ و زندگی در سازمان‌های فضایی مانند ناسا یا سامانه‌های مالی حساس منحصر می‌ماند.
اما اکنون در عصر گسترش فراگیر هوش مصنوعی زاینده و پدیده‌ای که به «برنامه‌نویسی حسی» (Vibe Coding) مشهور شده — جایی که کاربران و مهندسان کدهایی حجیم را بدون مطالعه دقیق خط به خط توسط چت‌بات‌ها تولید می‌کنند — نیاز به یک شبکه ایمنی ریاضی به اوج رسیده است. موجی از استارتاپ‌های جدید معتقدند هوش مصنوعی می‌تواند اعتبارسنجی صوری را کاربردی و فراگیر کند.
یکی از این پیشگامان استارتاپ Truth& است که سان اخیراً به آن پیوسته و روز پنج‌شنبه رسماً از فعالیت خود پرده برداشت. سان در تحقیقات خود موفق شد با هوش مصنوعی بخش حساسی از کدهای رمزنگاری پیام‌رسان محبوب Signal را به شکل ریاضی اعتبارسنجی کند. ایلیا سرگی، مدیر ارشد علمی Truth& توضیح می‌دهد: «پل‌ها و آسمان‌خراش‌ها فرو نمی‌ریزند زیرا قبل از ساخت آن‌ها محاسبات دقیق ریاضی انجام می‌شود. چرا نباید برای کدهای نرم‌افزاری حیاتی نیز همین رویکرد را پیاده کنیم؟ فناوری استدلال ریاضی همیشه وجود داشت، اما مقیاس‌پذیری آن به دست انسان ناممکن بود؛ کاری که هوش مصنوعی اکنون میسر کرده است.»
این استارتاپ تاکنون ۷۰ میلیون دلار سرمایه جذب کرده و هدفش پشتیبانی از تمام زبان‌های برنامه‌نویسی است. همزمان، استارتاپ هارمونیک (Harmonic) به رهبری ولاد تنف (مدیرعامل رابین‌هود) با سرمایه‌گذاری ۲۹۵ میلیون دلاری، عامل هوش مصنوعی ارسطو (Aristotle) را برای اعتبارسنجی کدهای زبان C و طرح‌های تراشه با Verilog معرفی کرده است و غول‌هایی مانند انویدیا در حال تست آن هستند. هفته گذشته نیز آنتروپیک و تیم Theorem افزونه‌ای برای Claude معرفی کردند که موفق شد باگ‌های پیچیده‌ای را در پروژه‌های متن‌باز کشف کند که تریلیون‌ها تست کلاسیک قادر به ردیابی آن نبودند.