Why not use Verus?
It augments Rust with Z3 and is not a pile of unverified slop.
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?
Verus, not Venus: https://verus-lang.github.io/verus/guide/
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?
Verus, not Venus: https://verus-lang.github.io/verus/guide/