It's still relevant (and probably also rather difficult) to prove that seL4 itself conforms to those best practices.