You might find Viper (Verification Infrastructure for Permission- based Reasoning) from ETH-Zurich useful - https://www.pm.inf.ethz.ch/research/viper.html and https://viper.ethz.ch/tutorial/

I came across this when researching/studying Formal Methods but have not yet really sat down and tried it out.