The exact code might not be deterministic but the behavior can be if your spec uses something like Dafny or TLA+ and is detailed enough