# Announcing the Formal Verification Working Group **URL:** \ **Category:** announcements\ **Created:** [April 5, 2018, 7:36pm UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240 "2018-04-05T19:36:47Z")\ **Posts on this page:** 16\ **Page:** 1
**Author:** ![avadacatavra](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/avadacatavra/32/3913_2.png) [@avadacatavra](https://internals.rust-lang.org/u/avadacatavra)\ **Post date:** [April 5, 2018, 7:36pm UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/1 "2018-04-05T19:36:47Z")
At the recent Rust work week in Berlin, we formed a working group to investigate formal methods in Rust. The scope of this working group ranges from projects like [RustBelt](http://plv.mpi-sws.org/rustbelt/) that are intended to develop a formal foundation for the language to projects that will directly analyze Rust programs. Our goals are to provide a central location where we can gather and share information on ongoing efforts. As we make progress, we’d like to look at integration with testing frameworks to provide “testing on steroids.” Our first priorities are currently: - extracting required information from the compiler (e.g. trait impls, types) - writing example specifications to help design a common, extensible way to write annotations on Rust programs We’ll be tracking our progress on [github](https://github.com/rust-lang-nursery/wg-verification) and a [site](https://rust-lang-nursery.github.io/wg-verification/) with more details on ongoing projects. Join us on [gitter](https://gitter.im/rust-lang/wg-verification) or IRC (#wg-verification). We also have a [mailing list](mailto:rust-verification@googlegroups.com). Welcome to Rust’s first **formal** working group ( 😛 ) ---
**Author:** ![gnzlbg](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/gnzlbg/32/3858_2.png) [@gnzlbg](https://internals.rust-lang.org/u/gnzlbg)\ **Post date:** [April 5, 2018, 10:19pm UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/2 "2018-04-05T22:19:31Z")
Is the memory model part of this working group tasks, or is it there some other working group on that? ---
**Author:** ![asajeffrey](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/asajeffrey/32/3002_2.png) [@asajeffrey](https://internals.rust-lang.org/u/asajeffrey)\ **Post date:** [April 5, 2018, 10:27pm UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/3 "2018-04-05T22:27:09Z")
Separate, I think the memory model ended up being part of the unsafe code guidelines? ---
**Author:** ![RalfJung](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ralfjung/32/2415_2.png) [@RalfJung](https://internals.rust-lang.org/u/RalfJung)\ **Post date:** [April 6, 2018, 6:00pm UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/4 "2018-04-06T18:00:06Z")
> [@asajeffrey](#): > > Separate, I think the memory model ended up being part of the unsafe code guidelines? Yes. The verification WG is mostly about how to verify software written in Rust, and concerned with things like tools that let you do that, and how the interaction between the developer, the compiler, and the tool should look like. Eventually, the verification WG (and, in particular, the tool developers) will be a consumer of the memory model that the unsafe code guidelines team came up with. ---
**Author:** ![comex](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/comex/32/2587_2.png) [@comex](https://internals.rust-lang.org/u/comex)\ **Post date:** [April 7, 2018, 12:50am UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/5 "2018-04-07T00:50:56Z")
I think the mailing list may be misconfigured. I wasn’t able to find it by searching the name (`rust-verification`) on Google Groups, and while manually entering the URL [https://groups.google.com/forum/#!forum/rust-verification](https://groups.google.com/forum/#!forum/rust-verification) got me somewhere, the resulting page says “You must be a member of this group to view and participate in it.” (requiring manual approval even to view posts) ---
**Author:** ![skade](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/skade/32/3333_2.png) [@skade](https://internals.rust-lang.org/u/skade)\ **Post date:** [April 9, 2018, 5:22am UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/6 "2018-04-09T05:22:06Z")
> [@avadacatavra](#): > > Welcome to Rust’s first formal working group ( 😛 ) How should I believe this when there's no dress code? ---
**Author:** ![Geal](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/geal/32/1171_2.png) [@Geal](https://internals.rust-lang.org/u/Geal)\ **Post date:** [April 9, 2018, 8:50am UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/7 "2018-04-09T08:50:16Z")
well of course the dress code is formal ---
**Author:** ![avadacatavra](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/avadacatavra/32/3913_2.png) [@avadacatavra](https://internals.rust-lang.org/u/avadacatavra)\ **Post date:** [April 9, 2018, 12:46pm UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/8 "2018-04-09T12:46:11Z")
I think I’ve fixed the issue – is it working now? ---
**Author:** ![Gankra](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/gankra/32/6002_2.png) [@Gankra](https://internals.rust-lang.org/u/Gankra)\ **Post date:** [April 9, 2018, 9:19pm UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/9 "2018-04-09T21:19:52Z")
Is there any industry partners for this project yet? Something to use as a testbed/motivation for verification efforts? e.g. is there a component in firefox that’s particularly hungry for more robust verification? ---
**Author:** ![avadacatavra](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/avadacatavra/32/3913_2.png) [@avadacatavra](https://internals.rust-lang.org/u/avadacatavra)\ **Post date:** [April 9, 2018, 9:36pm UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/10 "2018-04-09T21:36:49Z")
Mostly I’ve been talking to [Galois](https://saw.galois.com/) and some researchers over at [ETH Zurich](http://www.pm.inf.ethz.ch/research/viper.html). These are two established tools that we can use to guide initial investigations. At various conferences/meetings, others have expressed interest. Another inspiration for this WG is the [excellent work](https://blog.mozilla.org/security/2017/09/13/verified-cryptography-firefox-57/) that the NSS team has done with HACL\*. This should be viewed more as an investigatory/research-oriented WG with no immediate FF component target (in my opinion). ---
**Author:** ![gasche](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/gasche/32/1930_2.png) [@gasche](https://internals.rust-lang.org/u/gasche)\ **Post date:** [April 10, 2018, 12:37pm UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/11 "2018-04-10T12:37:23Z")
If you forgive some self-advertisement, I think that a participation of the Rust community to the ML and HOPE workshops at ICFP (see my previous [announce thread](https://internals.rust-lang.org/t/ml-workshop-2018-september-28th-st-louis-usa-call-for-presentations/7209) on internals) could help further the goals of the Rust Verification WG. To verify Rust programs, you need to have a semantics of everyday Rust code, while foundational verification efforts such as RustBelt naturally study a suitably aestheticized subset of the langague (sufficient to express everyday programs, but without syntactic sugar or features designed for convenience, such as lifetime inference or the pattern-matching ergonomics). In a community which decentralizes the surface language design through the RFC process and numerous working groups, the best way to ensure that clean, _formalizable_ translations exist between the evolving surface language and those core/simplified languages is to (1) disseminate precise descriptions of ongoing/new language features and (2) teach the wider “internals” community to use _and produce_ these precise descriptions. Participating to academic workshops on language design is an engaging, low-cost way to get started on that front – and there are enough knowledgeable people in the Rust community to serve as mentors to produce nice submissions. Not everyone can build Iris, but anyone that has gone through the demanding process of language design by RFCs can submit and participate to ICFP-colocated workshops on language design. Consider submitting to the ML workshop! (And encouraging/helping your fellow rustaceans to do it.) ---
**Author:** ![JerryWang304](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/jerrywang304/32/3975_2.png) [@JerryWang304](https://internals.rust-lang.org/u/JerryWang304)\ **Post date:** [April 17, 2018, 1:00pm UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/12 "2018-04-17T13:00:55Z")
I am working on the semantics of Rust. Maybe we can work together. ---
**Author:** ![erlend\_sh](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/erlend_sh/32/5019_2.png) [@erlend\_sh](https://internals.rust-lang.org/u/erlend_sh)\ **Post date:** [May 2, 2018, 3:07am UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/13 "2018-05-02T03:07:13Z")
Related: [https://arxiv.org/abs/1804.10806](https://arxiv.org/abs/1804.10806) [https://news.ycombinator.com/item?id=16970050](https://news.ycombinator.com/item?id=16970050) ---
**Author:** ![RalfJung](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ralfjung/32/2415_2.png) [@RalfJung](https://internals.rust-lang.org/u/RalfJung)\ **Post date:** [May 3, 2018, 11:52am UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/14 "2018-05-03T11:52:12Z")
> [@erlend\_sh](#): > > [[1804.10806] KRust: A Formal Executable Semantics of Rust](https://arxiv.org/abs/1804.10806) And then there is also [[1804.07608] An Executable Operational Semantics for Rust with the Formalization of Ownership and Borrowing](https://arxiv.org/abs/1804.07608) which uses almost the same name but has a disjoint set of authors? ---
**Author:** ![RalfJung](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ralfjung/32/2415_2.png) [@RalfJung](https://internals.rust-lang.org/u/RalfJung)\ **Post date:** [May 15, 2018, 9:00am UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/15 "2018-05-15T09:00:42Z")
> [@avadacatavra](#): > > We also have a [mailing list](mailto:rust-verification@googlegroups.com). FYI, contrary to what Google [says](https://support.google.com/groups/answer/1067205?hl=en) it is actually possible to join this group without getting a Google account. The usual way used to be to send an email to [rust-verification+subscribe@googlegroups.com](mailto:rust-verification+subscribe@googlegroups.com), but nowadays that just links you to [Redirecting to Google Groups](https://groups.google.com/forum/#!forum/rust-verification/join). That form, however, seems to have worked for me. ---
**Author:** ![system](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/system/32/14092_2.png) [@system](https://internals.rust-lang.org/u/system)\ **Post date:** [March 25, 2019, 8:30am UTC](https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240/16 "2019-03-25T08:30:01Z")
This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.