Well they claim it is a HoTT (thus presumably univalent) and furthermore has higher inductive types, neither of which exist in Coq's CIC.

For example, they emphasise that function extensionality is a theorem here: https://arend-lang.github.io/about/arend-features (not true in CIC).

It would just be nice to see a list of the rules.

Still I don't want to get hung up on this; the rules must exist somewhere and presumably will become more discoverable. The project looks superb.