Skip to content

The Power of Ten, adapted#

SafeLint is an adaptation of Gerard Holzmann's "The Power of Ten - Rules for Developing Safety-Critical Code" (NASA/JPL, 2006). The original ten rules target C for spacecraft flight software; SafeLint translates their intent to Python, JavaScript, TypeScript, Java, Rust, Go, PHP, C, and C++. Some rules map almost directly (bounded function length, assertion density); others have no literal analogue in a garbage-collected or memory-safe language and are adapted, or deliberately left to the compiler. C and C++ are the exception: as (near-)descendants of Holzmann's original target language they get the literal rules - clauses 1, 3, 8, and 9, adapted away for every other language, exist verbatim as the C-family rules SAFE106 / SAFE310 / SAFE311 / SAFE312 / SAFE313 (which apply to both C and C++). C++ additionally layers on its own ownership / cast-safety rules (SAFE315 raw_new_delete, SAFE316 dangerous_casts).

This page maps each of the ten rules to the SafeLint rules that implement it, and records the rationale wherever a clause is adapted away. For the full per-rule configuration, see the rules reference; for what fires on each language, see the per-language pages under Languages.

Coverage map#

# Holzmann rule SafeLint rules Notes
1 Simple control flow; no goto, setjmp, or recursion SAFE102 nesting_depth, SAFE104 complexity, SAFE105 no_recursion, SAFE106 nonlocal_jumps (C / C++) SAFE105 enforces the recursion ban in every language. goto / setjmp exist in C and C++, where SAFE106 flags them literally (enabled at warning severity).
2 Fixed loop bounds SAFE501 unbounded_loops Flags while True / loop {} without a reachable exit.
3 No dynamic memory allocation after initialisation SAFE310 dynamic_allocation (C / C++); (adapted away elsewhere, see below) C and C++ get the literal rule (SAFE310 flags the malloc family, plus C++ new / delete); for the memory-managed languages the clause is adapted away (intent partly served by SAFE501 / SAFE401).
4 Functions no longer than ~60 lines SAFE101 function_length, SAFE103 max_arguments Default cap 60 lines / 7 arguments.
5 At least two assertions per function SAFE601 missing_assertions, SAFE701 / SAFE702 SAFE601 checks in-function assertions; the test rules check external verification.
6 Declare data at the smallest possible scope SAFE301 global_state, SAFE302 global_mutation, SAFE305 wide_scope_declaration, SAFE307 interior_mutable_static Python global; JS/TS globalThis.* writes and var hoisting; Java non-final static fields; Rust interior-mutable statics; Go package-level var declarations; PHP global keyword and $GLOBALS[...] writes.
7 Check every return value; validate parameters SAFE802 return_value_ignored, SAFE803 null_dereference, SAFE205–SAFE208 (Rust), SAFE112 (Rust), SAFE903 (Spring), SAFE907 + SAFE906 (Python / PHP framework presets) Return-value checking is broadly covered; parameter validation is covered precisely where it can be (Spring @Valid, the Django / Flask / FastAPI / Laravel request-validation rules, Rust arithmetic-on-input) rather than via a noisy generic rule.
8 Limit the preprocessor SAFE311 complex_macro (C / C++), SAFE312 conditional_compilation (C / C++), SAFE309 dynamic_code_execution, SAFE801 tainted_sink, SAFE204 (Rust) C and C++ have a real preprocessor, so SAFE311 (complex macros) and SAFE312 (conditional compilation) flag it literally. Elsewhere the analysability threat is dynamic code execution / reflection (SAFE309 / SAFE801). See below for Rust macros.
9 Restrict pointer use SAFE313 restricted_pointers (C / C++), SAFE803 null_dereference, SAFE306 (Rust), SAFE308 (Rust), SAFE602 (Rust) C and C++ get the literal rule: SAFE313 flags multi-level and function-pointer declarators (smart pointers are exempt on C++). Null/Option dereference everywhere; raw-pointer / transmute hazards on Rust.
10 All warnings on; heed every warning SAFE603 blanket_suppression, plus the engine-internal codes SAFE000 / SAFE004 SafeLint runs as the always-on analyser; SAFE603 flags blanket suppressions of other analysers; SAFE004 polices SafeLint's own unused suppressions.

