Topics / Standards and assurance
DO-333: a formal result needs a visible model and assumptions.
Formal methods can strengthen an assurance argument when the property, model and connection to the implementation are explicit.
Understand the supplement’s role.
DO-333 is RTCA’s formal-methods supplement to DO-178C and DO-278A. It is used with the core document, not as an independent shortcut to assurance.
Source: RTCA: DO-333. Scope and edition reviewed 3 October 2026.
For project credit, the applicable objectives and agreed method matter. A solver returning success is not, by itself, a statement that a software product satisfies those objectives.
Review what the proof assumes away.
Illustrative example
The model’s clock never moves backward.
A model establishes that a control function uses only recent sensor samples, assuming a shared monotonic time source. The implementation instead calculates sample age from a clock that can reset. If its freshness check accepts any age below the limit, a negative age after reset can admit an old sample. The formal result leaves that behavior outside its assumptions.
Decide how the system must treat uncertain sample age. Then represent clock reset and the chosen response in the model, or establish a justified implementation constraint that excludes the condition. Keep a test of the actual clock and timestamp path alongside the formal argument.
| Keep with the result | Review question |
|---|---|
| Property | What makes a sample usable, including unknown or negative age? |
| Model and assumptions | Can clocks reset, disagree or receive older timestamps? |
| Implementation relationship | Which clock supplies each timestamp, and how is age calculated? |
| Tool result and revision | Which property, model and tool run support the conclusion? |
| Remaining scope | Which timing and sensor-integration conditions still need evidence? |
Connect formal evidence to the engineering record.
Proof can retain formalized requirements and evidence alongside implementation and tests. Requirements formalization and verification of critical code are related but distinct activities. Preserve that distinction in reports.
A pilot should select a property small enough to inspect thoroughly and consequential enough to matter. Have the assurance owner review the limits before using the result as acceptance evidence.
Try it on your software
Choose one property worth formalizing.
Bring the requirement, critical implementation and assumptions that constrain the claim.