Investigate the possibility of using the type system of Z formal specification language (Spivey's Z).

http://spivey.oriel.ox.ac.uk/mike/zrm/
http://usingz.com/

[The fuzz type-checker for Z](http://spivey.oriel.ox.ac.uk/mike/fuzz/) (2008)
https://bitbucket.org/Spivey/fuzz

https://en.wikipedia.org/wiki/Z_notation
[Typechecking Z (2000)](http://www-users.cs.york.ac.uk/susan/bib/ss/z/zb-tchk.pdf)