Oomotion A textobject-oriented editor plugin for VS Code

An editor inspired by Vim, Kakoune and Helix. With tree-sitter and easy-motion support.

TheoryComboViz Polite theory combination visualizer

A visualizer for polite theory combination, demonstrated using Sets. Theory combination is implemented extensively in SMT solvers, which are used for fields such as formal program verification, automated reasoning, and software testing. We also contributed to Z3 Typescript API in this project.

HilbertProver A prover for Hilbert system

An Automatic Theorem Prover for Hilbert System, generating nearly-minimal proofs, with some interesting optimizations.