Rust SIG Meeting - 2026-08-04

[PLeVasseur]

Hey folks 👋 welcome to our 15th meeting of 2026.

Rust SIG Meeting 2026-08-04

Agenda

1. Solicitation of notetaker
   • Pete LeVasseur
2. Rust Watercooler Chat Topic: Unsafe Rust Code: From Encapsulation to Verification; Hui Xu / Fudan University
3. Review GitHub repo content and discuss how to enrich it (Pete)
   1. Issues
   2. Discussions are now active. The SIG previously agreed to take meeting notes there.
4. Office hours: Rust + Automotive questions — come chat (All)
5. Discuss upcoming events / news related to Rust & Automotive (All)
6. Meeting close

Check-in area

We had roughly xx people present at peak attendance, including those listed below.

• xx

Housekeeping

• Document space: https://drive.google.com/drive/folders/1Ub0qTLKvTFilPC9TFVEdTyWn_9qJ-vYD?usp=drive_link
• GitHub repo: https://github.com/rust-sig/rust-sig
• Eclipse SDV Slack channel: #rust-sig

Tasks / action items

• No explicit action items were captured in the source notes.

Rust Watercooler Chat Topic: Unsafe Rust Code: From Encapsulation to Verification; Hui Xu / Fudan University

About Us: Safer-Rust (Unofficial) Working Group on Unsafe Rust

• Mitigate the risk of unsafe code usage in the Rust ecosystem
• Useful these days more than ever in the age of agentic coding

I. Example of Unsafe Code Encapsulation

Using Linked List to explain

Key point: how can we ensure that we can say that something is "safe" when it uses / calls unsafe code?

Can guarantee some properties of push_back(), may not be able to do for others.

• NonNull can be guaranteed
• Dereferenceable?
  *
• Aligned?
  • Created from Box on first function call, so can guarantee that so long as it comes from that previous method call

Can guarantee some properties of pop_front(), may not be able to do for others.

• two unsafe operations
• need to check each one individually
  • Box::from_raw(old_head)
    • Allocated
      • Yes, from Box::new()
    • Owning
      • interesting properties
      • temporarily violating single ownership principle, but set .head = next
      • no risk for double free issue
    • Alias
      • interesting properties
      • value from a boxed owner
      • have to ensure during this context that the Node is not modified through any other raw pointer
      • need to check rest of code to make sure guaranteed
      • after returning value Some(value) need to make sure no other raw pointer still aliasing it
  • latter one has the same properties as above
    • NonNull?
    • Dereferenceable?
    • Aligned?

Unsound encapsulation of front()

• Have two owners -- both that returned by front() and the LinkedList itself
• If T is copy, this is okay, as we can return a copy
• But we don't specify that trait bound here, so this is a bug

Questions

What about borrow checker for raw pointer in your example? I think we talked about ownership rule. For example, the borrow checker may not help with multiple references to the same raw pointer in a given code block. (@bharatGoswami8 will follow up later with a post on this thread)

Verification

Can annotate unsafe APIs with Contracts
Can then assume invariants are upheld when returning from the function
Same concept is used in Rust for Linux, but in plaintext, not machine checked

(Add more details here later)

Example code shown

For example, can annotate to ensure that copy_front() will have a bound allowing for copying the element

prepare-targets

• Scanning source code for verification targets

verify

• Show green if verification passes

Question: does verify cover "all current uses" or "all possible uses" of functions?

• answer: "all possible uses"
• for example, if no bound then we assume no bounds

front()

• Or is unknown therefore it shows up as yellow

Question: So if you constrain the type by copy, RAPx will be fine with it?

• Answer: yes

The safe version has the bound for T: Copy, so then it is verified.

RAPX already reads the core/standard library docs to determine properties useful to the verification

Adoption of the standard / guidelines for unsafe (RAPX)

Two perspectives

• Auditor perspective is currently challenging to "prove"

Safety Promise of Rust

• "We say that a library () ... using its public API."
• Some tension, as some devs feel it should apply to non-public as well

Default Soundness Criterion: Module Level (for pub APIs)

