مایکروسافت ریسرچ یک روند کاری با کمک عامل‌های هوش مصنوعی را نمایش داده که بررسی می‌کند آیا کد تولیدشده برای ورود، الزامات مورد توافق را رعایت می‌کند. تیم سازنده در مطلبی وبلاگی به تاریخ ۵ نوامبر ۲۰۲۶ گزارش داد که از نمونه پژوهشی PDD Kit برای راستی‌آزمایی زیرسامانه ورود Pet Store، یک برنامه وب نوشته‌شده با راست با حدود ۵٬۰۰۰ خط کد، استفاده کرده است. این نمایش به یک زیرسامانه مربوط است، نه راستی‌آزمایی کل برنامه.
این رویکرد که «توسعه مبتنی بر اثبات» نام دارد، تمرکز بازبینی را به تعریف رفتار مورد انتظار منتقل می‌کند. PDD Kit در محیط برنامه‌ریزی Chopin متعلق به GitHub Next از توسعه‌دهندگان می‌خواهد ابهام‌ها را برطرف کنند و تصمیم‌های آنان را در سندی به زبان عادی ثبت می‌کند که به قراردادهای صوری پیوند دارد. یکی از پرسش‌های تعیین‌کننده این بود که الزام گذرواژه درست، صرفاً صدور توکن غیرمجاز را ممنوع می‌کند یا موفقیت احراز هویت را نیز الزامی می‌داند. مشخصات تأییدشده هر دو جهت را پوشش داد، اما اجازه داد شکست جست‌وجوی حساب یا امضای توکن به خطای داخلی منجر شود.
تیم، الزامات را به هشت پس‌شرط برای تابع login_flow تبدیل کرد. عامل‌ها کد پیاده‌سازی و اثبات‌ها را تولید کردند و Verus با استفاده از حل‌گر Z3 آن‌ها را به‌صورت ماشینی بررسی کرد. نویسندگان از اثبات پنج تابع login_flow، login_core، lookup_target، decide_login و issue_token خبر می‌دهند. در چارچوب مدل صوری و فرض‌های آن، قراردادها گذرواژه بررسی‌شده را به همان حسابی متصل می‌کنند که در توکن مشخص شده، نقش‌های مشتری و مدیر را محدود می‌کنند و نتایج خطا را تعیین می‌کنند. اگر هم ایمیل و هم نام کاربری ارسال شوند، ایمیل اولویت دارد؛ توکن مدیر نیز مستلزم طی‌شدن مسیر جست‌وجوی حساب مدیر است.
این روند همچنین درج یک تغییر عمدیِ خطاساز به‌ازای هر پس‌شرط در نسخه‌ای موقت از کد، مانند ردکردن همه درخواست‌های ورود، را توصیف می‌کند تا بررسی شود آیا Verus تخلف هدف‌گرفته‌شده را رد می‌کند. این بررسی‌ها می‌سنجند که آیا قرارداد واقعاً رفتار ناخواسته را منع می‌کند. گزارش، آمار تجمیعی رد این تغییرهای خطاساز را ارائه نمی‌دهد. جریان راستی‌آزمایی‌شده به رسیدگی‌کننده واقعی ورود برنامه متصل شد و طبق گزارش، توسعه‌دهنده پس از بازبینی قصد و الزامات، تغییرها را بدون بازبینی جامع و خط‌به‌خط کد تولیدشده ادغام کرد.
اثبات به مؤلفه‌هایی وابسته است که خود آن‌ها را راستی‌آزمایی نمی‌کند. جست‌وجوهای پایگاه داده، بررسی گذرواژه با bcrypt، امضای توکن، ساعت، تبدیل خطای پایگاه داده و استخراج داده‌های درخواست، همگی پشت قراردادهای فرض‌شده‌ای قرار دارند که توسعه‌دهنده تأیید کرده است. نویسندگان از آزمون‌هایی با bcrypt واقعی، SQLite و مسیریاب واقعی خبر می‌دهند. این آزمون‌ها برای ورودی‌های بررسی‌شده شواهد فراهم می‌کنند، نه اثباتی برای فرض‌ها. راستی‌آزمایی همچنین به زنجیره ابزار Verus، راست و Z3 و کتابخانه استاندارد Verus متکی است.
قراردادها تضمین نمی‌کنند که ورود پایان یابد، سریع پاسخ دهد، تعداد تلاش‌ها را محدود کند، در برابر حملات زمان‌بندی مقاوم باشد، از توقف ناشی از زمان خارج از محدوده جلوگیری کند یا نقش‌های آن در سایر نقاط پایانی درست تفسیر شوند. اثبات همچنین نمی‌تواند الزاماتی را تضمین کند که در مشخصات نیامده‌اند. این نمایش وبلاگیِ گزارش‌شده توسط سازندگان، داوری علمی یا تکرار مستقل نتایج را احراز نمی‌کند و هیچ مقایسه اندازه‌گیری‌شده‌ای از سرعت توسعه، میزان تلاش برای بازبینی، نرخ نقص یا امنیت ارائه نمی‌دهد. PDD Kit در حال حاضر راست را از طریق Verus راستی‌آزمایی می‌کند؛ مقیاس‌پذیری و سهولت استفاده از آن فراتر از این تک‌مورد همچنان اندازه‌گیری نشده است.
تصویر جلد با هوش مصنوعی تولید شده و تصویرسازی مفهومی است؛ مدرک پژوهش نیست.