أنت تراجع المواصفة، والآلة تراجع الكود

أعلنت GitHub Next وMicrosoft Research في 21 أكتوبر عن Proof-Driven Development Kit. الإصدار تجريبي بحثي، ويعمل على Rust فقط، ويطرح حجة كانت معظم الفرق التي تشغّل وكلاء البرمجة تتجنبها: إن لم تكن قادرًا على قراءة الـ diff سطرًا بسطر، فتوقف عن التظاهر بذلك، وراجع شيئًا آخر.

ذلك «الشيء الآخر» هو مواصفة. في سير عمل PDD Kit، يوافق إنسان على المواصفة، وتتحقق آلة من أن التنفيذ يلبيها لكل إدخال ممكن.

خمس خطوات، وأين يجلس الإنسان

تعمل الحلقة هكذا. يخطط الفريق للميزة داخل Chopin، أداة التخطيط الوكيلية متعددة المشاركين من GitHub Next. ثم تناقش PDD Kit الكود، وتستنتج النية، وتقترح مواصفة صورية مكتوبة بـ Verus، وهي لغة إثبات مفتوحة المصدر موجودة أصلًا لـ Rust. يوافق الإنسان على المواصفة، لا على الكود. بعدها يثبت Verus أن الكود الذي ولّده الوكيل يحقق تلك المواصفة لكل إدخال. وحيث لا يكون الإثبات الكامل ممكنًا، تتراجع PDD Kit إلى الاختبارات ووكلاء computer-use للتحقق التجريبي، ويكون الناتج pull request موثّقًا بالإثبات.

الانقلاب هو الفكرة كلها. أنت تراجع المتطلب. والمدقّق يراجع التنفيذ. في Verus، تعلّق المواصفة على الدوال شروطًا مسبقة وشروطًا لاحقة على المدقّق أن يسدّدها، والضمان أقوى من مجموعة اختبارات خضراء بمعنى محدد: الاختبارات تعاين إدخالات، والإثباتات تُكمّم على كل الإدخالات.

صياغة GitHub نفسها أن Chopin مع PDD Kit تتيح للفرق تسليم كود مولّد بالذكاء الاصطناعي إلى الإنتاج دون مراجعته سطرًا بسطر، بضمان أقوى من مراجعة الكود والاختبارات وحدهما. لكن هذا بائع يصف إصداره البحثي، لا نتيجة مدقّقة. لا تمسك بها بقوة.

{{INLINE1}}

الكلفة انتقلت، ولم تختف

هناك إغراء بأن تقرأ هذا على أنه «مشكلة المراجعة حُلّت». ليست كذلك. انتقلت إلى مقدمة خط الأنابيب، وصارت أصعب بطريقة يسهل التقليل من شأنها.

كتابة مواصفة دقيقة بما يكفي لتكون قابلة للإثبات مهارة مختلفة عن مراجعة diff. المتطلبات الغامضة تُنتج مواصفات غير قابلة للإثبات، وسيخبرك المدقّق بذلك عبر الفشل، لذلك تبدو الأسابيع الأولى من التبني كأداة لا تعمل. ما يحدث فعلًا هو أن الغموض في متطلباتك يظهر أبكر من المعتاد، بدفعة من شيء لن يغطيه بدالة تبدو معقولة.

أما الفرق التي تكتب أصلًا مستندات تصميم لا يقرأها أحد، فهذا تغيير حقيقي. يصبح مستند التصميم عنصرًا حاملًا للبنية، لأنه هو الأثر الذي يُفحص.

حيث تتوقف الإثباتات

هناك ثلاثة حدود أهم من قائمة الميزات.

Rust فقط. يفحص Verus كود Rust، وتقول GitHub Next إن PDD Kit تعمل على Rust اليوم، بلا لغة جديدة وبلا تغيير في طريقة إنتاج الكود. إذا كان وكلاؤك يكتبون TypeScript أو Python، فلا شيء لتركيبه بعد. وبالنظر إلى كم الكود الإنتاجي ليس Rust، فهذا قيد كبير يلبس جملة صغيرة.

فقط ما تستطيع المواصفة التعبير عنه. يغطي الإثبات الصوري الخصائص التي يمكنك صياغتها بدقة: عقود الإدخال والإخراج، والثوابت، وانتقالات آلة الحالة. لا يغطي سلوك الواجهة، ولا معظم المنطق المكثّف بالإدخال والإخراج، ولا أي شيء تكون فيه الصحة حكمًا لا خاصية. كل ذلك ينزل إلى مسار الاحتياط من الاختبارات والمراجعة البشرية، وهو بالضبط حيث تعيش الكلفة اليوم.

