Rzk: a Proof Assistant for Synthetic ∞-Categories
A comprehensive description of rzk, a proof assistant implementing a refinement of Riehl and Shulman’s simplicial type theory (RSTT) for synthetic reasoning about ∞-categories. The type theory implemented by rzk is a computational variant of RSTT, adjusted to make type checking practical.
We define a translation from RSTT to rzk and prove that it is sensible: every RSTT proof translates to an rzk proof (faithfulness), and rzk proves nothing new about RSTT types (conservativity). The paper also gives a tutorial introduction to proving in rzk, and describes the implementation, including the type-checking algorithm and the automated prover for the logic of shapes.
The preprint describes rzk v0.7.8. Ancillary files include the code of every example in the paper, together with the scripts and trace behind the evaluation.
Code: rzk-lang/rzk
Kudasov, N., Sim, V., Ahrens, B. (2026). "Rzk: a Proof Assistant for Synthetic ∞-Categories." arXiv preprint arXiv:2607.12207.