Rust Ownership/Borrowing proof

Hello

I am interested in Rust's design and I heard that the creators made a proof that Rust's ownership/borrowing system is correct.

I tried to find it on the Internet, but without success.

But because I still want to read it, I am asking here.

Thanks in advance