It's backed by z3, an SMT solver. There are theories in SMT for strings that can sometimes answer questions of your first flavor, but I don't know if they're in

It's backed by z3, an SMT solver. There are theories in SMT for strings that can sometimes answer questions of your first flavor, but I don't know if they're in z3. Solvers can also answer questions of your second variety, but again, sometimes they can't, and they can't be guaranteed to in general. For an example, consider this example: https://rise4fun.com/Dafny/Cube https://rise4fun.com/Dafny/Cube where the "ensures" on the return value enforces exactly that. You also should be able to write set-inclusion style queries like your second clause, i.e. a function that takes an element and a list of elements as an input and only returns true if the element is contained within the list of elements. I think? I'm not sure why you couldn't. Of course, whether or not that does what you think it does or not depends on how something can get written to that database - if there was a path to write something new to your exclusion list from elsewhere in your application, then the "verified" code would return true when you would think it would return false but it was doing exactly what you told it to do. Is this a problem with your design, or the verification? I'd argue the design, but verification-nihilists would probably say it's a problem with the verification.