[alexisread]

There are many properties as such, but we can still prove many properties about a program despite non-deterministic behaviour, using hidden logic https://cseweb.ucsd.edu/~goguen/pps/hherb.ps

As such, a proof system which incorporates behavioural specification is highly desirable.