پژوهشگران Google DeepMind با استفاده از هوش مصنوعی عاملیت‌محور، شماری از تضمین‌های رمزنگاریِ کلیدیِ پروتکل Signal را به‌طور ریاضی اثبات کردند؛ فرایندی که «راستی‌آزمایی صوری» نام دارد. این دستاورد، تحولی مهم برای این پروتکل رمزنگاریِ پرکاربرد و نیز برای خود هوش مصنوعی به‌شمار می‌رود.

این کار که در قالب نوعی پروژه اثبات مفهوم و طی تنها چهار هفته انجام شد، از دو جهت اهمیت دارد. نخست، تأیید مستقلی دیگر برای رمزنگاری‌ای به‌شمار می‌رود که از حجم عظیمی از ارتباطات مردم در سراسر جهان، در پلتفرم‌هایی مانند اپلیکیشن Signal، Google Messages و WhatsApp محافظت می‌کند. دوم، توانایی‌های Google DeepMind در راستی‌آزمایی صوری را با استفاده از چارچوب هوش مصنوعی جدیدی به نام AlphaProof Code نشان می‌دهد.

به‌طور کلی، راستی‌آزمایی صوری با کمک هوش مصنوعی این روزها مورد توجه فراوان قرار گرفته است؛ اما هنوز مشخص نیست که این روش تا چه اندازه برای استفاده گسترده کاربردی خواهد بود و تا چه حد می‌تواند امنیت حجم زیادی از کد را تأمین کند. طرفداران راستی‌آزمایی صوری مدت‌هاست آن را نوعی جام مقدس در امنیت نرم‌افزار می‌دانند، چرا که با استفاده از ریاضیات بررسی و تأیید می‌کند نرم‌افزار مطابق انتظار عمل می‌کند؛ به بیان دیگر، آسیب‌پذیری‌های حیاتی ندارد.