3 ms·

Hi, I (Shuxian) worked with Michael on this project. Happy to answer any questions! We'll also post a followup next week on formally verifying our unsafe primit

Hi, I (Shuxian) worked with Michael on this project. Happy to answer any questions! We'll also post a followup next week on formally verifying our unsafe primitives in the style of RustBelt (https://plv.mpi-sws.org/rustbelt https://plv.mpi-sws.org/rustbelt), if that interests you.

wsx-antithesis 7mo ago
The sequel is now up at https://antithesis.com/blog/2026/rust_formal_methods/ https://antithesis.com/blog/2026/rust_formal_methods/