15
The Power of 10 — Rules for Safety-Critical Code Gerard Holzmann, NASA/JPL, 2006 — ten coding rules that make C statically analyzable. Discipline as gravity.
Gerard Holzmann, at the NASA Jet Propulsion Laboratory Laboratory for Reliable Software, distilled four decades of safety-critical software experience into ten coding rules for C. Restrict control flow to simple constructs (no goto, no recursion, no setjmp/longjmp). Bound every loop with a fixed upper limit a static analyzer can verify. No dynamic memory allocation after initialization. No function longer than a single printed page. At least two assertions per function. Restrict scope of data to the smallest reasonable. Check return values of all non-void functions or explicitly cast to void. Limit preprocessor use. Restrict pointer indirection to one level; no function pointers. Compile with all warnings enabled, treat as errors, run multiple static analyzers. The rules are restrictive enough that any C program following them is amenable to formal analysis, and lax enough that real flight software is written in them. The rules of the road for code that flies.
Holzmann, G. J. (2006). The Power of 10: Rules for Developing Safety-Critical Code. IEEE Computer, 39(6), 95–99. Source → 🇺🇸 Cultural context · United States
NASA after the Columbia disaster of 2003 was rebuilding its software safety culture. The shuttle had been lost on re-entry due to a foam strike during launch — not a software failure, but the post-mortem reopened questions about what software safety meant across the agency. JPL was operating Spirit and Opportunity on Mars, both already past their planned missions. Holzmann, who had also developed the SPIN model checker at Bell Labs, was at JPL's Laboratory for Reliable Software with a mandate to make safety-critical coding teachable. The Power of 10 was the result — a checklist short enough to memorize, restrictive enough to mean something, adopted by the agency and exported far beyond it.
In plain terms
Holzmann had spent decades writing code that flew — Voyager, Cassini, Mars rovers. In 2006 he wrote down what he had learned, and the answer is almost laughably blunt: most of the rules are restrictions on what you are allowed to do.
No goto. No recursion. No dynamic allocation after the program starts. Every loop must have a bound the compiler can prove. Every function must fit on one printed page. Every non-void return value must be checked. All warnings must be enabled and treated as errors. Every function must contain at least two assertions.
These rules look austere. They are. They forbid most of the techniques that make modern software development convenient. No malloc-as-needed. No clever recursive descent. No throw-and-catch. No "we'll just bound this loop dynamically." The rules are designed so that any program written in their style can be statically analyzed end-to-end — meaning a tool can prove, before the program ever runs, that it has no buffer overflows, no use-after-free, no infinite loops, no dereferences of NULL.
This is the discipline Hoare's logic enables, made into a checklist. The Power of 10 is not the deepest formal-methods technique in this book — that distinction belongs to seL4 in chapter eighteen and CompCert in chapter seventeen. But it is the most adoptable . A team that cannot afford full formal verification can adopt the Power of 10 in an afternoon. A code review that follows these rules will catch most of the bugs that take down embedded systems.
These rules are why the Mars rovers do not crash. They are why the SpaceX flight software does not crash. They are why Boeing's avionics work — when they are written under DO-178C, which incorporates these constraints — and why the 737 MAX MCAS system, which was not written under that discipline, did not.
The rest of the industry has the opposite culture. Use any pattern, any library, any abstraction; let the runtime handle it; iterate fast. The opposite culture works fine for software whose worst case is a refunded subscription. It does not work for software whose worst case is a fatal overdose, a crashed plane, or a satellite lost in transit. And as AI tools push the cost of writing "any pattern, any library" toward zero, they push the rest of the industry further from this discipline, not closer.
Ten rules. Mars. Discipline as gravity.