إصدار بحثي، وله تاريخ محدد. Chopin مدرج في صفحة مشاريع GitHub Next كنموذج أولي بحثي بتاريخ سبتمبر 2026. وقد أطلقت GitHub Next نماذج أولية من قبل — Repo Mind وProject Copernicus وSpecLang بينها — لم تصل قط إلى الإتاحة العامة. أول عرض عام على كود حقيقي مقرر في GitHub Universe، يومي 28 و29 أكتوبر.

الصدق يسكن في مسار الاحتياط

قرار التصميم الأكثر دلالة ليس المدقّق نفسه. بل المسار الثاني الصريح للكود الذي لا يمكن إثباته، والذي يتجه إلى الاختبارات ووكلاء computer-use للتحقق التجريبي.

هذا اعتراف ترفض معظم أدوات التحقق تقديمه. تقول البنية صراحة إن بعض الكود قابل للإثبات وبعضه ليس كذلك، وإن التظاهر بغير ذلك سيكون أسوأ من تسليم خطي أنابيب. الفريق الذي يستخدم هذا ينتهي إلى وسم لكل وحدة — مُثبت، مُختبر، مُراجع — وهو جرد ثقة أصدق من أي شيء ينتجه تقرير تغطية.

المشكلة أن مسار الاحتياط هو أيضًا حيث يصحّح الوكلاء واجبهم بأنفسهم. وكيل computer-use الذي ينقر عبر واجهة ليتحقق من نجاح تغيير يبقى وكيلًا، ويبقى يعاين، ويبقى قادرًا على الاستنتاج بأن مسارًا مكسورًا يبدو جيدًا. المسار المُثبت يعطي إثباتًا. والاحتياط يعطي عرضًا تجريبيًا نجح.

البحث الواقع تحته هو الجزء المطمئن

PDD Kit ليست مدقّقًا بُني من الصفر. Verus مستقل وراسخ. ومستودع verus-proof-synthesis في Microsoft Research يحمل الأساس: نظامان مدفوعان بـ LLM، هما AutoVerus وVeruSAGE، يولّدان ويصلحان إثباتات Verus، وقد قيسا على 150 و849 مهمة تحقق على التوالي.

ما يبدو أن PDD Kit تضيفه هو التغليف. هذه أول مرة تُطوى فيها خطوط بحث تركيب الإثباتات داخل سير عمل منتج من التخطيط إلى الـ PR بدلًا من تمرين قياس أداء. هذا ادعاء أصغر من «الذكاء الاصطناعي يستطيع إثبات كوده»، وأكثر تصديقًا.

لاحظ أيضًا أن المصادر لا تتفق على الاسم. سترى Proof-Driven Development Kit وProperty-Driven Development Kit في تغطية الأسبوع نفسه، وكلاهما منسوب إلى الإعلان ذاته. اختر واحدًا وامضِ؛ فالاختصار هو الذي يصنع العلامة على أي حال.

ما يمكنك فعله اليوم

الخلاصة الباقية ليست «انتظر الإتاحة العامة». بل أن قاعدة كود مليئة بالوكلاء تنقسم الآن إلى أرض قابلة للإثبات وأرض غير قابلة، وإعداداتك يجب أن تعرف بالفعل أيّهما أيّ.

المحللات، وآلات الحالة، وثوابت بنى البيانات، والحساب المحدود الحدود، وأوليات التزامن — هذه أرض قابلة للإثبات، وVerus مفتوح المصدر وصالح للاستخدام الآن، مع PDD Kit أو بدونها. أما معظم عمل الواجهات، ومعظم الكود اللاصق، وكل ما تعتمد صحته على ما قصده المستخدم، فليس كذلك.

يتبع ذلك حركتان عمليتان. أولًا، ضع وسومًا على الوحدات القابلة للإثبات في مستودعك ووجّه وكلاءك إلى Verus لها تحديدًا، قبل أن يسلّم أي بائع سير عمل. ثانيًا، توقف عن مطالبة الوكلاء بكتابة الاختبارات التي تصادق على عملهم هم؛ هذا الترتيب كان دائمًا تضارب مصالح، وهو سبب أن المجموعة الخضراء تعني أقل مما كانت تعنيه.

السؤال المزعج

إذا كانت المواصفة يمكن أن يوافق عليها إنسان والإثبات أن تسدّده آلة، فما وظيفة المراجع بالضبط؟ ليست قراءة الكود، وربما ليست الإمساك بالخطأ الذي أدخله الوكيل في السطر 412.

تصبح وظيفة المراجع هي ما كان يجب أن تكونه طوال الوقت: أن يقرر ما يفترض بالنظام أن يفعله، وأن يرفض مواصفة لا تقول ذلك. هذا أصعب من النقر على موافقة في diff. وهو أيضًا الجزء الوحيد من العمل الذي لا يستطيع مدقّق أن يفعله عنك.