My research mostly falls within formal methods (FM). Right now my big research question is:

Better in this context can mean simpler, more featureful, less buggy, more maintainable, etc.

I am pretty agnostic as to what flavor of FM I use, but right now I work almost exclusively in the Lean 4 programming language/theorem prover . It is my "daily driver" for regular old programming, as well as my main research tool.

LeanSAT Library

Boolean satisfiability on CNFs (SAT) has proven to be a remarkably useful interface for solving instances of many combinatorial and NP-complete problems.

From the "client" side, many combinatorial problems can be encoded as instances of SAT via short, straightforward encodings. From the "provider" side, efficient algorithms exist for solving SAT problems, and researchers have found many classes of common SAT formulas for which performance can be much better than the general case.

The goal of the LeanSAT library is to produce formally verified results which use SAT solvers to perform the difficult or combinatorial reasoning. This includes:

• Verified, composable encoding machinery
• Programmatic interfaces to SAT solvers
• Verified SAT certificate checkers

Joint work with Wojciech Nawrocki, Cayden Codel, and Josh Clune. Available on GitHub.

Collection Interfaces for Lean

Standardized collection interfaces are useful (citation needed). For ~2 years on and off, I've been experimenting with how to design collection interfaces in Lean.

Available on GitHub.