&Truth تجمع 70 مليون دولار في جولة تمويل تأسيسية لبناء آلة تحقق شاملة للبرمجيات

خرجت &Truth، وهي شركة ذات منفعة عامة تطوّر تقنيات لإثبات سلامة البرمجيات رياضيًا، من مرحلة التخفي في 29 أكتوبر 2026، وأعلنت عن جمع 70 مليون دولار في جولة تمويل تأسيسية، إلى جانب خطتها لبناء ما تسميه آلة تحقق شاملة للبرمجيات.

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

أتمتة البراهين بالاستناد إلى Lean

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

كما عرضت الشركة تقنية أطلقت عليها اسم «مصنع المواصفات»، وقالت إنها تتيح للمؤسسات والمطورين تحويل مقاصد البشر ومتطلبات الأعمال إلى مواصفات صورية دقيقة على نطاق واسع، بما يوفر ضمانات يمكن التحقق منها بصورة مستقلة، بدلًا من الاعتماد على الاختبارات أو ادعاءات البائعين.

تبني &Truth عملها على Lean، وهو نظام مفتوح المصدر لإثبات النظريات، وعلى Mathlib، وهي مكتبة تضم أكثر من مليوني سطر من التعريفات والنظريات الرياضية، إلى جانب تقنيات مفتوحة المصدر، منها CSLib. وبحسب الشركة، يتمثل الهدف في إنشاء مفردات صورية موحدة للبرمجيات، تشمل نماذج رياضية للغات البرمجة والأنظمة، وتقنيات للإثبات، ومواصفات دقيقة تتيح التحقق الآلي عبر لغات البرمجة. وقالت &Truth إنها تعمل مع Lean Focused Research Organization، وتعتزم إتاحة مكتباتها الأساسية كمصادر مفتوحة.

قال كلارك باريت، الشريك المؤسس والرئيس التنفيذي المشارك، إن Lean وMathlib وفّرا للذكاء الاصطناعي لغة دقيقة للاستدلال في الرياضيات، وإن البرمجيات تفتقر إلى أساس مماثل. وقال إيليا سيرغي، الشريك المؤسس ورئيس قسم العلوم، إن الثقة بالبرمجيات ينبغي أن تستند إلى براهين يمكن التحقق منها على نحو مستقل، لا إلى أقوال أي شركة.

المؤسسون والمقران الرئيسيان

يشغل باريت منصب أستاذ كوربل لعلوم الحاسوب في Stanford University، وهو المدير المشارك المؤسس لـ Stanford Center for AI Safety، ومدير Stanford Center for Automated Reasoning، وأحد مبتكري CSLib، وقائد مشروع محرك الاستدلال الآلي cvc5. وأسّس سيرغي VERSE Lab في National University of Singapore، وشارك في ابتكار أداتي التحقق مفتوحتي المصدر Veil وVelvet. أما الشريك المؤسس والرئيس التنفيذي المشارك ورئيس مجلس الإدارة التنفيذي كريس هسو، فهو عضو في المجلس الاستشاري الاستراتيجي لـ Lean FRO، ورئيس Infinitude Foundation، وقد شغل سابقًا منصب الرئيس التنفيذي في Kilometre Capital، ومنصب المدير العام في Citadel Investment Group.

كما سمّى الإعلان غريغوري ماليشا، الذي سبق أن قاد قسم الأساليب الصورية في BlueRock Security وكان أحد المهندسين الرئيسيين لإطار التحقق BRiCk؛ وسيباستيان أولريش، المشارك في تصميم Lean 4 والشريك المؤسس لـ Lean Focused Research Organization؛ ولينوس لي، الشريك الإداري السابق في Kilometre Capital؛ ودرو هارمان، المدير التجاري السابق في Fastino Labs والشريك التشغيلي في Insight Partners وShasta Ventures. وقالت &Truth إن عملها يستند إلى عقود من الأبحاث في التحقق الصوري والاستدلال الآلي في Stanford University وNational University of Singapore.

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

ويضم موقع الشركة أيضًا نقاشًا على مائدة مستديرة مع ليوناردو دي مورا، مبتكر Lean ونائب الرئيس والعالم المتميز في AWS، وسيمون سيفيريني، عضو المجلس الاستشاري الاستراتيجي لـ Lean FRO والمهندس المتميز في Google.

