What Rust proves for safe Rust is that even if you were to use these incorrectly, your program is still data-race free and memory safe.

That is, if you use relaxed where you actually wanted to use sequential consistency, your program might do many sorts of incorrect things (e.g. a counter is incremented in the wrong order), but it will not have undefined behavior (it won't dereference a null pointer, doing an access out of bound, double free, or having a data-race).

To write atomic code that creates a data-race, you'd need to use unsafe Rust, and then your program would have UB.

Rust proves this for safe Rust using ownership + borrowing, and `Sync`+`Send`. Ownership and borrowing deal with "aliasing xor mutability" which essentially eliminates all data-races, because a data-race requires a conflicting access involving two aliases where one is a write, and these two features prevent that from happening. `Sync` and `Send` provide proofs that some concurrent accesses are ok, e.g., an atomic relaxed write that conflicts with an atomic relaxed read is ok (what's not ok is unsynchronized conflicting accesses).

As mentioned this does not proves that your program has no logic bugs, only that it has no data-races and UB. It is possible to write programs in safe Rust that do not do what you intend.