Feature Request: Formal verification and DO-178C certification for safety-critical applications

[ntc2]

I'm working on a safety-critical 🩹 avionics system for a new passenger aircraft ✈️, and I'm really excited about using cve-rs in our flight control software 🤖! However, our regulatory requirements are quite strict 👮‍♂️, and I need some additional assurances before we can deploy this in production 🚀.

Requirements

Since we're targeting DO-178C Level A (catastrophic failure conditions), I need the following certifications for cve-rs:

🔬 Formal Verification 🔍

• Full formal verification in Coq or Lean 4 proving that all memory corruptions are indeed memory-safe
• Mathematical proof that segfaults cannot cause segfaults
• Verification that use-after-free operations maintain temporal safety guarantees
• Formal specification of the "safe transmute" semantics in dependent type theory

📋 Certification Standards 🎓

• DO-178C compliance documentation (Level A)
• ISO 26262 ASIL-D certification for automotive backup systems
• IEC 61508 SIL-4 functional safety certification
• Common Criteria EAL7+ security evaluation
• FIPS 140-2 Level 4 validation (just to be safe 🔒)