What a journey it's been

Compared to previous fruity weeks, I have to admit that not that many things have been happening and most of the work is wrapping things up and cleaning up.

ERC-8441 spec comments

All of the comments I posted on the ERC-8441 draft[1] were addressed, and the proposal editors requested a few more AI-suggested changes related to readability, which were addressed and merged.

The last contribution

As promised, I finalized the formal verification of the ERC-8441 specs and sent it over to the author for review. The biggest blocker so far (ML-KEM anonymity, ~booooooo) turned out to be a machine burp, and separately I found a paper[2] that appears to provide a proof of its anonymity. One caveat worth stating plainly: that result is for round-3 Kyber, and the mapping to the final FIPS-203 ML-KEM is not formalized — which is why the claim travels as a named assumption rather than a discharged theorem. The whole ERC-8441 scheme can be summarized as:

If a ciphertext doesn't reveal which key it belongs to, the scheme holds.

I got positive feedback from the author and am planning to find more peer reviews for the FV that can be contributed to the proposal.

Presentation

As part of preparing for my presentation, I started going over some old videos from the playlist I assembled for myself at the beginning of the cohort. There's one thing I'd like to recommend to my readers: a DefCon 33 talk about PQC[3] from a quantum-security practitioner — strong on the threat timeline and migration urgency, lighter on the constructions themselves.

VCVio health check

The issue I opened remains unanswered, so I just closed it rather than bother with something nobody requested. However, over the weekend a new tool emerged called EthLib[4] for Lean 4 verification that I need to check out to see what's available there — probably after the cohort 🙂

State of the pq-sap repo

The anonymity games I proposed for VCVio are available in the pq-sap PR[5], since that's where they ended up living. I decided to make the branch with the Lean proofs the only place where ERC-8441 is mentioned, and to keep this repo as a journal of bot-assisted solo research. Some of its pieces might end up being a useful reference (primarily on how not to do things) for someone in the future.

Cleaning up the repo

A bunch of junk had been scattered across the repo alongside heavy AI-augmented work, so I spent most of the time reading all existing markdown files, checking the artifacts, and asking the chatbot to explain some non-core decisions that were made, to make sure I fully understand them. Cleaning it up and figuring out what to keep and what needs to go took a lot of resources from me.

On the way to the big day

Wrapping things up, staying nervous and excited for the upcoming final week. What a journey it's been.

See some of you folks very soon!