Safety audit pack

Status: prepared 2026-10-29 for an independent audit of Nova's memory-safety and data-race guarantees (the roadmap's P0). This page is the starting point for an auditor: what is claimed, where it is enforced, what the tests show, where holes are most likely, and what the first review found. It is explanatory; the normative rules are in the documents it cites.

1. What is claimed

Safe Nova (no unsafe block or function, no extern call) has no use after free, double free, out-of-bounds access, use of uninitialised memory, or data race, and no undefined behaviour in the generated C (ownership.md §0, §2; c-backend.md §5). Integer overflow, bounds and character-boundary failures panic. unsafe code is outside the guarantee and must keep the contract in unsafe.md.

The invariants, by family (ownership.md §2):

Family	Subject	Where enforced
O*	ownership, moves, drops	Analysis/MoveChecker.cs, MovePaths.cs, DropElaborator.cs
B*	borrowing (shared xor mutable, two-phase, reborrows)	Analysis/BorrowChecker.cs; mutability of places in Semantics/TypeChecker.cs (MutabilityError, Coerce)
E*	escape: no reference outlives its referent	Semantics/TypeChecker.cs (region and signature flows), BorrowChecker.cs
R*	regions, arenas and guards	TypeChecker.cs, BorrowChecker.cs
H*	the heap: Box, Vector, String, allocators	runtime/core/nova_rt_core.c, CEmitter.cs, fault-injection tests
T*	threads: Send/Share, joins, Thread.both	Semantics/Types.cs (IsSend, IsShare, IsForkSafe), TypeChecker.cs (CheckThreadSpawn, CheckThreadBoth), runtime/hosted/nova_rt_thread.c, lib/std
U*	unsafe and FFI	TypeChecker.cs (N0280, N0283), unsafe.md

2. What the tests show, and what they do not

• The corpus (testing.md §3) holds at least two compile-fail tests per rule, and runs every run-pass program in each C configuration, ASan+UBSan included, and since 2026-10-29 every program that starts threads under ThreadSanitizer.
• The M2 mutation suite (MutationTests.cs) turns accepted programs into rejected ones, with verdicts computed independently of the checker.
• The fault-injection sweep (FaultInjectionTests.cs) fails each allocation of each allocating program in turn.
• The NIR interpreter is a dynamic oracle: it faults on an invalid access, an uninitialised read, or a removed check that would have failed (InterpreterTests, CheckEliminationTests).
• The random program generator (testing.md §5) compares the interpreter with every C configuration. Since 2026-10-29 it runs nightly (.github/workflows/fuzz.yml).

None of these proves the checker sound. They catch accepted programs that misbehave when a test happens to write one. The generator writes only programs it believes correct, so it tests the backend and the optimisations, not the checker's rejections. There is no formal model and no borrow tracking at run time (Stacked Borrows style): an aliasing violation that does not corrupt memory in a given run is invisible (R-1).

3. Where holes are most likely

1. Place mutability and reborrows (TypeChecker.cs, MutabilityError, Coerce, ToPlace). Both holes of §4 were here. Mutable access is decided on paths of projections; every projection kind added (fields of references, SliceMut fields, optionals, closures' captures) is a new way in.
2. Field-precise closure captures (M13 G5; TypeChecker.cs, captures). A closure captures a path, not a variable, so conflicts between captures depend on path disjointness, and Thread.both's fork-safety on how each path is used.
3. Send/Share and IsForkSafe (Types.cs). Structural and conservative, but each new type kind needs a rule.
4. Region parameters (M6x; od3-design.md): references stored in structs and collections, and the signature flows that bound them.
5. The generated C's own safety: CEmitter.cs (3,454 lines) and nova_rt_core.c. The checklist in c-backend.md §5 is enforced by construction, not checked.
6. Optimisations that remove checks (CheckElimination.cs, ClosureSpecialisation.cs, PlacementAnalysis.cs). The checker runs before them; each relies on written preconditions (optimisations.md), checked dynamically by the interpreter (R-8).
7. The libraries' @threadSafe types (lib/std's Arc and Mutex, lib/core's atomics, lib/kernel's locks, PerCpu and ObjectCache): unsafe code whose contracts are argued in comments.
8. Moves through raw pointers (ADR 0027): p.read()/p.write(v) of types that are not Copy. The move checker lets a value leave *p (MoveChecker.cs, NirPlace.IsRawDeref), the drop elaborator never drops the old contents of *p (DropElaborator.cs), and a write of C state is a placement (InPlaceChecker.cs, PtrPlace). Each is an exception to an ownership rule that the unsafe code's Safety: argument must make good (unsafe.md U2); lib/kernel's CacheBox<T> is the first user.

4. The first review (2026-10-29)

Three reviewers were given the code and the specification, not a conclusion, and asked to write programs that the checker accepts and that misbehave. Their programs are kept outside the repository (out/audit-closures, out/audit-threads, out/audit-opt). The reviewers were instances of the same model that wrote the compiler, so this is not an independent audit; it is a first pass that an outside reviewer should not rely on.

Area	Result
Closures, captures, dyn, owning closures	One hole, fixed. A borrow mut or SliceMut field read through a shared reference was reborrowed mutably (introduced 2026-10-28): two live mutable views of one vector, a heap use after free under ASan.
Threads and Thread.both	One hole, fixed (same root, older: in 0.1.1). A method needing borrow mut called on such a field through a shared reference was accepted: a use after free on one thread (ASan), and with Thread.both a data race on a Vector (TSan).
Optimisations (closure specialisation, BCE, OCE, ASCII boundaries, placement)	No finding. Two invariants noted as load-bearing: a closure parameter of a specialised variant is never reassigned, and a view is assigned only by let; both are language rules today (N0211, N0246).

Both holes are refused now (N0248; type-system §13.2–§13.3) and covered by check-fail/shared-path-mutation.nova. Suspected and not confirmed: locking a Mutex twice on one thread is undefined in POSIX for a default mutex (nova_rt_thread.c uses pthread_mutex_init(m, NULL)), though Nova's guard types make it a deadlock in practice; user allocators behind Box<dyn I + Send> were not explored.

5. For an outside auditor

Start with ownership.md §2 and type-system.md §13 and §38, then the files in §3 in that order. Each claim in the specification names its diagnostic code; docs/diagnostics.md lists the codes and tests/corpus/check-fail the programs refused for each. novac check --dump-hir shows the checker's view of a program, and novac run --interp runs it in the faulting interpreter (on small programs only). A finding is most useful as a program that novac check accepts, with the sanitizer or interpreter output that shows it misbehaving.