> Since it is the unverified SMP config of the kernel I don't disagree with your point (formal verification does not rid you of all bugs), but this is not the

> Since it is the unverified SMP config of the kernel I don't disagree with your point (formal verification does not rid you of all bugs), but this is not the subject of the linked issue. This was a bug in an unverified path.