• Developer within the team, working within the module could arbitrarily modify the length to be greater than the current length
• From the perspective of the auditor this is still sound
• From the perspective of the developer this could be seen as unacceptable
  • Unsafe fields as a way to try to model this idea
  • May be still not enough? head and tail could still be accessed and modified directly
  • Could we set head and tail to unsafe field as well? Do we need to mark all fields as being unsafe fields, as many potential invariants exist between them

Design Choices

In the case of showing a case of potentially "incorrect" state, we could think about using unsafe to note that you might get something "wrong"

This is sometimes called "indirect" or "library" undefined behavior in the Rust Project.

How far can you get without a full prover ? I.e., how do you handle cases where the caller must provide its own proof that its maintaining some invariant on behalf of the module ?

• Let's have this put in the thread here to allow for Hui to review and answer

Where are the definitions of "Aliasing" and so on?

• Can visit the RAPX repo to review
• https://github.com/safer-rust/safety-tags
• RFC: RFC: Safety Tags rust-lang/rfcs#3842

Recent events / things coming up for Rust

xx

Requested topics

xx

Material

xx

[mhatzl]

@mhatzl

[senier]

@senier

[mik90]

@mik90

[bharatGoswami8]

@bharatGoswami8

[8rsrf7]

@8rsrf7

[arshadm]

@arshadm

[AntonSchmukel]

@AntonSchmukel

[charcoalfrostmetallic]

@perrymcmanis144

[rajh619]

@rajh619

[hxuhack]

Thank you all. I would be grateful if you could read the Rust Safety Standard and give us feedback.

[bharatGoswami8]

My question is: since raw pointers are not checked by the borrow checker, how is that requirement checked by this invariants (verify) ?, like it checks for ownership rule.

[hxuhack]

We first enumerate all reachable paths and then track the points-to and alias relationships among all pointers for each path, which is similar to what Miri does, but in a symbolic manner. The task is certainly NP-hard, so our approach may produce false positives. Such false positives are unacceptable in a compiler, but verification tools are generally more tolerant of them.

[zearen]

Sorry my question was unclear or if my understanding was unclear. The example of how len was unsafe had me wondering how far this prover can go compared to languages Agda that have a full prover in the type system. I.e., it seemed the issue in the code you provided was that the user had defined len = 10, and so the caller, not the type violated the invariant. Hence the actual question:

Is there a way for a caller to provide proof that it maintains an invariant that the method requires ? The easiest example I can think of is a visitor to some custom sum-like type. There are better ways to accomplish this API, so just consider this for rhetorical purposes:

#[rapx::invariant(any((Null(a), NotNull(b)), (NotNull(a), Null(b)))]
struct Swapper<A, B> {
    pub a: *mut A,
    pub b: *mut B,
}

impl<A, B> Swapper<A, B> {
    fn activate_b_with_fn<S>(&mut self, f: impl FnOnce(*mut A) -> *mut B) -> &B {
        if self.b.is_null() {
            // implicitly requires f always produces non-null.
            self.b = f(self.a);
            self.a = ptr::null_mut();
        }
        unsafe { &*self.b }
    }
}

This is fine if we can prove that f always produces a non-null values. Is there a way callers provide that proof, and that the type can require callers provide that proof ?

In essence, I'm asking a veiled question about the scope of RAPx's model/prover.

[zearen]

(More subtly, we only have the requirement f(nonnull) -> nonnull , but I didn't see a way to express implications in your invariant/requires expressions)

[hxuhack]

This is fine if we can prove that f always produces a non-null values. Is there a way callers provide that proof, and that the type can require callers provide that proof ?

This is a very interesting case. In this example, since the function f is a variable (we assume the function summary is UNKNOWN), our prover cannot establish that the safety precondition for the raw pointer dereference always holds or that the type invariant of the struct is always preserved.

(More subtly, we only have the requirement f(nonnull) -> nonnull , but I didn't see a way to express implications in your invariant/requires expressions)

activate_b_with_fn should be unsafe, right?
If this is the case, the function should have a safety comment saying: The function parameter f should neither accept a null pointer nor return a null pointer.
In this way, we can extend our contract system with expressions like NonNull(f.arg0) and NonNull(f.return).
This is not supported yet, but it should not be difficult to add.

[zearen]

That's really awesome ! Thanks for your talk ! And yes, the ability to add facts like that is exactly what I was curious about.