Overall, I'm very excited to see this.
I'm concerned about the usability of this feature given its interaction with exclusivity. Programmers will naturally think of atomic objects as mutable — a compare-exchange on an atomic is a mutating operation in the natural sense of the word — and so they will want to declare them as vars. Unfortunately, as discussed in the proposal, this is always wrong but not actually diagnosed. The exact same problem will also arise with non-allocating lock types.
I really think you should add an attribute to this proposal that either disallows declaring a var of a particular type or implicitly reinterprets var as let. (Maybe it should also ban declaring mutating methods on the type.) It would still be possible for users to accidentally get a mutable object of atomic type with generics, but it's reasonable to expect that it will be very uncommon to declare atomics that way, and covering the 99% case should be good enough. You can also give that attribute the (currently non-public) behavior of ensuring that borrowed values of the type are always passed by address, so that non-stdlib programmers have a complete tool they can use to safely wrap their own C-style concurrency primitives.