The current release is "v0.4". The following features are implemented:
The major new features:
New syntax for class declarations
Abstract classes with inductive abstract classes and abstract classes with formal generics.
Processes.
Generation of executable programs.
Hoare Logic
Mutable data structures
The major new features:
Inductively defined sets and relations
Syntax support for induction proofs, conditional proofs, proofs by contradiction, existential proofs, transitivity proofs.