گوگل دیپ‌مایند در ۱۰ نوامبر ۲۰۲۶ گزارش داد که چارچوب AlphaProof Code با استفاده از عامل‌های هوش مصنوعی و تخصص انسانی، ویژگی‌های امنیتی مشخصی را در پیاده‌سازی اصلی رمزنگاری سیگنال به‌صورت صوری راستی‌آزمایی کرده است. این اطلاعیه یک مطالعه موردی مهندسی درباره یک پیاده‌سازی را شرح می‌دهد و شاهدی بر عاری‌بودن تمام نرم‌افزار سیگنال از آسیب‌پذیری نیست.
راستی‌آزمایی صوری با استفاده از مشخصات و اثبات‌های ریاضی بررسی می‌کند که آیا یک سامانه، با فرض‌های معین، ویژگی‌های تعریف‌شده را برآورده می‌کند یا نه. پژوهشگران با همکاری مدل‌های زبانی، مشخصات امنیتی سیگنال را تدوین کردند و متخصصان انسانی تک‌تک آن‌ها را بررسی کردند. سپس عامل‌های مبتنی بر Gemini Carbon در Lean، که یک زبان و سامانه بررسی اثبات است، اثبات تولید کردند. دیپ‌مایند می‌گوید Lean اثبات‌ها را بررسی کرد و عامل‌ها نیز موارد نیازمند بازبینی بیشتر توسط انسان را علامت زدند.
ویژگی‌های گزارش‌شده شامل حفاظت از پیام‌ها پیش و پس از نفوذ موقت به یک دستگاه است. دیپ‌مایند می‌گوید این کار از طراحی پروتکل فراتر می‌رود و به پیاده‌سازی کامپایل‌شده می‌رسد؛ یعنی شکافی را هدف می‌گیرد که در آن کد واقعی ممکن است از طراحی موردنظر فاصله بگیرد. ارزیابی این ادعا به مشخصات دقیق، فرض‌ها و زنجیره ارتباط پیاده‌سازی با بازنمایی صوری آن نیاز دارد؛ جزئیاتی که در اطلاعیه ارائه‌شده در دسترس نیست.
شرکت گزارش می‌دهد که راستی‌آزمایی در چهار هفته تکمیل شده است. مقایسه آن با پروژه‌های تاریخی چندساله، فاقد مبنای مقایسه هم‌تراز یا گزارش میزان کار انسانی و منابع محاسباتی است. متن مقاله از بیش از شش میلیون خط Lean تولیدشده خبر می‌دهد، درحالی‌که چکیده همراه آن، سه میلیون خط اثبات را ذکر می‌کند. این اختلاف حل‌نشده است. بنا بر گزارش، عامل‌ها یک درصد از مجموعه کد را برای توجه انسانی علامت زدند، اما مبنای محاسبه این درصد و دامنه بازبینی روشن نیست.
پژوهشگران همچنین دو آسیب‌پذیری واقعی را که پیش‌تر اصلاح شده بودند، دوباره در نسخه‌ای ایزوله از کد سیگنال وارد کردند. دیپ‌مایند می‌گوید سامانه در هر دو مورد، یعنی دو نمونه از دو نمونه انتخاب‌شده، اثبات‌هایی از ناامن‌بودن تولید کرد که ماشین آن‌ها را بررسی کرد. این نتیجه شواهد محدودی از توانایی تشخیص پیاده‌سازی امن از ناامن ارائه می‌دهد. اطلاعیه توضیح نمی‌دهد اشکال‌ها چگونه انتخاب شده‌اند، آیا مدل‌ها قبلاً با آن‌ها مواجه شده بودند یا سامانه در برابر آسیب‌پذیری‌های نادیده چه عملکردی دارد.
تنها اطلاعیه دیپ‌مایند ارائه شده است؛ مقاله فنی و مستندات راستی‌آزمایی که به آن‌ها پیوند داده شده، در داده‌های ارائه‌شده موجود نیستند. بنابراین نسخه دقیق کد، اجزای تحت پوشش، بخش‌های خارج از بررسی و وضعیت داوری علمی مشخص نیست. اظهارات حمایتی سیگنال بازخورد یکی از طرف‌های ذی‌نفع است و تکرار مستقل نتایج محسوب نمی‌شود. اثبات‌های صوری از همان ویژگی‌های مشخص‌شده و در چارچوب فرض‌هایشان پشتیبانی می‌کنند، نه از حفاظت در برابر هر تهدیدی. ادعاهای نخستین دستاورد بودن، عمق بی‌سابقه و کاربردپذیری گسترده را نمی‌توان با اتکا به این مطالب مستقلاً تأیید کرد.
تصویر جلد با هوش مصنوعی تولید شده و تصویرسازی مفهومی است؛ مدرک پژوهش نیست.