Indeed, and this is why people who care about this are also proving memory safety in C. The issue is that we do not have good open-source tooling that specifica

Indeed, and this is why people who care about this are also proving memory safety in C. The issue is that we do not have good open-source tooling that specifically focuses on formal verification of memory safety in C.