型による静的検証能力の高い組版システムの開発は、2017年未踏テーマに採択されたプロジェクト。クリエータ諏訪 敬之によって開発が行われた。担当PMは竹迫 良範。

成果報告時は「型による静的検証能力の高い組版システムの開発 ー SATySFi：Typesetting System with a Type System ー」と題された。