Our synthetic Euclidean Geometry proof assistant is now open for public contributions! We created this together as a class in my Build Your Own Proof Assistant course this semester. Please give it a spin and consider contributing! https://github.com/nicegeo/nicegeo

Some features:

- Dependent-type-theory-based proof kernel
- Synthetic Euclidean geometry layer (axiomatization of System E) with elaboration exhaustively tested
- Tactic-based interactive proofs
- Holes, bidirectional type checking, and unification
- Proof state management
- Custom tactic framework in OCaml
- Pretty-printing and error reporting
- Kind error messages
- Standard library (Euclib) for Euclidean geometry
- VSCode IDE plugin with many novel usability features
- Some geometry-specific proof automation

What's next:

- Interactive visual proofs
- Tabular proofs
- More geometry-specific & advanced automation
- Better support for user-written automation (e.g., a tactic language)
- Stronger IDE integration
- Expansions to Euclib
Please see our GitHub issues for more!

Our proof assistant is MIT licensed. Please see our contributor's guide if you would like to contribute. We especially welcome contributions addressing any of our open GitHub issues! https://github.com/nicegeo/nicegeo?tab=contributing-ov-file

This was a very impressive collaboration of about 20 students from many different backgrounds, who all came together for a semester to build something real. Everything from the domain to the design philosophy to the kernel to the automation was built from scratch collaboratively!

I'm giving a talk at NJPLS (5/22 at Penn)! It’s about cool things you can do with a DSL for specifying hardware communication protocols!

Joint work w/ @nikilshyamsunder, Francis Pham, @adrian & @ekiwi

https://njpls.org/may2026.html

I'm deeply honored to have received one of this year's ASPLOS Most Influential Paper awards, for the Overshadow paper from way back in ASPLOS 2008.

This was a really fun project to work on with a really great group of people at VMware.

I shared some retrospective thoughts on the project at the conference today; I'll share some more here once I have time to write them up!

🏄 Today we released Surfer 0.6.0 🎉 This release contains a bunch of improvements including configurable key bindings, mapping translators, new commands and much more! Oh, and we have a new icon!

Also, some students will work on better annotations in Surfer soon. They asked for opinions here: https://forms.gle/CKqtgemjrNsfE7XY7

You can read the full change-log for the new release over at https://gitlab.com/surfer-project/surfer/-/releases/v0.6.0

Oh, and we have a new logo!

Finally, we have a proper journal paper about Spade 🎉!

It is a pretty complete description of the current state of the language, but I'm honestly more excited about the way we managed to argue for having a new HDL at Spade's abstraction level, roughly RTL but with zero cost abstractions on top

https://dl.acm.org/doi/10.1145/3793550

For those who missed my #Asahilinux #39c3 talk, it's available at https://media.ccc.de/v/39c3-asahi-linux-porting-linux-to-apple-silicon now.

I've also just pushed my slides to https://github.com/svenpeter42/39c3 and uploaded them as PDF to https://cfp.cccv.de/39c3/talk/YGHB9K/