The Solidity compiler was built with a high degree of paranoia, extensive defensive coding, and a custom-built fuzzer that caught bugs before it made its way to production. It has almost no external dependencies and a tightly controlled end-to-end compilation pipeline. One of my proudest moments was a piece of work I put in to verify that a change in memory model was correct. In doing so, I discovered a very subtle bug that likely would have slipped through to production. The work ultimately gave the team the confidence to implement the change. In 2021, Solidity introduced changes to how memory is managed. Instead of always starting at 0x80, it can now reserve slots for local variables. However, this change breaks a core invariant in Solidity, and we've to check if any parts of the code generator will be affected by this change. Particularly, is it possible that a portion of the codegen can read or write from this location as part of a subroutine? You can manually inspect the code to examine this, but you'd never be able to build confidence this way. Reasoning about semantics when multiple subroutines dealing with memory interact is very challenging. One of the tricks I found was encoding this problem as a set of mathematical constraints and sending it to a math solver for solution. This idea works in theory, but usually, such ideas fail in practice because constraint solvers quickly get to exponential complexity. However, I knew one or two things about building linear algebra solvers and this particular set of constraints were easy to solve without exponential blowup. In fact, I could probably teach you how to build it in less than an hour, it was dead simple. The final work was the following. 1. Build a transpiler that transpiles programs to these linear constraints (here, I implemented it as an optimizer step) 2. Send off the constraints to a solver. I used Z3 for simplicity, but it could've been built one from scratch. 3. Solve this constraint optimization problem and trigger if the constraints have a solution. This tells us there was a conflict with the new memory model. 4. Run this on a large corpus of test cases to build coverage. Solidity has a good corpus. It ultimately identified a bug where one of the memory management routines conflicted with the change, which was immediately fixed. More importantly, this work gave the team confidence that the memory management update was safe and effective. The reason I'm proud is that it required knowledge of a lot of different, distinct skills that I picked up by accident. Building compilers/transpilers, having a deep understanding of how these solvers work, and some magic 🪄