Verus: أداة تحليل ثابتة للتحقق من صحة رمز Rust

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