I was thinking that maybe a good part of Z-notation would fit really
good in the already logic, or assumptions system, since Z-notation is
currently defined as an ISO standard would be a nice addition to sympy
and an easy to constrain GSOC project.

The idea then is just to follow the ISO standard, or a previous
draft[1] if we can't get it. We can avoid all the parsing process, and
working immediately  with the concrete syntax tree defining and
reusing classes from the logic and assumption module. The definition
is split in phases, which after the parsing process are:
Characterizing, Syntactic Transformation, Type Inference, Semantic
Transformation, Semantic relation. I will try to unfold this sections
in more concrete steps for the GSOC (I have a test tomorrow, so I have
to stop here until Thursday).

What I imagine is a system based on Z-notation able to validate the
correctness of a model. So we can describe the model with Python
object and building as normal python, and after the Summer a parser
for plain Z-notation document could be made. I think that the already
present pprint facilities on sympy will ease the printing process of a
model.

If anyone has any comment about this, I don't really know if you think
this fits correctly on sympy, but it seems to me that it would be a
good complement for the logic, and assumptions module, since is not
only useful to verify models of computing systems, but also to really
proof mathematical theorems.

We can also use some Isabelle/HOL ideas in this project too, look what
Isabelle can do [2].

[1] http://std.dkuug.dk/jtc1/sc22/open/n3187.pdf
[2] http://afp.sourceforge.net/

Some more docs:
[3] http://iweb.dl.sourceforge.net/project/hol/hol/kananaskis-3/kananaski...
[4] http://www.lemma-one.com/ProofPower/specs/specs.html