The error-handling rules (SAFE201–SAFE203 and their Rust analogues SAFE206/SAFE207) and the hidden-side-effect rules (SAFE303/SAFE304) are SafeLint extensions in the spirit of the Power of Ten (predictable, reviewable, testable code) rather than direct mappings of a numbered clause.

Fidelity notes from the paper#

The paper's rule texts carry secondary clauses beyond the headlines. Where SafeLint's behaviour differs or the clause needs a modern-language reading, the decision is recorded here:

  • Rule 2's non-terminating exception. The paper exempts loops that are meant to run forever (a process scheduler) and applies the reverse requirement: it must be provable the loop cannot terminate. SAFE501 flags every while true without a break precisely so the intentional cases surface; the justified # nosafe: SAFE501 annotation is SafeLint's analogue of the paper's documented exception. The paper's suggested mitigation for variable-bound loops (an explicit iteration-cap counter plus an assertion) pairs naturally with SAFE601.
  • Rule 5's density and assertion quality. The paper asks for a minimum of two assertions per function on average, requires assertions to be side-effect-free Boolean tests, requires an explicit recovery action when one fails, and disallows assertions a static checker can prove trivially true (assert(true) does not count). SAFE601 implements the density half: min_assertions defaults to 1 (noise control) and min_assertions = 2 matches the paper. Side-effect-freeness, recovery actions, and trivial-assertion detection need effect and constant analysis that does not fit a structural rule; they remain review concerns.
  • Rule 7's explicit-ignore escape hatch. The paper permits casting a deliberately ignored return value to (void). The per-language analogues are recognised by SAFE802's shape: a Rust let _ = f();, a Python _ = f(), and a Go _ = f() / x, _ := f() are assignments (not bare expression statements) and therefore do not fire, exactly the audit-able explicit-discard the paper intends. On C the paper's own (void)fclose(fp) cast is recognised directly by SAFE802 (the cast wraps the call, so it is no longer a bare expression statement). Among the memory-managed languages, Go's blank identifier is the closest analogue.
  • Rule 9's function-pointer ban. Banned in the paper because function pointers defeat static call-graph analysis (including the recursion proof of rule 1). First-class functions are foundational in the seven memory-managed languages, so this clause is adapted away there (on C, SAFE313 flags function-pointer declarators literally); the analyzability cost shows up in SafeLint as the documented SAFE105 blind spot for anonymous-function recursion.
  • Rule 10's zero-warning policy. The paper requires rewriting code that confuses an analyser even when the warning looks invalid, rather than suppressing it. SAFE603 enforces the suppression half (blanket silencing of analysers); SafeLint's own source follows the rewrite half (its tree-walkers were converted to iterative form rather than annotated when SAFE105 landed). PHP's @ error-suppression operator is the most literal "suppress the analyser" construct in any supported language: prefixing any expression with @ (@file_get_contents(...)) silences both the runtime warning and the analyser at once, so SAFE603 flags every @ use on PHP (alongside bare phpcs:ignore / @phpstan-ignore-line / @psalm-suppress all).

Adapted-away clauses#

Rule 3: no dynamic allocation after initialisation#

The original rule forbids malloc/free after start-up so that memory behaviour is statically bounded and there is no allocator non-determinism or use-after-free. SafeLint implements it literally for C and C++ and adapts it away elsewhere:

  • C and C++ get the literal rule: SAFE310 flags every malloc / calloc / realloc / aligned_alloc / free / strdup call (and, on C++, new / delete). Disabled by default - embedded and safety-critical projects opt in; pre-allocate fixed pools / arenas at init to satisfy it.
  • Python, JavaScript, TypeScript, Java are garbage-collected. Allocation-site analysis is not a meaningful safety gate in these languages: allocation is pervasive and implicit, and the failure modes the rule targets (fragmentation, allocator latency, leaks-by-forgotten-free) are managed by the runtime. The rule's underlying intent, predictable memory and termination behaviour, is partly served by SAFE501 (bounded loops) and SAFE401 (deterministic resource cleanup).
  • Rust makes allocation explicit but idiomatic; rustc and clippy own the performance lane, and a blanket "no allocation in a loop" rule would be noisy. An allocation-in-loop rule is a possible future addition, deliberately not committed to here.
  • AssemblyScript (.as, parsed via the TypeScript grammar) genuinely has manual memory management and is the one place a rule-3 analysis would be meaningful; it is currently an un-analysed surface and is noted here as a known gap.

