Eurydice compiles (a modest subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.

A verification toolchain for Rust programs

Interface with the rustc compiler for the purpose of program verification

A Rust verification tool

The formally verified crypto library for Rust

A Proof-oriented Programming Language

Empowering everyone to build reliable and efficient software.

HACL*, a formally verified cryptographic library written in F*

Bertie TLS 1.3 Implementation

KaRaMeL is a tool for extracting low-level F* programs to readable C code

Nix overlay for Lean 4, and lake2nix

write scripts in compiled languages that run in the nix ecosystem, with no separate build step

Ferrocene Language Specification

RFCs for changes to Rust

This tool formalizes the operation of match ergonomics.

A Rust library for building interactive prompts

The Dark Arts of Advanced and Unsafe Rust Programming

Rust Project Goals tracker

Rust teams structure

A Rust compiler front-end for IDEs