Unsafe Rust

Unsafe Rust Authoring and Audit

Treat each safety contract as an English-language theorem and each safety comment as its proof. Reject hand-waving, folklore, hidden assumptions, and proof by testing.

Establish the Exact Claim

Unless the user specifies a narrower claim, establish:

For the exact audited source snapshot, every supported compilation configuration, every valid in-scope use in a context satisfying all out-of-scope safety obligations preserves freedom from Rust undefined behavior under the documented Rust abstract semantics, and every mandatory in-scope documented postcondition holds, assuming only the explicitly recorded trusted computing base (TCB).

Interpret valid use as follows:

• For a safe API, quantify over every well-typed safe use. Impose no hidden safety precondition.
• For an unsafe API, quantify over every use satisfying all documented initial, ongoing, and terminal safety obligations.
• For a binary or other entrypoint, quantify over executions satisfying the explicitly recorded deployment assumptions. Do not transfer those assumptions silently to a safe library API.

Prove every documented postcondition of each unsafe API in scope and every documented guarantee consumed by an in-scope soundness proof. Include broader safe-API robustness only when the user or audit scope requests it.

Prove source-level Rust soundness first. State claims about a particular compiler backend, binary, platform, security property, probability, or deployment separately with their additional premises.

Use Only Applicable Premises

• Bottom out Rust-language and standard-library facts in exact applicable text from versioned Rust Reference or standard-library documentation.
• Quote and link the smallest sufficient set of passages whose propositions, together with justified inference steps, entail the fact. Open each citation and verify its wording, qualifications, version, and scope.
• Attach an applicability domain to every claim and premise, whether stated locally or inherited from an identified project policy or canonical entry. A derivation proves only the cases covered by all premises it consumes.
• Define or inherit a precise supported toolchain/configuration predicate before consuming versioned premises or issuing a full verdict. If applicable project sources conflict or materially underdetermine that predicate, obtain an authorized resolution, prove an explicit conservative superset covering every materially supported candidate predicate identified from those sources, or leave the affected full-scope claim UNPROVED. Do not silently select an MSRV, current toolchain, or convenient interpretation, and do not assume that one earliest version represents the whole predicate.
• Apply a guarantee documented for an older Rust release to a later stable release only when an exact applicable Rust backwards-compatibility commitment preserves that exact proposition throughout the later release's relevant domain. An API's stability badge does not by itself preserve every behavioral statement in its current documentation. Record a non-authoritative compatibility premise explicitly in the TCB. Never infer an earlier-version guarantee merely from later documentation.
• Do not promote this skill, the Rustonomicon, Unsafe Code Guidelines, RFCs, blogs, issue discussions, implementation behavior, Miri, or common practice to Rust axioms. Use them to discover risks and authoritative text, or record the exact additional proposition as a TCB assumption.
• Trust a deliberately selected safe dependency API to behave as documented only when that exact trust is explicit in the TCB. Do not extend this exception to caller-controlled safe code, callbacks, values, or safe trait implementations.
• Audit a third-party unsafe API through to admissible premises or record its exact implementation and contract as an additional TCB assumption.

When no admissible direct or derived proof can be completed because authoritative documentation is ambiguous or insufficient, identify the smallest missing proposition. Do not repair it with intuition. Report a documentation gap and suggest an upstream improvement when appropriate.

Compose Proofs Locally and Literally

• Identify the controlling contract independently of the existing safety comment. Distinguish normative contract text from examples, rationale, implementation comments, and inferred design intent.
• Read the controlling contract according to its actual text. Decompose every applicable conjunction, implication, quantifier, temporal clause, precondition, and postcondition into separately reviewable obligations. Do not replace a literal requirement with an operationally similar property. Give every normative clause a disposition even when no known consumer uses it.
• Reify every fact used nonlocally as a named contract or invariant carried by a type, field, function boundary, guard, typestate, lock, token, or other locally checkable mechanism. A function contract about global state is an acceptable degenerate case.
• Prove that each state transition establishes, preserves, transfers, deliberately suspends under an explicit obligation, or discharges every applicable invariant. At each consumer, prove that the current invariant entails the exact needed precondition.
• Trace dataflow across calls and time rather than limiting review to lexical unsafe blocks. Account for every producer, transition, and consumer.
• Do not promote a producer's preconditions into a universal invariant of its output type. Any type- or abstraction-wide conclusion needs a complete derivation independent of that invalid reversal—for example, applicable authoritative premises, construction-and-preservation closure under an enforced boundary, or an admissible explicit TCB premise. Local checks and other applicable derivations may instead prove the proposition for the particular consumed values or quantified subset.
• For new code, place invariant-bearing representation in the smallest practical leaf module, keep safely accessible representation fields private to it, and treat safe code outside that module—including the rest of the same crate—as untrusted.

Follow the Proof Workflow

