Broadly speaking, does Evergreen allow me to prove/enforce more invariants than what Verus/rust allows? Evergreen certainly looks cleaner since its built in rather than bolted on.