The formal verification angle is what makes this interesting. Most coding agents optimize for "code that compiles and passes tests" — that's a low bar. Curious whether the proof artifacts are persisted for audit trails or thrown away after verification.