1. Frame the claim. Record the artifact identity, exact scope, valid uses or executions, Rust and dependency versions, the supported toolchain/configuration predicate and its controlling sources, mandatory postconditions, TCB, exclusions, unresolved support-policy conflicts, and whether design alternatives are requested.
2. Inventory the surface. Enumerate every in-scope safe and unsafe API surface, obligation site, invariant producer/transition/consumer, and generated or expanded artifact across the supported set.
3. State every obligation. Obtain each controlling contract, decompose it literally, and state the exact proposition and applicability to prove.
4. Construct the derivation. Derive every conjunct from checked local facts, named invariants, applicable authoritative axioms, tool-derived theorems, or explicit TCB entries. Unfold definitions and seek indirect multi-premise derivations; absence of one direct sentence is not itself a documentation gap. Justify every intermediate inference.
5. Close composition. Over the entire supported toolchain/configuration predicate—by one parametric proof or an exhaustive partition as appropriate—give every literal clause of each applicable controlling contract and every safe surface a disposition. Ensure every consumed premise has an admissible source. Try to falsify the contract reading, each derivation, and coverage, including boundary and adversarial cases derived from the clauses themselves rather than from any supposedly exhaustive hazard list, before concluding PROVED.
6. Report exactly. Keep unresolved obligations visible and state the smallest missing implication. Record proofs, TCB, coverage, findings, postcondition failures, documentation gaps, and residual scope without optimism.

Do not require a concrete UB counterexample to reject an incomplete proof. A missing, ambiguous, circular, or inapplicable derivation is sufficient for UNPROVED.

Write and Review Proof-Grade Documentation

Read proof-obligations.md before authoring or reviewing an unsafe contract, invariant, SAFETY comment, or local proof.

Keep each proof adjacent to the smallest cohesive unsafe operation or assertion. State the exact operation and its preconditions, cite checked facts and named invariants, show the derivation, and prove resulting postconditions and invariant state on every applicable exit.

When existing code can be validated only by reconstructing a material derivation absent from its safety comment, do not accept it silently. Include the reconstructed derivation—or the smallest missing portion—in the review, with its citations and applicability. Classify implementation correctness separately from proof-documentation quality. If changes are authorized, improve the adjacent proof; otherwise provide proposed wording. Do not use a reconstructed implementation proof to invent or strengthen a caller-facing contract retroactively.

Close API and Configuration Boundaries

Read api-boundaries-and-evolution.md for fields, constructors, methods, traits, sealing, macros, public or hidden APIs, robustness, or contract evolution.

Apply this mandatory safe-surface checklist: public fields, constructors, safe methods, safe trait methods, and macro-generated APIs all count as safe API surfaces. Include language-reachable #[doc(hidden)] safe items for soundness even when excluded from documentation or compatibility promises.

Treat caller-provided safe code as adversarial within the behaviors permitted by safe Rust and its types. Seal a trait or make it unsafe when soundness requires an unenforced implementer behavior.

Read configurations-and-generated-code.md for every full audit and whenever supported-toolchain policy, conditional compilation, targets, generated code, FFI, assembly, SIMD, allocators, linking, or build tooling is relevant. Every supported combination of compilation options that can ship downstream must be sound. Use parametric proofs or exhaustive partitions when literal enumeration would explode; do not substitute a tested sample.

Evaluate Trust and Evidence

Read tcb-and-evidence.md for every full audit and whenever a proof uses dependencies, external specifications, tools, testing, formal verification, environmental restrictions, or cryptographic or probabilistic assumptions.

Judge evidence by the exact proposition it establishes, its artifact and model, its quantified domain and bounds, its premises, and its residual trust—not by a label such as testing, static analysis, model checking, or formal verification.

Design for Provability When Requested

Read abstraction-design.md when the user asks to design, refactor, or reconsider an unsafe abstraction, or when authoring a new unsafe abstraction.

Judge existing code under its current source and controlling contract. Inferred intent or a preferable model may guide a separate proposal but may not narrow, reinterpret, or discharge a current obligation. Treat implemented changes as a new artifact and audit them anew.

Use Exact Verdicts

Read audit-reporting.md before delivering a persistent or full audit.

• PROVED: Every obligation for the exact named claim is discharged over its complete applicability, relative to the stated TCB.
• UNPROVED: At least one required derivation, premise, applicability or coverage argument, postcondition proof, or citation is missing, ambiguous, circular, or unverifiable.
• UNSOUND: A valid use or in-scope execution is proved to reach undefined behavior.
• CONTRACT-BROKEN: It is proved that there exists a valid in-scope execution which, considered as a whole, contains no undefined behavior and falsifies a documented postcondition.

Classify a witness using the execution as a whole, not observations from a prefix of an execution that later reaches undefined behavior. An undefined-behavior-containing execution can witness UNSOUND but cannot establish the existential claim required for CONTRACT-BROKEN. If it is the only behavioral evidence, report soundness as UNSOUND and the postcondition as UNPROVED. An independent UB-free witness or equivalent existence proof may establish CONTRACT-BROKEN; separate proofs may therefore establish both verdicts.

Apply verdicts separately to soundness, documented postconditions, and conditional application claims. State exact scope, applicability, and TCB beside every verdict. Never substitute “looks sound,” “probably sound,” or test success.

For a persistent audit, complete:

• tcb-audit-log-template.md
• unsafe-code-audit-report-template.md

For an inline review, provide the equivalent material compactly. Reuse an existing canonical project log rather than creating a competing trust model.