Ironically, AI is able to produce research-grade algorithms and will probably become an authority on the subject, helping take more traditional CS to the next level.
I have low hopes for this kind of approach; it’s sure to hit the limits of what’s possible with static analysis of C code. Also, choosing Rust as the target makes the problem unnecessarily hard because Rust’s ownership model is so foreign to how real C programs work.
For example, C's buffers obviously have lengths, but in C the length isn't explicitly tied to a pointer, so the translator has to deduce how the C program tracks the length to convert that into a slice. It's non-trivial even if the length is an explicit variable, and even trickier if it's calculated or changes representations (e.g. sometimes used in the form of one-past-the-end pointer).
Other C patterns like `bool should_free_this_pointer` can be translated to Rust's enum of `Owned`/`Borrowed`, but again it requires deducing which allocation is tied to which boolean, and what's the true safe scope of the borrowed variant.
That’s just one example of how C code is nowhere near meeting Rust’s requirements. There are lots of others.
It’s literally in the standard library
https://doc.rust-lang.org/std/collections/struct.LinkedList....
In practice, a little unsafe is usually fine. I only bring it up since the article is about translating to safe rust.
Unsafe blocks are an escape hatch where you promise that some invariants the compiler cannot verify are in fact true. If the translated code were to use that collection, via its safe interfaces, it would still be “safe rust”.
More generally: it’s incorrect to say that the rust ownership model forbids X when it ships with an implementation of X, regardless of if and how it uses “unsafe” - especially if “unsafe” is a feature of the ownership model that helps implement it.
I agree with the sibling -- I think LLMs may be able to help automate some parts of it, but humans are still 95% of it. At least for now.
Imagine refactoring your average C program to use GLib for all (all!) of its data structures. Now imagine doing that, but also translating it into Rust at the same time.
You can also see this effect in the article on the history of Coverity’s analyzer. Real-world code was horrible to deal with vs the academic examples they started with.
https://cacm.acm.org/research/a-few-billion-lines-of-code-la...
You can nitpick the meaning of "forbids", but as far as the current context is concerned, if you translate code that implements a doubly linked list (as opposed to using one from a library) into Rust, it's not going to work without unsafe. Or an index-based graph or something.
The problem with transpiling C to rust is that unsafe and unverified behavior can be a key property of the behavior resulting program, so there isn’t an obvious way to spit out a sort of rustified (CRustified?) binary that matches the behavior of the C program.
Similarly, it they might generate safe wrappers that let teams write new code in Rust side by side with the field-proven C. New code has the full benefits, old code is proven safe, and the interfaces are safer.
A full on translator might be an ideal option. We’d want one language for the codebase in the future. Push-button safety with low, false positives for existing C and C++ is still the greatest need, though. Maybe auto-correcting bad structure right in the C, too, like Google’s compiler tool and ForAllSecure’s Mayhem do.
C programmers don’t do linked lists by using libraries, they hand roll them, and often they are more complex than “just” a linked list. Lots of complex stuff out there.
If that’s the Rust way, then I’m all for it. Will make it easier for Fil-C to have some epic kill shots.
That's what LLMs are for - idiom translation. You can't trust them to do it right, though.
[Pan et al . 2024] find that while GPT-4 generates code that is more idiomatic than C2Rust, only 61% of it is correct (i.e., compiles and produces the expected result), compared to 95% for C2Rust.
This problem needs both AI-type methods to help with the idioms and formal methods to insure that the guessed idioms correctly capture the semantics.
A big advance in this project is that they can usually translate C pointer arithmetic into Rust slices. That's progress on of one of the hardest parts of the problem. C2Rust did not do that. That system just generates unsafe raw pointer arithmetic, yielding ugly Rust code that replicates C pointer semantics using function calls.
DARPA is funding research in this area under the TRACTOR program. Program awards in April 2025, so this is just getting started. It's encouraging to see so much progress already. This looks do-able.
Unlike C++ or Rust, C has no references, only pointers, so developer must release memory manually at some arbitrary point. This is the problem and source of bugs.
It sounds interesting, but I'm not tuned into either community enough to know what parallels you see.
The thing is, rust is used today in more and more places because it's reliable. We're not going to switch out the ground we are standing on every time something shiny comes along and that's why this is such an interesting development.
Formally verified C involves sticking to a strict subset of the capabilities of C that is verifiable, much like Rust enforces, so it makes sense that programs meeting that standard could be translated.
Optimizing C compilers also happened to be good at idiom recognition, and we can probably trust them a little more. The OP paper does mention future plan to use clang as well: >We have plans for a libclang-based frontend that consume actual C syntax.
If such transformation can be done at IR level it might be more efficient to be to C-IR > idiom transform to Rust-IR > run safe-checks in Rust-IR > continue compilation in C-IR or Rust-IR or combining both for better optimization properties.
Note that the converse to this isn't necessarily true! People I trust way more to write unsafe Rust code than me than me have argued that unsafe Rust can be harder than writing C in some ways due to having to uphold certain invariants that don't come up in C. While there are a number of blog posts on the topic that anyone interested can probably find fairly easily by googling "unsafe Rust harder than C", I'll break my usual rule of strongly preferring articles to video content to link a talk from youtube because the speaker is one of those people I mention who I'd trust more than me to write unsafe code and I remember seeing him give this talk at the meetup: https://www.youtube.com/watch?v=QAz-maaH0KM
Zig seems to be awesome at creating mixed environs of zig for new code and C for old, and translating or interop, plus being a C compiler.
There must be some very good reasons why Linux kernel maintainers aren't looking to zig as a C replacement rather than Rust.
I don't know enough to even speculate so would appreciate those with more knowledge and experiencing weighing in.
I'm not sure what it has to do with translating the code to Rust.
Rust isn't a "replacement for C", but an addition to it. It's a tool that Torvalds et. al. has recognised the value of and thus it's been allowed in the kernel. The majority of the kernel code will still be written in C.
I'm no kernel maintainer, but I can speculate that two of the main reasons for Rust over Zig are the compile time guarantees that the language provides being better as well as the rate of adoption. There is a lot of work done by many leading companies in the industry to provide Rust native code or maintained Rust bindings for their APIs. Windows devs are re-writing parts of _their_ kernel in Rust. There's a "movement" going on that has been going on for a while. I only hope it doesn't stop.
Maybe the maintainers feel like Zig doesn't give them enough over C to be worth the change? Many of them are still opposed to Rust as well.
> The coercions introduced by conversion rules can however lead to subtle semantic differences
The example they give is this C code:
1 uint8_t x[1] = { 0 };
2 uint8_t *y = x;
3 *y = 1;
4 assert(*x == 1); /* SUCCESS */
getting translated to this (safe) Rust code: 1 let x: [u8; 1] = [0; 1];
2 let mut y: Box<[u8]> = Box::new(x);
3 y[0] = 1;
4 assert!(x[0] == 1) /* failure */
So the pointer (iterator) targeting an existing (stack-allocated) array declared on line 2 gets translated to an owning pointer/Box) targeting a (heap-allocated) new copy of the array. So if the original code was somehow counting on the fact that the pointer iterator was actually targeting the array it was assigned to, the translated code may (quietly) not behave correctly.For comparison, the scpptool (my project) auto-translation (to a memory safe subset of C++) feature would translate it to something like:
1 mse::lh::TNativeArrayReplacement<uint8_t, 1> x = { 0 };
2 mse::lh::TNativeArrayReplacement<uint8_t, 1>::iterator y = x; // implicit conversion from array to iterator
3 *y = 1;
4 assert(*x == 1); /* SUCCESS */ // dereferencing of array supported for compatibility
or if y is subsequently retargeted at another type of array, then line 2 may end up as something like: 2 mse::TAnyRandomAccessIterator<uint8_t> y = x; // implicit conversion from array to iterator
So the OP project may only be converting C code that is already amenable to being converted to safe Rust. But given the challenge of the problem, I can respect the accomplishment and see some potential utility in it.edit: added translation for line 2 in an alternate hypothetical situation.
Saying this as someone who generally likes Zig's direction.
Formally verified C programs typically have had all their undefined behaviour already stamped out during the verification process. That makes mapping it over to Rust a lot simpler.
The first is that the translation function (from C to Rust) has itself been formally verified. In other words: if you give it a C program that obeys certain necessary pre-conditions, it will give you a safe Rust program. I believe the title of the paper is primarily using "Formalized" with regard to this characteristic.
The second is that the set of programs the authors evaluate their tool on are C programs that have themselves been formally verified. I only barely skimmed the introduction and didn't see it addressed directly there, but I would assume that this is because the pre-conditions necessary for their translation to work are most easily (only?) met by formally verified C programs, where of course the verification has been rendered with respect to properties that would be relevant here (e.g., memory use).
Hmm I think to clarify I would say that Rust _is_ intended as a replacement for C in general, but that this isn't how the Linux kernel developers are choosing to use it.
As for why the kernel developers would choose Rust, I would think another one of the primary benefits is that the type system guarantees the absence of a wide class of memory-related errors that are prevalent in C, and this type system (as well as those of its predecessors) has been subjected to significant scrutiny by the academic community over the last couple of decades to help iron out problems. I suspect this is also part of why Rust has a relatively large and passionate community compared to other C alternatives.
No, some C programs cannot be made safe. This can be due to dependency on undefined or unspecified behaviors, or it can be because introducing proper safety checks would limit the domain of possible inputs too much to be useful, or other things.
Translating to a safe language can maintain the expressive capabilities of the inputs while statically guaranteeing correct operation at run-time. It is objectively better in these cases.
> field-proven C
I don't think this exists, as the numerous critical vulnerabilities over the years have shown. All we have is C that seems to work pretty well often enough to be useful.
> old code is proven safe
Old code is assumed to be safe due to luck, actually. "Prove" has a specific meaning (especially on a post for a paper about proving things), and the overwhelming majority of C code is not proven to any rigorous mathematical standard. In contrast, the Rust type system has been mathematically proven to be correct.
> A full on translator might be an ideal option.
It depends on what you're willing to give up. If you don't mind losing performance, limiting your domain of inputs or range of outputs, giving up code legibility, and so on, then sure, this can probably be done to some extent. But when you start wanting your translator to be both sound and complete over all of these concerns, you run into problems.
Has there actually been a successfull contribution to the mainline kernel? The last two big projects I heard of (ext2 / Apple drivers) seemed to have issues getting their code accepted.
It is hard to get a full picture of how academic research influenced Rust and vice versa. Two examples:
- The use of linearity for tracking ownership in types has been known to academics but had never found its way into a mainstream language.
- researchers in programming language semantics pick Rust as a target of formalization, which was only possible because of design choices around type system. They were able to apply techniques that resulted from decades of trying to get a certified C. They have formalized parts of the standard library, including unsafe Rust, and found and fixed bugs.
So it seems fair to say that academic research on safety for C has contributed much to what makes Rust work today, and in ways that are not possible for C and C++ because these languages do not offer static guarantees where types Transport information about exclusive access to some part of memory.
Also, is much of the authors did manual or was it run through something to produce the Rust code? If so, where is the code that generates Rust, I do not see any links to any source repos.
The paper states that these developments will be released under open source licenses after the review process is completed, i.e. most likely, after the paper is formally published.
These kinds of manual or automated conversation from C to <safer language> therefore have potential not only for increasing adoption of safer languages but also for uncovering existing bugs.
[1] https://www.researchgate.net/profile/James-Cheney-2/publicat...
First of all they never translated any C! At all. Zero lines.
They took code written in F* and modified its C compiler to emit Rust. They never had to deal with any actual C code of any complexity, aside from the most trivial code that might theoretically be emitted by a toy compiler (but wasn't even that!). They just pretended they were dealing with C (or a heavily restricted Mini-C).
Even if we accept this, there are plenty of arbitrary restrictions on the C it can even support in principle:
> If the original C program further relies on x, our translation will error out, and will ask the programmer to fix their source code.
That's saying you want C to already be written in a style that makes the Rust borrow checker happy! They're avoiding the actual hard parts of the problem.
> These rules present simplified versions of what we support. Our implementation features several peephole optimizations ...
If I may translate from the language of academia. "We present beautiful rules in figure 4. But in reality, our implementation relies on a large number of hacks."
But it gets worse!
> For overlap cases that can be distinguished statically (as above), we emit a compile-time error; otherwise, the Rust code will panic at runtime.
The resulting code is not guaranteed to be correct! For example, aliasing in C can cause crashes in the resulting Rust code. See comment at the top of page 10. We're going from a formally verified C program to a "It may crash now" Rust program!? That's nuts!
> We apply our methodology to existing formally verified C codebases, namely, the HACL* cryptographic library ...
This is such a blatant lie that I had to return to it. It's designed to catch an unwary reviewer. We often talk about HACL being in verified C because it gets compiled to that. But it's not a C library, it's written in a totally different language. You cannot confuse the two.
I'm not a reviewer for their paper. But if I was, I would strongly fight for rejection.
The fact that they only handle formally verified C is so astronomically far away from being their main problem.
An honest title would be "Compiling a subset of F* to partially Safe Rust, Partially Formalized"
Seems it would be a win even if the unsafe portion is quite large. Obviously not of it’s 90% of the end result.
In this case it's not about Frama-C or similar tools though, see your sibling comments about the caveats.
Sadly that is the name of the game in conference publishing. Make a big claim in the title and hope the reviewer does not read the fine print.
> If I may translate from the language of academia. "We present beautiful rules in figure 4. But in reality, our implementation relies on a large number of hacks."
Er, this I can understand. Every conference paper only presents you with a simplified view of the contributions. There is no way to describe every corner case within the page limits of a conference paper (specifically, I bet this was submitted to POPL 2025).
In my group I don't allow hacks. Most other good papers I can think of don't do that. It takes new students a while to get used to not maximizing performance at all costs. And if a hack must exist, then it's explained, not as a hack, but as part of the method.
Don't you hate it when you implement some beautiful idea from a paper only to discover that it hardly bares any relationship to the actual method that works?
> There is no way to describe every corner case within the page limits of a conference paper (specifically, I bet this was submitted to POPL 2025).
You're probably right. But POPL allows for unlimited pages in an attached appendix. They can and should describe the full method. Particularly if they're going to play the game of saying that they formalized this.
> Sadly that is the name of the game in conference publishing. Make a big claim in the title and hope the reviewer does not read the fine print.
It's a form of namespace squatting. Do the worst job possible to claim a title that you couldn't execute on, so that when people figure out that problem, they will be forced to cite your non-working solution. I loathe this approach to publishing.
We should punish people for doing. Reject for lack of honesty and your paper can't be published in related conference for X years.
Flagged, this is just a lie of a title.
Yes, this is absolutely correct and on top of this you sometimes have to employ tricks to make the compiler infer the right lifetime or type for the abstraction you're providing. On the other hand, again thanks to the abstraction power of Rust compared to C, you can test the resulting code way more easily using for example Miri.
So C and C++ are the exceptions to the rule, but how do they make it easy to write doubly linked lists? Obviously, the key assumption is that that the developer makes sure that node->next->prev = node->prev->next = node (Ignoring nullptr).
With this restriction, you can safely write a doubly linked list even without reference counting.
However, this isn't true on the pointer level. The prev pointers could be pointing at the elements in a completely random order. For example tail->prev = head, head->prev = second_last and so on. So that going backwards from the tail is actually going forwards again!
Then there is also the problem of having a pointer from the outside of the linked list pointing directly at a node. You would need a weak pointer, because another pointer could have requested deletion from the linked list, while you're still holding a reference.
If you wanted to support this generic datastructure, rather than the doubly linked list you have in your head, then you would need reference counting in C/C++ as well!
What this tells you, is that Rust isn't restrictive enough to enforce these memory safe contracts. Anyone with access to the individual nodes could break the contract and make the code unsafe.
You can certainly replace code using undefined behavior in C code by using defined constructs.
> I don't think this exists, as the numerous critical vulnerabilities over the years have shown. All we have is C that seems to work pretty well often enough to be useful.
I think this highly misleading. Some of the most reliable programs I know are written in C and Rust projects will also have critical vulnerabilities. Most vulnerabilities are not actually related to memory safety and the use of unsafe Rust will also lead to memory safety issues in Rust code. So I see some advantage to Rust but to me it is obviously overhyped.
Zig has much better interoperability with C than Rust, but it’s not memory safe or stable. I think we’ll see quite a lot of Zig adoption in the C world, but I don’t think it’s in direct competition with Rust as such. In my region of the world nobody is adopting Rust, the C++ people are remaining in C++. There was some interest in Rust originally but it never really caught on in any company I know of. Likely for the same reason Go has become huge in younger companies but will not really make its way into companies which are traditionally Java/C# because even if it made sense technically (and it probably doesn’t) it’s a huge change management task. Zig is seeing traction for programs without the need for dynamic memory allocation, but not much beyond that.
Is this the case? E.g. the issue "Prove the Rust type system sound" https://github.com/rust-lang/rust/issues/9883 is closed with comment "This will be an open issue forever. Closing." in 2016: https://github.com/rust-lang/rust/issues/9883#issuecomment-2... .
At least nowadays (since 2022) we do have a language specification for Rust: https://ferrous-systems.com/blog/the-ferrocene-language-spec...
https://dl.acm.org/doi/pdf/10.1145/3597503.3639226
> As for C2Rust, the 5% unsuccessful translations were due to compilation errors, the majority of them caused by unused imports.
I'm rather confused by what that's supposed to mean, since unused imports cause warnings, not errors in Rust.
Neither of these papers include the trait system, unfortunately, and I'm not aware of another line of research that does (yet?).
It frustrates me more than it should, I admit, that people always mention Rust when they talk about safety, but never Ada / SPARK. You want formal verification? Use Ada / SPARK. It has been battle-tested. It has been used for critical systems for a really long time now.
(And a compiler being formally verified vs. being able to write formally verified code means two different things.)
For example if someone on GitHub sees that the project is written in Rust, they are automatically going to assume it is safe, incorrectly so. I do not blame them though.
The concept of the borrow checker has been on a simplified version of rust https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf - work has continued in this area steadily (e.g. see tree borrows)
There's a variety of tools that take rust code and translate it to something a proof system understands, and then checks that it matches a specification. AWS is leading a project to use these to verify the standard library: https://aws.amazon.com/blogs/opensource/verify-the-safety-of...
Alternatively this might be seen as a stepping stone to translating non-formally-verified C to rust, which I understand the US government has expressed a fair bit of interest in.
That seems excessive and tedious.
Concretely: spatial and temporal memory safety are good things, and Rust achieves both. It’s not unique in this regard, nor is it unique in not having a formal definition.
So, back to my original comment, the investment in making a Rust to C transpiler would make a C to safer C transpiler that fed that code into the verification tooling. A small transpiler would be easier to write with huge, immediate gains.
On field proven, there’s two angles: spec and code. Many C/C++ apps didn’t become usable at all until years of iteration based on feedback from field use. An alternative in Rust might have incorrect specs which. From there, a number have had much code review, static analysis, and testing. They have few to no known bugs at any point. So, there are definitely C/C++ applications out there that are field-proven with a decent level of safety.
(Note: Any transpiler might need to be bug for bug and weird behavior for weird behavior compatible to match the implicit spec in the C/C++ code.)
You’re right about the average Rust vs C code, like type system vs correctness. I’d prefer new code be written in safer languages, which I added to my proposal.
If apples to apples on correctness, you’d have to compare C written for verification with Rust. Quite a few C projects have been proven to be correct. Since you’re using a compiler, I’ll add that tools like Softbound+CETS make C code safe automatically.
I do think Rust brings the cost and effort down quite a lot, though. It’s tooling is usually more mature or at least free than most for verifying C.
https://stackoverflow.com/questions/75743030/is-there-a-spec...
Sorry if my previous comment came off as dismissive, it's just that I'm getting increasingly disillusioned with the state of things in this space.
It also strikes me as extraordinarily unlikely that any formal verification effort will use the existing specification, and not build their own (using their own formal language) as they go.
Then the point is hypocritical.
Runtimes for safe programming languages have been implemented in unsafe languages since the dawn of safe programming languages, basically.
EDIT: I see now that you are the cigarette warning guy. In that case I don’t understand what this coy “I think” speculation is about when you made such a bizarre proclamation on this topic.
1. Converting a C program to Rust, even if it includes unsafe code, often uncovers bugs quickly thanks to Rust’s stringent constraints (bounds checking, strict signatures, etc.).
2. automated C to Rust conversion is IMO something that will never be solved entirely, because the design of C program is fundamentally different from Rust; such conversions require a significant redesign to be made safe (of course, not all C programs are the same).
3. in some cases, it’s plain impossible to port a program from C to Rust while preserving the exact semantics, because unsafety can be inherent in the design.
That said, tooling is essential to porting, and as tools continue to evolve, the process will become more streamlined.
At least it's compatible. But that approach is a dead end. To make any progress, translation must recognize the common idioms of the language and upgrade those to the ideomatic forms of the target language. Compiling into Rust generates awful Rust, full of calls to functions that do unsafe C-type pointer manipulation.
The big upgrading problems mostly involve pointers. The most promising result in this paper is that they figured out how to convert C pointer arithmetic into Rust slices. Slices can do most of the things C pointer arithmetic can do, and now someone automated the translation. Pointer arithmetic that can't be translated has to be looked at with deep suspicion.
A useful way to think about this is that raw pointers in C which point to arrays implicitly have a length associated with them. That length is not visible in C source code, but exists somewhere, as a function of the program state. It might be a constant. It might be the size requested back at a "malloc" call. It might be a parameter to a function. It's usually not too hard for maintenance programmers to find array lengths.
That could be an LLM kind of problem. Ask an LLM, "Examine this code. What is the length of array foo?" Then use that to guide translation to Rust by a non-LLM translator. If the LLM is wrong, the resulting Rust will get subscript errors or have an oversize array, but will not be unsafe. Array size info idioms are stylized enough in C that it should be possible to get it right most of the time. Especially since LLMs can read comments.
I agree in principle, and I have strong feelings based on my experience that this is the case, but I think it would be illustrative to have some hard examples in mind. Does anyone know any simple cases to ground this discussion in?
the translated code may (quietly) not behave correctly.
The whole point of them show that example is that they say they catch this case, and bring it to the attention of the programmer: If the original C program further relies on x, our translation will error out, and will ask the
programmer to fix their source code. This is another area where we adopt a “semi-active” approach
to verification, and declare that some patterns are poor enough, even for C, that they ought to be
touched up before the translation takes place.
If Rust was forced to expose such an API (to be on par with C's old API), it would have to use `*const u8` in its signature. Converting that to something that can be used in Rust is unsafe.
Even once converted to &[u8], it now has to deal with non-UTF8 inputs throughout its whole codebase, which is a lot more inconvenient. A lot of methods, like .split_ascii_whitespace, are missing on &[u8]. A lot of libraries won't take anything but a &str.
Or they might be tempted to convert such an input to a String, in which case the semantics will differ (it will now panic on non-UTF8 inputs).
Automated conversion of C to safe fast Rust is hard. Automated conversion of C to safe Rust in general is much easier - you just need to represent memory as an array, and treat pointers as indices into said array. Now you can do everything C can do - unchecked pointer arithmetic, unions etc - without having to fight the borrow checker. Semantics fully preserved. Similar techniques have been used for C-to-Java for a long time now.
Of course, the value of such a conversion is kinda dubious. You basically end up with something like C compiled to wasm, but even slower, and while the resulting code is technically "safe", it is still susceptible to issues buffer overflows producing invalid state, dangling pointers allowing access to data in contexts where it shouldn't be allowed etc.
- A dynamic part specifies what is actually allowed, and totally supports doubly linked lists and other sorts of cyclic mutable data structures.
- A static part conservatively approximates the dynamic part, but is still flexible enough to express the interfaces and usage of these data structures even if it can't check their implementations.
This is the important difference over traditional static analysis of C. It enables `unsafe` library code to bridge the dynamic and static rules in a modular way, so that that extensions to the static rules can be composed safely, downstream of their implementation.
Rust's strategy was never for the built-in types like `&mut T`/`&T` to be a complete final answer to safety. It actually started with a lot more built-in tools to support these patterns, and slowly moved them out of the compiler and runtime and into library code, as it turned out their APIs could still be expressed safely with a smaller core.
Something like Fil-C would be totally complementary to this approach- not only could the dynamic checking give you stronger guarantees about the extensions to the static rules, but the static checks could give the compiler more leverage to elide the dynamic checks.
Perhaps what you were looking for is NativeAOT? Either way C ports really well to C# since it supports a large subset of it "as is" and then some with generics and other features originating from C# itself.
No, only that it complies with a formal specification. The code will have bugs if and only if the specification has bugs.
The difficulty of writing a bug-free formal specification is just as great as writing bug-free code. In some domains it's easier to write the specification, but not in most. Fully specifying what a program shoud do is often the hardest part of programming, after all.
Formal verification is verifying a mathematical model of the program correct, according to certain mathematical correctness properties. That model may not actually represent the real world, or the correctness properties may not actually be the properties that you want to guarantee. Famously, there was the formally verified Java LinkedList implementation that was buggy due to the formal model not taking into account integer overflow.
There are parts of the Rust language and standard library that have been formally verified. That helps provide confidence that the basic model, of having safety properties upheld by unsafe core functions, to be sound.
But the big advantage of Rust, especially for everyday open source code that the world widely depends on, is that it strikes a good balance between a language that people actually want to use, and which can provide good practical safety guarantees.
Rust is far, far safer than C and C++. Most other memory-safe languages also are, but trade that off for lower performance, while Rust provides a similar level of performance as C and C++. And additionally, it's a language that people actually want to use for writing a lot of the core infrastructure.
As far as I know, I have never use any open source software written in Ada/SPARK. People just don't do it. The only reason they generally do is if they need to for functional safety reasons, in a high-criticality system, and they find it easier to get their software certified by writing it that way.
And even in safety critical systems, most people find using a subset of C, with restrictive rules, static checkers to check those, code review, and extensive testing, done by independent teams and testing on real hardware with requirements based tests that achieve 100% coverage at the MC/DC level is considered to be the gold standard of verification.
Formal verification can not possibly provide some of the safety guarantees that testing on real hardware based on actual system level requirements can provide.
Formal verification is one tool in a toolbox. It is useful for providing certain guarantees. But it's less important than many other factors for the actual improvements in safety that Rust can provide; by actually being used, in critical software that is exposed to potential network based exploitation, a memory-safe language like Rust makes a much better foundation than C or C++, and more people will actually use it in such a context than Ada/SPARK.