Servo is not using Quark, and is not formally verified. I assume the link on the Servo page is along the lines of pointing out another cool project in a similar space of writing safer browsers.
Formal verification is cool, but speaking as somebody who worked out it for about 7 years, it is not really ready to be used in large software. Most people care much more about performance and features for their browser. Hopefully by writing a browser in Rust instead of C++, the result will be much more secure, but not have to make many compromises.
That said, we would like to at least formally verify that the core subset of Rust's type system is sound. That has important practical implications for Servo: it means that any (potentially exploitable) memory safety problems in the safe part of Servo will be of the "straightforward compiler bug" variety and not the "oh no, now we have to redesign the type system and break everyone's code" variety.
What is the current state of formal verification in Rust (of the language, of compilers, of other programs)? I would assume that since parts of the language are still undergoing change there isn't much work towards super-rigorous proofs until that gets nailed down. Has there been any provisional work in this direction, and is there any work towards making formal methods practical for Rust?
I like the idea of formal methods, but my familiarity with the subject is entry-level at best, so I don't even know what sort of details I should be asking about here =P.
Niko Matsakis, Rust's type theory guru, has been working on a formal model of Rust's type system to prove its soundness. Not sure how much of it is published yet, but I did find this: https://github.com/nikomatsakis/rust-redex
Few languages have any formal verification work at all. There is a verified C compiler (CompCert; it comes with a guarantee that the compiled assembly is a correct compilation of the source, and it does some very basic verified optimizations) and a verified ML compiler (CakeML, see this year's POPL proceedings).
Few languages have verified anything—verification is still very challenging to do.
A proof of type safety of a language, which I think is what pcwalton is talking about, is a different beast than the proof of the correctness of a compiler, which is what you are talking about.
I actually cannot think of any languages except SML that have complete formal proofs of type safety. Now, I may simply be forgetting something obvious. But Haskell's type systems keeps growing by little features here and there, so no full proof is anywhere; OCaml doesn't have a formal semantics, so it sure as hell doesn't have a proof of type safety (in the usual "a well-typed program doesn't go wrong" sense); Java is unsound (in a particular manner of speaking, of course); C# seems too complicated to have such a proof. The Go authors don't seem the type. Rust is the language in question. Those seem like the big players.
Formal verification is cool, but speaking as somebody who worked out it for about 7 years, it is not really ready to be used in large software. Most people care much more about performance and features for their browser. Hopefully by writing a browser in Rust instead of C++, the result will be much more secure, but not have to make many compromises.