Haven't heard of Venus (the programming language), but it sounds interesting. I'm curious to know what you mean by verified?

Do you happen to know if Venus has a Result type with canonical error codes, pipes, and other ergonomics?

Does it have C parity performance?