The part that’s not clear to me is, does the spec actually align with what’s been implemented, or has the spec only been formally verified. I think the risk with vibe coding this sort of thing is that claude assures you the rust code implements the spec when it doesn’t