... and formal verification is where Ada / SPARK wins over Rust.
I mean, we can go on but I think it quite ends there, as far as safety goes. :D
There is a reason for why Ada is used in industries that are mission-critical.
> Ada needs a profile that guarantees that code can't be the source of erroneous execution and constrains bounded errors further.
Not really, you can just use Ada / SPARK and it is all checked at compile-time. Look for my comments where I mention Ada.
Only if SPARK is powerful enough to verify the code you need to write in the first place, which from my experience with SPARK is not a given as soon as access types are involved. Also Rust doesn't need to exclude high level language features just to prove memory safety, whereas SPARK can't even verify any use of controlled types.
If SPARK really were enough, I'd just write all Ada in SPARK of course.
You're partly right that SPARK is conservative, but the claim that it "can't handle access or controlled types" is misleading.
SPARK does support Ada access types (pointers) under a formal permission/ownership model added to GNATprove in recent years. This system - drawn from Rust's borrow-checker ideas - enforces a Concurrent Read, Exclusive Write (CREW) discipline. It enables verification of typical pointer-based structures (singly-linked lists, trees, other acyclic data) via ownership transfers and borrows that the prover can reason about automatically[1]. So long as you follow the ownership rules (no uncontrolled aliasing, no cycles), GNATprove can verify pointer-based code, ensuring the absence of memory leaks and dangling references.
As for controlled types, SPARK excludes them in the verifiable subset because `Initialize`, `Adjust`, and `Finalize` introduce implicit operations that complicate sound reasoning for the automated prover[2]. However, that doesn’t prevent you from using controlled types - you just need to isolate them. The standard pattern is to define them in a `private` part under `pragma SPARK_Mode(Off)` and expose only SPARK-safe wrappers[3]. The controlled operations still run at runtime, but they are hidden from the proof engine. This way, you retain deterministic finalization and prove correctness for the SPARK-visible interface.
In short: SPARK doesn't "exclude high-level features just to prove memory safety" - it modularizes them. It restricts what the prover sees so proofs remain sound and automatic, but you can still use these features through encapsulation. Rust enforces memory safety through its type system at compile time; SPARK aims to prove memory safety plus richer functional properties (absence of runtime errors, contractual correctness) via formal verification. Their goals differ, and SPARK's restrictions are a deliberate trade-off that enable stronger, machine-checked guarantees for high-assurance software.
If you want me to elaborate on the specifics, let me know. Additionally, see https://news.ycombinator.com/item?id=45494263.
Additionally, I am willing to provide more information about what SPARK typically can prove automatically and why some gaps exist.
[1] Jaloyan, Moy, Paskevich - Borrowing Safe Pointers from Rust in SPARK (permission-based alias analysis)
[2] SPARK 2014 User’s Guide, Language Restrictions (implicit operations, excluded features)
[3] AdaCore SPARK tutorials/blogs - exposing controlled types behind SPARK-safe interfaces
There is more than one formal verification library for Rust, although none is as integrated as SPARK I believe.
How does that work?
Why can't other languages have a "formal verification library"?
> How does that work?
Usually taking the IR (MIR) from rustc and translating it to a verifier engine/language, with the help of metadata in the source (attributes) when needed. E.g. Kani, Prusti, Creusot and more.
> Why can't other languages have a "formal verification library"?
I don't think there is a reason that prevents that, and perhaps some have, however it turns out that modelling shared mutability formally is really hard, and therefore the shared xor mutable rule in Rust really helps verification.
Wouldn't C have such a library already if it really was "possible"? You can turn off strict aliasing.
Not a library, but it kinda does: Frama-C will formally verify C code using special comments to write the contracts in, and I hear it can prove more pointer properties than SPARK, although it takes more more effort to maintain a Frama-C codebase due to all the other missing language features.
Does that mean I can use C + Frama-C so I won't have to use Rust (or Ada / SPARK)? :P
Well, I'm not an expert in formal verifications, but there are such libraries, I listed few of them above, you can go and check them. So it is possible.
C doesn't have the shared xor mutable rule - with strict aliasing or without.
I checked them, but I am not convinced and I am not sure why it was brought into this thread.
SPARK has industrial-strength, integrated verification proven in avionics (DO-178C), rail (EN 50128), and automotive (ISO 26262) contexts. Rust's tools are experimental research projects with limited adoption, and they're bolted-on and fundamentally different from SPARK.
SPARK is a designed-for-verification language subset. Ada code is written in SPARK's restricted subset with contracts (Pre, Post, Contract_Cases, loop invariants) as first-class language features. The GNAT compiler understands these natively, and GNATprove performs verification as part of the build process. It's integrated at the language specification level.
Rust's tools retrofit verification onto a language designed for different goals (zero-cost abstractions, memory safety via ownership). They translate existing Rust semantics into verification languages after the fact - architecturally similar to C's Frama-C or VCC (!). The key difference from C is that Rust's type system already guarantees memory safety in safe code, so these tools can focus on functional correctness rather than proving absence of undefined behavior.
Bottom line is that these tools cannot achieve SPARK-level verification for fundamental reasons: `unsafe` blocks create unverifiable boundaries, the trait system and lifetime inference are too complex to model completely, procedural macros generate code that can't be statically verified, interior mutability (`Cell`, `RefCell`) bypasses type system guarantees, and Rust can panic in safe code. Most critically, Rust lacks a formal language specification with mathematical semantics.
SPARK has no escape hatches, so if it compiles in SPARK, the mathematical guarantees hold for the entire program. SPARK's formal semantics map directly to verification conditions. Rust's semantics are informally specified and constantly evolving (async, const generics, GATs). This isn't tooling immaturity though, it's a consequence of language design.
> SPARK has no escape hatches
It does, you can declare a procedure in SPARK but implement it in regular Ada. Ada is SPARK's escape hatch.
This is just as visible in source code as unsafe is in Rust, a procedure body will have SPARK_Mode => Off.
Yes, SPARK provides an explicit escape hatch, but it is meaningfully different from Rust's `unsafe`.
In SPARK: you keep the spec in the verifiable world (a SPARK-visible subprogram declaration) and place the implementation outside the proof boundary (for example in a body or unit compiled with `pragma SPARK_Mode(Off)`). The body is visible in source but intentionally opaque to the prover; callers are still proved against the spec and must rely on that contract.
In Rust: `unsafe` is a lexical, language-level scope or function attribute that disables certain compiler/borrow checks for the code inside the block or function. The unchecked code remains inline and visible; the language/borrow-checker no longer enforces some invariants there, so responsibility shifts to the programmer at the lexical site.
Practical differences reviewers should understand:
- Granularity: `unsafe` is lexical (blocks/functions); SPARK's hatch is modular/procedural (spec vs body).
- Visibility: Rust's unchecked code is written inline and annotated with `unsafe`; SPARK's unchecked implementation is placed outside the prover but the spec remains visible and provable.
- Enforcement model: Rust's safety holes are enforced/annotated by the compiler's type/borrow rules (caller and callee responsibilities are explicit at the site). SPARK enforces sound proofs on the interface; the off-proof body must be shown (by review/tests/docs) to meet the proven contract.
- Best practice: keep off-proof bodies tiny, give strong pre/postconditions on the SPARK spec, minimize the exposed surface, and rigorously review and test the non-SPARK implementation.
TL;DR: `unsafe` = "this code block bypasses language checks"; SPARK's escape hatch = "this implementation is deliberately outside the prover, but the interface is still what we formally prove against."
I think I did say:
> although none is as integrated as SPARK I believe
And yes, they're experimental (for now). But some are also used in production. For example, AWS uses Kani for some of their code, and recently launched a program to formally verify the Rust standard library.
Whether the language was designed for it does not matter, as long as it works. And it works well.
> `unsafe` blocks create unverifiable boundaries
Few of the tools can verify unsafe code is free of UB, e.g. https://github.com/verus-lang/verus. Also, since unsafe code should be small and well-encapsulated, this is less of a problem.
> the trait system and lifetime inference are too complex to model completely
You don't need to prove anything about them: they're purely a type level thing. At the level these tools are operating, (almost) nothing remains from them.
> procedural macros generate code that can't be statically verified
The code that procedural macros generate is visible to these tools and they can verify it well.
> interior mutability (`Cell`, `RefCell`) bypasses type system guarantees
Although it's indeed harder, some of the tools do support interior mutability (with extra annotations I believe).
> Rust can panic in safe code
That is not a problem - in fact most of them prove precisely that: that code does not panic.
> Most critically, Rust lacks a formal language specification with mathematical semantics
That is a bit of a problem, but not much since you can follow what rustc does (and in fact it's easier for these tools, since they integrate with rustc).
> Rust's semantics are informally specified and constantly evolving (async, const generics, GATs)
Many of those advancements are completely erased at the levels these tools are operating. The rest does need to be handled, and the interface to rustc is unstable. But you can always pin your Rust version.
> This isn't tooling immaturity though, it's a consequence of language design.
No it's not, Rust is very well amenable to formal verification, despite, as you said, not being designed for it (due to the shared xor mutable rule, as I said), Perhaps even more amenable than Ada.
Also this whole comment seems unfair to Rust since, if I understand correctly, SPARK also does not support major parts of Ada (maybe there aren't unsupported features, but you not all features are fully supported). As I said I know nothing about Ada or SPARK, but if we compare the percentage of the language the tools are supporting, I won't be surprised if that of the Rust tools is bigger (despite Rust being a bigger language). These tools just support Rust really well.
> Whether the language was designed for it does not matter, as long as it works. And it works well.
It matters fundamentally. "Works well" for research projects or limited AWS components is not equivalent to DO-178C Level A certification where mathematical proof is required. The verification community distinguishes between "we verified some properties of some code" and "the language guarantees these properties for all conforming code."
> Few of the tools can verify unsafe code is free of UB
With heavy annotation burden, for specific patterns. SPARK has no unsafe - the entire language is verifiable. That's the difference between "can be verified with effort" and "is verified by construction."
> You don't need to prove anything about [traits/lifetimes]: they're purely a type level thing
Trait resolution determines which code executes (monomorphization). Lifetimes affect drop order and program semantics. These aren't erased - they're compiled into the code being verified. SPARK's type system is verifiable; Rust's requires the verifier to trust the compiler's type checker.
> The code that procedural macros generate is visible to these tools
The macro logic is unverified Rust code executing at compile time. A bug in the macro generates incorrect code that may pass verification. SPARK has no equivalent escape hatch.
> some of the tools do support interior mutability (with extra annotations I believe)
Exactly - manual annotation burden. SPARK's verification is automatic for all conforming code. The percentage of manual proof effort is a critical metric in formal verification.
> That is not a problem - in fact most of them prove precisely that: that code does not panic
So they're doing what SPARK does automatically - proving absence of runtime errors. But SPARK guarantees this for the language; Rust tools must verify it per codebase.
> you can follow what rustc does (and in fact it's easier for these tools, since they integrate with rustc)
"Follow the compiler's behavior" is not formal semantics. Formal verification requires mathematical definitions independent of implementation. This is why SPARK has an ISO standard with formal semantics, not "watch what GNAT does."
> Rust is very well amenable to formal verification [...] Perhaps even more amenable than Ada
Then why doesn't it have DO-178C, EN 50128, or ISO 26262 certification toolchains after a decade? SPARK achieved this because verification was the design goal. Rust's design goals were different - and valid - but they weren't formal verifiability.
> SPARK also does not support major parts of Ada
Correct - by design. SPARK excludes features incompatible with efficient verification (unrestricted pointers, exceptions in contracts, controlled types). This is intentional subsetting for verification. Claiming Rust tools "support more of Rust" ignores that some Rust features are fundamentally unverifiable without massive annotation burden.
The core issue: you're comparing research tools that can verify some properties of some Rust programs with significant manual effort, to a language designed so that conforming programs are automatically verifiable with mathematical guarantees. These are different categories of assurance.
I could be wrong, but the Ferrocene Language Specification, FLS, adopted by Rust as its specification, may be severely incomplete.
For instance, it describes atomics, but I am not sure that it defines Rust's memory model or the semantics of atomics anywhere.
This Ferrocene page looks very short, and has a lot of links to Rust API documentation.
https://public-docs.ferrocene.dev/main/specification/concurr...
Conversely, the Rustonomicon has this page that says that Rust just uses C++20's memory model for its atomics. Yet I do not believe that memory model is defined anywhere in FLS.
https://doc.rust-lang.org/nomicon/atomics.html
I do not know if FLS defines unwinding of panics anywhere either.
Is FLS severely incomplete regarding rustc and Rust, despite being adopted by Rust as its specification? It almost seems fake.
It is certainly incomplete. Virtually all specifications for programming languages are. It is good enough for safety critical work, which is a higher bar than most.
The idea is that you adopt them and improve them over time. It is more complete than the reference, which is the previous project in this area.
Rust does have a qualified compiler: Ferrocene. It supports ISO 26262 (ASIL D), IEC 61508 (SIL 4) and IEC 62304 currently, with more on the way, including plans for DO-178 I believe. It’s being driven by actual adoption, so they’ve started in automotive and will move to other industries eventually.
Do you happen to know how Ferrocene relates to AdaCore's Rust compiler?
https://www.adacore.com/press/adacore-announces-the-first-qu...
> ISO 26262 (ASIL D)
Isn't that only for a very small subset of Rust and its standard library?
Also, do you happen to be able to explain this comment?
https://reddit.com/r/rust/comments/1nhk30y/ferrous_systems_j...
> I think it's important to note, the certification is only for a subset of the run-time, which means some language features will not be available. Also, the certification is only to SIL-2 level, so any projects requiring SIL-3 or 4 will still not be able to use the Ferrocine compiler!
I know that Ferrocene and AdaCore were working together, but then parted ways. I am assuming they're both doing roughly the same thing: qualifying the upstream compiler with some patches. I know that Ferrocene's patches are mostly adding a new platform, they've upstreamed all the other stuff.
> Isn't that only for a very small subset of Rust and its standard library?
It is currently for the compiler only. This ties into the next bit, though:
> Also, do you happen to be able to explain this comment?
Yeah, you can see me posting in that thread, though not that specific sub-thread. Rust has a layered standard library: core, alloc (which layers memory allocation on top of core), and std (which layers OS specific things on top of that). There's three parts to this comment:
First, because it's only core, you don't get the stuff from alloc and std. So, no dynamic memory allocation or OS specific things like filesystem access. That's usually not a problem for these kinds of projects. But that's what they mean by 'some language features will not be available', but they're mistaken: all language features are available, it's some standard library features that are not. No language features require allocation, for example.
Second, they qualified a subset of libcore for IEC61508. A founder of Ferrous mentions that IS 26262 is coming next, they just had a customer that needed IEC61508 quickly, so they prioritized that. This is how it relates to the above, for ISO 26262, it's just the compiler currently.
I mentioned Ferrocene here: https://news.ycombinator.com/item?id=45494263.
> It matters fundamentally. "Works well" for research projects or limited AWS components is not equivalent to DO-178C Level A certification where mathematical proof is required
As said in a sibling comment, certification to Rust starts to appear. Rust is young and its usage in regulated industries is just barely beginning. Ada and SPARK are old and mature. It's not a fair comparison - but that doesn't mean Rust couldn't get there.
> > Few of the tools can verify unsafe code is free of UB > > With heavy annotation burden, for specific patterns
> > some of the tools do support interior mutability (with extra annotations I believe) > > Exactly - manual annotation burden.
SPARK does not support the equivalent (shared mutable pointers) at all. Rust verifies do with a heavy annotation burden. What's better?
> Trait resolution determines which code executes (monomorphization). Lifetimes affect drop order and program semantics. These aren't erased - they're compiled into the code being verified. SPARK's type system is verifiable; Rust's requires the verifier to trust the compiler's type checker.
Has the Ada compiler formally verified? No. So you're trusting the Ada type checker just as well.
The Ada specification was, if I understand correctly, formally defined. But there are efforts to do that to Rust as well (MiniRust, a-mir-formality, and in the past RustBelt).
> The macro logic is unverified Rust code executing at compile time. A bug in the macro generates incorrect code that may pass verification. SPARK has no equivalent escape hatch.
And if you have a script that generates some boilerplate code into your Ada project, is the script logic verified? The outputted code is, and that's what important. Even with full formal verification, proving that the program fulfills its goals, you don't need to verify helpers like this - only the code they generate. If it works, then even if the script is buggy, who cares.
> So they're doing what SPARK does automatically - proving absence of runtime errors
Exactly - that's the point, to prove free of runtime errors.
I'm not sure what you mean by "SPARK guarantees this for the language; Rust tools must verify it per codebase" - does SPARK not need to verify separate codebases separately? Does it somehow work magically for all of your codebases at once?
It's clear at this point that neither of us will get convinced, and I think I said everything I had about this already.
Have fun developing with Ada!
rustc and Rust have some rather serious type system holes and other kinds of issues.
https://github.com/Speykious/cve-rs
https://github.com/lcnr/solver-woes/issues
That first one is an implementation bug that's never been discovered in the wild.
Regardless, all projects have bugs. It's not really germane to qualification, other than that qualification assumes that software has bugs and that you need to, well, qualify them and their impact.
> Certification to Rust starts to appear. Rust is young and its usage in regulated industries is just barely beginning.
Ferrocene has ISO 26262 qualification for the compiler, not verification tools. That's compiler correctness, not formal verification of programs. SPARK's GNATprove is qualified for proving program properties - fundamentally different.
> SPARK does not support the equivalent (shared mutable pointers) at all. Rust verifies do with a heavy annotation burden. What's better?
SPARK supports controlled aliasing through ownership aspects and borrow/observ annotations - but these are designed into the verification framework, not bolted on. The key difference: SPARK's aliasing controls are part of the formal semantics and verified by GNATprove automatically. Rust's unsafe shared mutability requires external verification tools with manual proof burden. SPARK deliberately restricts aliasing patterns to those that remain efficiently verifiable: it's not "can't do it" it's "only allow patterns we can verify".
> Has the Ada compiler formally verified? No. So you're trusting the Ada type checker just as well.
Qualified compilers (GNAT Pro) undergo qualification per DO-178C/ED-12C. The difference: SPARK's semantics are formally defined independent of the compiler. Rust verification tools must trust rustc's implementation because Rust has no formal specification. When rustc changes behavior (happens frequently), verification tools break. SPARK's specification is stable.
> And if you have a script that generates some boilerplate code into your Ada project, is the script logic verified?
External build scripts are different from language features. Procedural macros are part of Rust's language definition and can access compiler internals. If you use external code generation with SPARK, you're explicitly stepping outside the language's guarantees - and safety standards require justification. Rust embeds this escape hatch in the language itself.
> I'm not sure what you mean by "SPARK guarantees this for the language; Rust tools must verify it per codebase"
SPARK: If your code compiles in the SPARK subset, overflow/division-by-zero/array bounds are automatically proven impossible by language rules. You can add contracts for functional correctness.
Rust tools: You must annotate code, write invariants, and run verification per program. The language provides memory safety via the type system, but not freedom from arithmetic errors or functional correctness. These must be proven per codebase with tools.
The distinction: language-level guarantees vs. per-program verification effort.
> It's clear at this point that neither of us will get convinced
Fair enough, but the fundamental difference is whether verification is a language property or a tool property. Both approaches have merit for different use cases.
> No it's not, Rust is very well amenable to formal verification, despite, as you said, not being designed for it (due to the shared xor mutable rule, as I said), Perhaps even more amenable than Ada.
I would like to add a few clarifications that I may not have mentioned in my other reply.
You are correct that Rust's ownership/borrow model simplifies many verification tasks: the borrow checker removes a great deal of aliasing complexity, and that has enabled substantial research and tool development (RustBelt, Prusti, Verus, Creusot, Aeneas, etc.). That point is valid.
However, it is misleading to claim Rust is plainly more amenable to formal verification than Ada. SPARK is a deliberately restricted subset of Ada designed from the ground up for static proof: it ships with an integrated, industrial-strength toolchain (GNATprove) and established workflows for proving AoRTE and other certification-relevant properties. Rust's type system gives excellent leverage for many proofs, but SPARK/Ada today provide a more mature, production-proven path for whole-program safety and certification. Which is preferable therefore depends on what you need to verify - research or selected components versus whole-program, auditable certification evidence.
SPARK/Ada is used in many mission-critical industries (avionics, rail, space, nuclear, medical devices) for a reason: the language subset, toolchain, and development practices are engineered to produce certifiable evidence and demonstrable assurance cases.
Rust brings superior language ergonomics and strong compile-time aliasing guarantees, but it faces structural barriers that make SPARK's level of formal verification fundamentally unreachable. These are not matters of tooling immaturity, but of language design and semantics:
- Rust allows pervasive unsafe code, which escapes the borrow checker's guarantees. Every unsafe block must be modelled and verified separately, defeating whole-program reasoning. SPARK forbids such unchecked escape hatches within the verified subset.
- Rust's semantics include undefined behavior and panics, which cannot be statically ruled out by the compiler. SPARK, by contrast, can prove statically that such run-time errors are impossible.
- Rust's rich features (lifetimes, traits, interior mutability, macros, async, etc.) greatly complicate formal semantics. SPARK deliberately restricts such constructs to preserve provable determinism.
- Rust lacks a single, formally specified, stable verification subset. SPARK's subset is precisely defined and stable, with a formal semantics that proofs can rely on across versions.
- Rust's verification ecosystem is fragmented and research-oriented (Prusti, Verus, Creusot, RustBelt), whereas SPARK's GNATprove toolchain is unified, production-proven, and already qualified for use in DO-178C, EN-50128, and IEC-61508 workflows.
- Certification for Rust toolchains (qualified compilers, MC/DC coverage, auditable artifacts) is only beginning to emerge; SPARK/Ada toolchains have delivered such evidence for decades.
In short, Rust's design - allowing unsafe code, undefined behavior, and a complex evolving feature set - makes SPARK-level whole-program, certifiable formal verification structurally impossible. SPARK is not merely a verifier bolted onto Ada: it is a rigorously defined, verifiable subset with an integrated proof toolchain and an industrial certification pedigree that Rust simply cannot replicate within its current design philosophy.
If your objective is immediately auditable, whole-program AoRTE proofs accepted by certifying authorities today, SPARK is the practical choice.
I hope this sheds some light on why SPARK's verification model remains unique and why Rust, by design, cannot fully replicate it.
I'm a long term Ada developer who has also used SPARK in the past (SPARK was/is great). I've been looking into Rust out of curiosity. I will dispute that "Rust brings superior language ergonomics". To me, Rust's syntax is unnecessarily cryptic and ugly. In particular, Ada's syntax and semantics for exact, low-level data representation and hardware interfacing is much more ergonomic than Rust's.