Rule 8: limit the preprocessor#

C's #define macros generate code the compiler (and any analyser) cannot see until expansion, which is why the original rule restricts them. SafeLint implements it literally for C and C++ and adapts it to runtime code generation / reflection elsewhere:

  • C and C++ get the literal rule: SAFE311 flags function-like macros using ## / __VA_ARGS__ and unbalanced object-like macros, and SAFE312 flags every #if / #ifdef / #ifndef beyond an include guard (the paper's "2^n testable versions" caution). Both disabled by default.
  • Python, JavaScript, TypeScript, Java are covered structurally by SAFE309 (flag eval / new Function / Class.forName / Method.invoke wherever they appear) and dataflow-wise by SAFE801 (flag user input reaching those sinks). The two are complementary and may both fire on one line.
  • Go has no eval; its rule-8 surface is reflection and plugin loading. SAFE309 flags reflect Call / CallSlice / MethodByName and plugin Open / Lookup structurally, and SAFE801 covers user input reaching the os/exec / database/sql / plugin sinks. Go has no C-style preprocessor or conditional-compilation directive (build constraints are file-level, not in-source #ifdef), so there is no cfg-density concern.
  • PHP has the largest dynamic-execution surface of any supported language: eval, the string form of assert, create_function, the call_user_func / call_user_func_array dispatchers, and variable include / require (loading a path computed at runtime). SAFE309 flags the structural call sites and SAFE801 covers user input from the web superglobals ($_GET / $_POST / ...) reaching the eval / exec / unserialize / raw-SQL sinks and the dynamic include / require. The two are complementary and may both fire on one line.
  • Rust's true preprocessor analogue is its macro system. Macro bodies parse as opaque token trees that SafeLint does not decode (the same documented limitation that makes SAFE801 blind to sqlx::query!), so coverage is limited to SAFE204 (panic-family macros) and the lazy_static! case caught by SAFE307. A general macro-as-codegen rule is not offered.
  • Rust conditional compilation (#[cfg(...)] / #[cfg_attr(...)]) is the direct analogue of the paper's caution against #ifdef: the paper notes that just ten conditional directives can yield up to 2^10 testable versions of the code. SafeLint has no rule for cfg-count today; it is recorded under Deferred below as a candidate.

Deferred and out-of-scope#

These are recorded so they are recognised as deliberate decisions, not oversights:

  • Indirect / mutual recursion (rule 1): SAFE105 covers direct self-recursion only. Detecting a -> b -> a cycles needs a call graph and is out of scope for now.
  • Recursive macro calls (rule 8, C): SAFE311 flags token pasting, __VA_ARGS__, and unbalanced replacements, but does not detect mutually recursive macro definitions - that needs a macro-table analysis. (Direct self-reference is inert in standard C: the preprocessor never re-expands a macro inside its own expansion.)
  • Generic parameter validation (rule 7, second half): a blanket "validate every parameter" rule is unacceptably noisy without type information. The intent is served precisely where it can be: Spring @Valid (SAFE903), the non-Java web frameworks' request-validation (SAFE907, enabled by the Django / Flask / FastAPI / Laravel presets) and mass-assignment (SAFE906, enabled by the Django / FastAPI / Laravel presets and pydantic = true, but not Flask) checks, and Rust arithmetic-on-input (SAFE112).
  • Rust allocation-in-loop (rule 3): a real but niche check, recorded above as a possible future rule.
  • Java static final interior mutability (rule 6): a static final field holding a mutable collection is not flagged by SAFE302; detecting interior mutability needs type resolution SafeLint does not do.
  • Typedef- / macro-hidden indirection (rule 9, C): SAFE313 counts pointer levels syntactically in the declarator, so a level hidden behind a typedef (typedef int *intp; intp *pp;) or a macro is not seen; detecting it needs type resolution SafeLint does not do. The paper bans exactly this hiding, so paper-strict projects should also avoid pointer typedefs by convention.
  • Rust #[cfg(...)] density (rule 8): a count-based check on conditional-compilation attributes (the paper's 2^n-versions concern) is a plausible future Rust-only rule; not committed to.
  • Assertion quality checks (rule 5): side-effect-freeness, explicit recovery actions, and trivial-assertion (assert True) rejection need effect / constant analysis; SAFE601 checks density only (min_assertions).