What unsafe Actually Moves
For CULPA, the key fact about Rust is not simply that some operations are marked unsafe. The important question is who must establish the conditions that make those operations sound. This explanation follows the Rust Reference’s distinction between guarantees enforced by the compiler and obligations delegated to programmers, so a reader can inspect an unsafe function, block, trait implementation, or external declaration without confusing permission with proof.
What the compiler can enforce
Rust’s safe subset is built around a set of relationships that the compiler can check. Ownership gives a value one controlling owner at a time. Borrowing permits other code to use that value under rules about shared and mutable access. Lifetimes describe how long those uses may remain valid. Together, these rules prevent many ordinary routes to memory corruption: a reference should not outlive the data it names, two pieces of code should not hold incompatible access at the same time, and a value should not be freed twice through ordinary ownership operations.
Those guarantees are powerful precisely because they are attached to types and program structure. A shared reference is not merely a numerical address. It carries a promise that the referenced value is available for the relevant lifetime and that the aliasing rules for shared access are respected. A mutable reference carries a different promise: the access is exclusive in the way Rust’s rules require. The compiler does not need to inspect every machine instruction to enforce these relationships; it rejects code whose ownership, borrowing, or lifetime structure cannot support them.
Low-level systems work sometimes needs a representation that does not fit those rules. A program may receive an address from an operating-system interface, pass a pointer to hardware, call a foreign library, reinterpret an existing allocation, or build a data structure with links that ordinary references cannot express efficiently. Rust’s raw pointers provide that flexibility. They are not automatically invalid, but they do not carry the same lifetime and aliasing guarantees as references. A raw pointer may be null, dangling, misaligned, outside the intended allocation, or aimed at bytes that do not contain a valid initialized value. The compiler cannot infer all of those facts from the pointer’s type.
The Rust Reference therefore describes unsafe as a way to create or discharge an extra safety condition. An unsafe function is one that is not safe for every possible input or context. Its additional conditions become requirements for callers, and the compiler does not check them. The documentation for such a function is not decorative: it is where the function tells callers what they must make true before using it.
Take an operation that reads an element without performing a normal bounds check. Its signature can express the element type and the index type, but it may not express the relationship that the index must be within the collection’s valid range at the moment of the read. The function can still be useful and fast. The missing relationship is the caller’s proof obligation. A caller might discharge it with a check, a loop invariant, or a data-structure invariant established elsewhere. Without such evidence, the operation is only permitted—not justified.
An unsafe block is the other side of that arrangement. The Reference says that putting operations inside unsafe { ... } states that the programmer has taken care of the relevant safety conditions. The block is a boundary for the compiler’s permission to perform unsafe actions; it is not a runtime verifier. If the programmer enters the block with a false bound, a dangling address, or an invalid value, the block does not repair the mistake. It records an assertion that the surrounding reasoning is supposed to support.
This distinction is easy to miss because the syntax is visible while the proof is often distributed. A reviewer can point to the exact line containing a raw-pointer dereference, but the fact that makes it valid may be a check several lines earlier, a constructor invariant in another function, or a property of all values accepted by a public API. Conversely, code outside the unsafe block may have already invalidated an assumption that the block appears to rely on. The location of the assertion and the location of the evidence need not coincide.
The compiler still performs many ordinary checks inside unsafe code. Names must resolve, types must line up, and the program must satisfy the language rules that have not been waived. What it does not do is turn every extra semantic condition into a statically verified fact. “This code compiles” means that the code is well-formed under the permitted rules. It does not mean that every unsafe precondition has been established for every input and every execution path.
Rust can make the visual boundary narrower without changing the underlying responsibility. By default, the body of an unsafe function is treated as an unsafe block. The unsafe_op_in_unsafe_fn lint can require operations in that body to be placed in explicit unsafe blocks instead. That setting helps a reviewer see the small expressions that need an assertion, but it still does not prove their preconditions. A more visible boundary improves accountability; it does not substitute for the missing semantic evidence.
Nor does the language require every proof to be a handwritten argument at the final line. A caller may establish a condition with a run-time check, a loop invariant, or a trusted data-structure invariant. A library may perform the check once and then expose a safe operation whose contract guarantees the condition for all accepted inputs. The crucial requirement is that the path from the public inputs to the low-level operation preserves the implication. If an interface admits an input that violates the internal assumption, hiding the operation behind a safe function has only hidden the proof obligation from the caller.
That is why unsafe should not be read as either a danger label or a safety certificate. It is a responsibility label. It tells the reader where the ordinary proof system has handed a particular question to someone else.
A useful way to make the handoff concrete is to imagine an operation that receives a raw pointer and a length. The caller may need to establish that the pointer is not null, that the whole requested range belongs to one valid allocation, that the address is aligned for the value being read, and that the bytes have been initialized with a legal value. If another reference can mutate or free the same memory at the wrong time, aliasing and lifetime conditions matter too. The length by itself proves none of these things. A non-null address can still be outside the allocation; an in-range address can still be misaligned; aligned bytes can still be invalid for the destination type.
The evidence may also change while the program runs. A collection can be resized, a pointer can be offset, or a value can be reinterpreted before the final read. A check performed when an allocation was created may no longer cover the range used later. This is why an unsafe call cannot be judged only by looking for any check somewhere nearby. The check must govern the same object, the same portion of that object, and the same state that exists at the operation.
The responsibility is distributed among different participants. The API author must describe the conditions accurately. The caller must establish them for the actual inputs and path. An unsafe trait implementer must preserve the trait’s semantic invariant, even when the trait author cannot inspect the implementation. A library that hides an unsafe operation behind a safe interface must make the internal proof hold for every input that the safe interface accepts. The keyword marks these assignments; it does not decide whether any participant has performed their part.
How the obligation crosses an interface
The responsibility can move in more than one direction. An unsafe function exports a condition to its callers. An unsafe block asserts that the conditions for operations inside it have been discharged. Unsafe traits and their implementations create the same relationship at a type-interface boundary: the trait defines conditions that implementations must uphold, while unsafe impl asserts that a particular implementation meets them.
This matters because a trait can be implemented by code that the trait author did not write. If the trait’s safety depends on an invariant—about ownership, aliasing, layout, or the meaning of returned data—every implementation becomes part of the proof. The compiler can enforce the spelling of an implementation and the types involved, but it cannot generally verify the semantic promise across all future implementations. The unsafe marker makes that promise explicit as a condition of implementing the trait.
External interfaces create a related boundary. The Rust Reference requires an unsafe external block because the programmer declaring it must assure that the signatures of the foreign items are correct. A declaration can look type-checked on the Rust side while still describing the wrong calling convention, argument layout, or return behavior for the library on the other side. The compiler cannot inspect an arbitrary foreign implementation to establish that correspondence. The obligation belongs to whoever writes and maintains the declaration.
Unsafe attributes carry conditions of a different shape. The Reference gives #[unsafe(no_mangle)] as an example of an attribute whose extra safety conditions must be upheld by whoever applies it. The compiler can parse the attribute, but it cannot decide from the spelling alone whether those conditions have been met. Wrapping it in an unsafe form makes the assertion visible instead of allowing a consequential assumption to pass as ordinary annotation.
These forms are not a catalogue of unrelated exceptions. They express one operating rule: when a property cannot be checked from the local Rust expression and its ordinary type information, the language marks the boundary where a human or a higher-level proof must take responsibility. The property may concern a pointer’s validity, a trait’s semantic invariant, a foreign function’s signature, or an attribute’s extra conditions. The object of the proof changes, but the transfer of responsibility is the same.
The boundary can also be wrapped. A library author may use an unsafe block internally and expose a safe function if they can establish the required conditions for every input admitted by that safe interface. That is one of the main reasons unsafe code exists: low-level operations can be concentrated behind a smaller, easier-to-use abstraction. But the wrapper is sound only if its public contract really implies the internal preconditions. A safe-looking function can therefore be the place where an unsafe assumption is hidden, not eliminated.
This is the point at which CULPA’s subject becomes more specific than the language keyword. CULPA does not attempt to treat every occurrence of unsafe as a defect, nor does it claim to encode every obligation created by every unsafe position. Its detector concentrates on memory-safety requirements around raw-pointer dereferences and unsafe APIs. It asks whether the relevant condition holds for the relevant memory region, and whether an unsafe operation can be reached from a public interface without the required protection. In that selected domain, it turns the responsibility label into a question an analysis can try to answer.
The sequence has an important asymmetry. The compiler’s permission arrives when the program is in the right unsafe context, but the conditions are established by the caller’s reasoning before the operation. If the caller’s check covers the wrong object, if an invariant has been invalidated, or if the input can come from an untrusted implementation, the operation can remain syntactically permitted while semantically unsound.
The paper’s examples make this asymmetry concrete. A vector’s length can be increased only when the newly exposed region is both within its allocated capacity and initialized as the element type requires. A conversion can use a correctly aligned address and still produce an invalid value for the destination type. A safe string value can lose its encoding guarantee after a later byte-level transformation. In each case, the unsafe block is only the visible endpoint of a longer argument about data, state, and invariants.
That longer argument is what a contract-oriented analyzer must preserve. It must know not just that an unsafe operation occurred, but which condition it required, which memory or value the condition concerned, where the supporting evidence came from, and whether later code changed the situation. The next step is to name those conditions precisely. Once bounds, nullness, alignment, initialization, and alias discipline are separated, the difference between an unsafe permission and a missing proof becomes much easier to see.