Yep, this is the correct answer. Accessing released memory is undefined in C, but well-defined in Vale. The goal is to ensure that the user predictably+safely gets either a segmentation fault or an assertion failure.

We have a future improvement planned here too: for unrelated reasons (to support generation pre-checking) the random generational references implementation will soon not even unmap any virtual address space, instead remapping it to a central page, so we won't even get any segmentation faults, just assertion failures.