I feel this is going to be the thing which really boosts automated theory proving.

Up until now it's always been a hard sell, people say "Well, I can prove it myself, and that's less work than getting the computer to prove it", and they weren't completely wrong.

However, now we have LLMs which can do lots of interesting work, but really can't be trusted for anything important (like an LLVM optimisation pass, for example). If those LLMs can convince a theorem prover the LLVM optimisation pass is correct, then suddenly their output is much more useful.

This piece starts out super-duper inside baseball (optimizing DER encoding for, in the main, X.509 certificate handling) in Rust code that is increasingly leveraged by Python's cryptography stack. But it ends up somewhere crazy: with an LLM agent apparently one-shotting an LLVM optimization, then semiformally verifying the change, which is ultimately merged by the LLVM team.

having two very different code paths for measuring the length of the DER buffer and writing the DER sounds very scary. i guess its fine with Rust but the idea would give me the heebee-jeebies for any other language unless they are using a safe buffer implementation. i would find it hard to trust that there is no buffer overflow based on divergent behaviour between the two functions.

The most interesting part of this post is the bit about half way down, where Alex uses Claude to help identify a missing compiler optimization in LLVM... and then uses Claude Code to implement that optimization and gets a PR accepted to LLVM itself! https://github.com/llvm/llvm-project/pull/142869

> There’s only one encoding I choose to acknowledge, which is DER (the Distinguished Encoding Representation, it’s got a monocle and tophat).

I also prefer to use DER, because it is better than BER and CER. DER is actually a subset of BER but BER has some messiness which is avoided by DER; because there are not as any ways to encode data by DER this makes it simpler to handle.

DER is also the format used by X.509 certificates, so this is fortunate; however, I use DER for other stuff too (since I think it is generally better than XML, JSON, CSV, etc).

I wrote a library in C to serialize and deserialize DER.

The post title is misleading and the content reads more like a guerilla advertisement for claude. TL;DR: author works for Anthropic, and used claude to implement an optimization for LLVM.

So many encoding rules. DER, PER. It's an xkcd cartoon but inside one asn.1 standard!