مقالات مرافقة تشرح مبررات الشركة

في مقال مكمّل مؤرخ في 29 أكتوبر 2026، فصّل هسو الاتجاهات التي تقول الشركة إنها تجعل التحقق أمرًا ملحًا. واستشهد بتصريحات للرئيس التنفيذي لشركة Google، سوندار بيتشاي، مفادها أن الذكاء الاصطناعي يولّد الآن 75% من الشيفرات الجديدة في Google، ويوافق عليها المهندسون؛ وباختبارات Veracode لعام 2026، التي وجدت أن نماذج الذكاء الاصطناعي أخفقت في ما يقرب من نصف مهام البرمجة التي كان الأمن فيها مهمًا. ويستشهد المقال أيضًا بحملة في سبتمبر 2026 نشر فيها مهاجم مئات من وكلاء الذكاء الاصطناعي لاختراق 395 مؤسسة في 48 دولة، مستغلًا ثغرات في برمجيات إدارة الطباعة واسعة الاستخدام، وبنشر رقم قياسي بلغ 14,959 ثغرة برمجية في سبتمبر 2026، وهو عدد يصفه المقال بأنه يعادل 3.5 أضعاف عدد الثغرات المنشورة قبل عام.

يسرد المقال محطات سابقة في التحقق الصوري: فقد استغرق البرهان الأصلي للنواة المصغّرة seL4 نحو 20 سنة عمل بشرية من جهود الخبراء، لإنتاج نحو 8,700 سطر من الشيفرة؛ وفي عام 2015، وفي إطار برنامج HACMS التابع لـ DARPA، دُمج seL4 في مروحية Boeing Unmanned Little Bird غير المأهولة، ولم يتمكن فريق اختبار اختراق محترف، رغم إتاحة أسابيع له، من اختراق أنظمة التحكم في طيرانها؛ وفي سبتمبر 2026، صاغ نموذج ذكاء اصطناعي طورته Anthropic البرهان الكامل لمبرهنة فيرما الأخيرة صياغة رسمية باستخدام Lean، في 11 يومًا. ويشير المقال أيضًا إلى أن كيم موريسون، وهو مهندس برمجيات أبحاث أول في Lean FRO، استخدم Claude من Anthropic في وقت سابق من عام 2026، مع توجيه بشري محدود، لبناء نسخة من مكتبة ضغط البيانات zlib بلغة Lean، وإثبات أنها تستعيد دائمًا البيانات التي ضغطتها نفسها، دون أي تغيير.

ينقل المقال عن مبتكر Lean ليوناردو دي مورا قوله: «يوفر الاختبار الثقة، أما البرهان فيوفر الضمان».

في مقال آخر نُشر في 29 أكتوبر 2026، يشرح سيرغي آليات التحقق من البرامج، بدءًا من ورقة آلان تورينغ المنشورة عام 1949، «Checking a Large Routine»، التي اقترحت أن يرفق المبرمجون شيفراتهم بادعاءات دقيقة يستطيع أداة تحقق فحصها كلًّا على حدة. ويشرح المقال المواصفات وثوابت الحلقات والبراهين التي يجري التحقق منها باستخدام Lean، ويذكر أن هدف &Truth هو تمكين المطورين من الحصول على أدلة قابلة للتحقق منها بصورة مستقلة، مثل برهان صوري باستخدام Lean، بتكلفة تجعل التحقق جزءًا اعتياديًا من عملية التطوير.

تصف &Truth رؤيتها طويلة الأمد بأنها انتقال من «البرمجة بالمزاج» إلى «البرمجة القائمة على التحقق»، بحيث يجري التحقق رياضيًا من الشيفرات التي يولدها الذكاء الاصطناعي قبل نشرها، وتعمل وكلاء الذكاء الاصطناعي ضمن بيئات يمكن إثبات احتوائها، وتُحدَّث البرمجيات القديمة بأمان، وتُحمى البنية التحتية الحيوية بضمانات رياضية يمكن التحقق منها بصورة مستقلة.