OATP, a Lean 4 REPL and CLI for automated theorem provers. It parses TPTP and runs local and online provers. It started as my Haskell online-atps.

What I wrote for it along the way:

• Grip, a graded parser-combinator library, inspired by prim-parser. Recursive parsers terminate without partial.
• grip-tptp, TPTP on Grip.
• grip-json, JSON on Grip.
• grip-diagnostics, readable parse errors.
• Argus, typed command-line parsing; help and shell completions come from one spec.
• termcolor, ANSI colours and styled text, with layout, diagnostics, widgets, terminal and repl.
• calc-chat, a chat-shaped terminal calculator, to try termcolor.
• precommit-lean, hooks for Lean style, module names and allowed axioms, plus the /lean-format command.

I used to think Haskell would become the next big language for me at least. Now I think it is any theorem prover with general-purpose programming support and dependent types. That is Lean 4, it could have been Agda, but AI simply pushed Lean so much, made it mainstream, that it would be a mistake to not learn it, and it's really fun, actually! I still miss Agda-way of proving things, proof-term construction I mean.

At Heliax, on the Juvix language, where I was one of the main contributors:

• juvix-docs, vscode-juvix, juvix-stdlib and juvix-mode, which I maintained.
• juvix-mkdocs, literate docs, used for the Juvix tutorial.

Distributed systems, also at Heliax:

• mailbox-actors, an actor model where mailboxes are actors too.
• Engines, the same idea for Anoma's node protocols, with a ticker as the example.
• elixir-tango, a small Tango: replicated in-memory data structures.
• AVM Lab, a formal spec of a distributed virtual machine, down to interaction trees.

From my master's:

• online-atps, runs the provers on SystemOnTPTP.
• apia, which I contributed to, proves Agda first-order goals with them.
• athena, turns Metis proofs into Agda terms.
• agda-prop and agda-metis, propositional logic and Metis proofs in Agda, tested on prop-pack.

From my PhD:

• Synthetic graph theory, graphs in HoTT.
• agda-unimath, univalent mathematics in Agda. I co-created it, but have been mostly away since.
• hott-cheatsheets and mini-hott, if you are learning HoTT.

Older still:

• agda-pkg, apkg, a package manager for Agda. Unmaintained; I don't think Agda needs one anymore.
• flask-ponywhoosh, full-text search for Flask, on ponywhoosh.

Nowadays, I build with agentic tools at work and have more recently started using them for my personal projects. A lot of people are against it for several reasons. To me, AI is another tool in my toolbox. I continue building as before, but more, and it is hard to keep the same level of supervision. For the projects I really need, I still write and review every line. But I don't want to spend all my time and energy reviewing everything I try. Some of these projects were built with AI, some only in part, some on my own, and some before any of this. The level of supervision varies. That distinction stopped mattering to me.