Resilient and DO-178C (Airborne Software)

DO-178C governs software in certified civil aircraft. This page lists the Annex A objectives where Resilient features contribute evidence, and the gaps that remain the integrator’s responsibility.

Table of contents

Honest framing

Resilient is not DO-178C compliant and not a qualified tool. No DER has audited the compiler. No PSAC, SDP, SVP, or SQAP for Resilient itself exists.

What follows is the realistic path for an applicant who chooses Resilient: the language reduces evidence burden on specific Annex A objectives, but tool qualification per DO-330 (TQL-1 through TQL-5) is required before Resilient artifacts can be used as primary verification evidence in a certified product. Until that work is done, Resilient acts as an input artifact generator to a qualified process the applicant runs.

Annex A objectives Resilient contributes to

The following list is non-exhaustive — these are the objectives where the mapping is direct.

  • A-5 (Verify software architecture). Function contracts (requires / ensures) express architectural invariants directly in source. When Z3 discharges them, the architectural property is proven for all inputs in the contract’s domain — stronger than test-based architectural verification.

  • A-6 (Verify source code). SMT-LIB2 certificates emitted by --emit-certificate are re-verifiable under stock Z3. This breaks the circular trust problem: an auditor does not need to trust the Resilient binary to accept the proof — they re-run the .smt2 file under their own solver and confirm unsat. Per-cert sha256 in manifest.json plus the cert.sig Ed25519 signature give tamper-evidence from the point of emission onward.

  • A-7 (Verify software requirements). requires / ensures clauses tied to a function provide traceable mappings from low-level requirements to code, with source locations.

  • A-3 / A-4 (Verify high-level / low-level requirements). When contracts mirror requirements, the verifier’s discharge is direct evidence of requirements satisfaction for the discharged subset.

  • Robustness testing scaffolding. Contracts that cannot be discharged at compile time become typed runtime asserts that act as instrumented oracles for robustness testing.

Gaps the integrator still owns

  • Tool qualification (DO-330). Without it, Resilient’s output is not primary evidence. This is multi-year work and has not started.
  • Hardware/software interaction (DO-178C §6.4.3). Resilient’s runtime is not yet integrated with a certified RTOS in a documented way.
  • Configuration management (A-8). Standard SCM applies; Resilient does not change this.
  • Quality assurance (A-9). Standard SQA applies.
  • Liaison process (A-10). Standard, unchanged.

See also