No, but small pieces of it are, and there's active work to extend it The concept of the borrow checker has been on a simplified version of rust https://people.

No, but small pieces of it are, and there's active work to extend it The concept of the borrow checker has been on a simplified version of rust https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf 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-the-rust-standard-library/ https://aws.amazon.com/blogs/opensource/verify-the-safety-of...