This is a genuine question.

I recently coauthored a cryptography paper which defines an encryption scheme called Kopis (really, a "key encapsulation mechanism", but that's not important for now). For theory papers, you usually just write the paper and that's it. For applied papers, you also write and benchmark some ugly code which, hopefully, nobody will ever look at. This paper, though, is a proposal for an encryption standard, which means it needs to be accompanied with very high quality code. It is not unbearably hard to write high quality code, in my experience, but it is hard to write high quality fast code, which is kind of the whole pitch of Kopis. Naturally, I turned to an LLM to make some improvements. It did the usual things, like inlining functions and reducing the number of variables on the stack, all things I could follow. But even with these optimizations, the code was 2–8x slower than the competing encryption schemes.

There were much more complicated optimizations on the table: number theoretic transforms, vectorized multiplication, multi-lane hashing, etc. The runtime savings would make this implementation exactly as fast as I was hoping, but I just did not trust myself to be able to review all that code. And given the fact that it's cryptography code, well, somebody's got to be responsible for it.

During an authors meeting somebody floated an idea: what if we could also include a formally verified implementation as part of the pitch in our paper? It would make the paper much stronger, and again put us on par with some of the existing encryption implementations. LLMs had only recently become good at writing Lean, so I thought this would be a great way of feeding two birds with one scone: improve the paper submission and also make sure that all the advanced optimizations did not affect correctness. So that's what I did.

Now, at the end of the process, I have a very pretty and succinct Lean implementation, a disgusting and extremely fast Rust implementation, a set of elegant human-readable theorems stating that the two implementations are equivalent, and tens of thousands of lines of Lean code proving those theorems. I also have scripts that check that all the code is constant-time (as much as that is a thing that can even be checked or achieved), as well as Github CI workflows to ensure that all the theorems hold after code changes.

Is this high-assurance cryptography, though? A prominent author of high-assurance cryptography defines it as follows:

High assurance software is usually seen as being more trustworthy than other software. This is especially interesting in high-risk/high-stakes environments such as financial institutions or governments.

The Rust code in my repo is the least effort cryptography code I have ever publicly put my name to. I haven't even read every line of it, let alone written every line. And at the same time, it is also the most thoroughly verified code I have ever put my name to. And it's not like I just slopped together all the tests and specs and harnesses and theorems. Those I actually put a lot of time and thought into.

In this blog post, I will describe my process for building kopis-rs with the aid of an LLM. I'll state my bias now: I think that some version of this process can produce high-assurance cryptography. I am curious whether this could be made more rigorous, and turned into a repeatable formula for producing high quality code.

Kopis is being standardized at C2SP. The Lean code, test vectors, and Rust implementations are all public as of this writing. In addition to kopis-rs, I'm releasing kopis-rs-smallcode, a Rust implementation which has almost no LLM-generated code (it still has the micro-optimizations that I included when I was personally reviewing all LLM outputs). It is extremely slow compared to kopis-rs, and has no formal verification, but hey the code size is smaller.

§ Introduction

Kopis is a post-quantum key encapsulation mechanism (KEM) intended for use in protocols which must obfuscate public keys and/or ciphertexts. This includes password-authenticated key exchange, obfuscated key exchange, oblivious transfer, anamorphic encryption, private set intersection, and steganography.¹ It is essentially a clone of Saber, the NIST PQC finalist. This means that its security story is pretty strong, and it is extremely close to ML-KEM in construction.

In the next sections, I will describe the process of carefully constructing the Rust implementation of Kopis. I tried my best at avoiding the traps of verification slop ("let's let Claude write the specs and the theorems and the proofs"), but I think there are parts that could use improvement. My hope is that people will read this and this procedure will eventually crystalize into a repeatable method for producing high-quality code. Some of this post will be a re-hashing of the appendix in the Kopis paper, and some of it will be some reflections thereon. If I had to give a TL;DR recommendation for writing code like this, it'd be:

1. Specify specify specify. Write out specs for everything you want to formalize, with your own hands, and make sure your specs are airtight.
2. Know your assumptions and theorems. "This crate is formally verified" is a meaningless sentence. What are your dependencies? Are you trusting them to satisfy some contract? Where'd you get that contract? What behavior are you promising about this crate? Why is this behavioral description it sufficient to fully constrain its behavior? The value of a formal proof hangs on these answers.
3. Consolidate the human-auditable parts. As a human auditor, you only need to keep track of definitions, theorems, and axioms. If you can put these in one place, you can be sure that they're not getting modified.
4. Make safeguards. There are things that cannot be proved yet. Some Rust intrinsics can't be extracted right now. Constant-timeness is not Lean-verifiable. So do your best to make sure to test these

Okay, let's start at the beginning.

§ Specifying Obsessively

Before we can implement anything, we have to make extremely sure that we know what we're building. Like, extremely sure.

§ Starting with Saber

Like I mentioned, Kopis is just a tweaked version of Saber. So it would make sense to start by specifying Saber and see if we run into any issues. Plus, I had a pretty solid Saber Rust crate from two years ago that I could use for testing. I picked Markdown for a specification format, since it seems everyone has a Markdown viewer, and LLMs seem to like it too.

I read the NIST PQC Round 3 Saber submission doc and started transcribing by hand. I took some creative liberties in fixing notation, but otherwise stayed pretty close to the PDF. I also made some changes where I already knew the Saber spec differed from the reference implementation.

Once I had a Markdown specification I was happy with, I iterated on it several times with an LLM. It did a great job at finding typos, inconsistencies from old versions, and, most importantly, ambiguities. Once I was satisfied with the specification, I decided it was time to test it. I asked the LLM to implement it in Python and produce some test vectors. For completeness, my prompt is below:²

Please read saber-spec.md and produce a pure Python implementation (no deps) which, when run, writes test vectors to claude-saber-kat.json (you can just do the Saber parameter set for now). The JSON file should contain one list of dicts. Each dict should contain fields sk, ct, ss, representing a KEM secret key, a KEM ciphertext, and the shared secret corresponding to that ciphertext. Each should be uppercase-hex-encoded. Please also write unit tests for the Python implementation so you can catch bugs as you go. Do not look at any other files in this repo (they will not help you). Any questions?

I'll note a caveat here, which I realized in hindsight. I did check that the LLM did not read any files (you can see this in the action logs in some clients). But this is not a good test of spec ambiguity. Saber is a well-known KEM. Any LLM would have certainly been trained on the Saber construction, as well as its C reference implementation. So this step was not nearly as conclusive as I thought it was at the time.

Anyways, I then had the LLM make a small test vector harness for my existing Saber Rust crate, and it passed. I concluded that the spec was solid, and so moved on to Kopis.

§ A Small Diff to Kopis

Confident in the spec, I started making the changes that turn Saber into Kopis. These were pretty minor, here is all of them: secret keys are 32-byte seeds, all hashes are TurboSHAKE instead of SHA3 and SHAKE, some XOF evals are now pointwise instead of one big squeeze, and the ciphertext is no longer hashed into the shared secret. Each one of these is a 1–5 lines diff in the pseudocode of the spec. So I made my specification edits, again going back and forth with the LLM. Quickly, I converged to something I was happy with.

§ Implementing Kopis

With the specifications obsessively reviewed, I was ready to start implementation.

Python. I had the LLM produce a Python implementation and known-answer test generator just like above (allowing xoflib as a dependency, since Python doesn't ship with TurboSHAKE). I'll be honest, I was feeling cocky about the Saber success so I only skimmed this implementation and did not read it carefully like the below ones. This didn't bite me later, but maybe that was chance. This makes me curious what the minimum amount of oversight necessary on these steps is, in order to rigorously guarantee results.

Rust. Then I asked the LLM to produce a minimal patch to the Saber crate to make it conform to the Kopis spec. The diff was +104/-128, which I found easy to review.

Lean. Finally we start working with Lean. I asked the LLM to produce a Lean implementation for Kopis. This required some dependencies. Fortunately Microsoft Research had just publicized their ML-KEM Lean implementation. This was perfect timing because I was able to steal some of their notation and their Keccak implementation, upon which the LLM built a TurboSHAKE implementation. The Lean implementation was just +209 lines, not including comments.

A note on the style of the Lean implementation. The first version of the implementation was not hard to review, but its code was not as one-to-one with the spec as it could have been. One thing I've been working on with a different Lean cryptographic specification project is seeing how closely I can mirror the actual specification in Lean code. Now, after some refactors, the current Kopis Lean spec is now extremely close to the Markdown.

Known-answer tests. At this point, I was able to start running some tests on the implementations to make sure that they all pass the Python-generated known-answer tests. So I asked the LLM to make a known-answer test harnesses for Rust and Lean, which came out to around +180 and +80 lines of Rust and Lean (without comments), respectively. After reviewing these diffs, I ran the tests and all passed.

§ Formal Verification

Finally, we are set up for the beets and potatoes of high-assurance cryptography: the proofs.

Proving components. I installed aeneas, the Rust-to-Lean extractor, and just went piecemeal through the feature of the crate, asking the LLM to prove equivalence to the Lean implementation. We did ring addition, then multiplication, then serialization, etc. At some point, I realized I could just tell it to finish the job, which it did. I did have to approve the axiomatization of our dependencies, namely the subtle crate (for constant-time equality checking) and the turboshake crate. Also I had to approve the axiomatization of some Rust intrinsics like wrapping_neg, since aeneas doesn't support them yet.

I'll note also that there were some small Rust code changes that were necessary for the proofs to work, because aeneas does not support the entire Rust language quite yet. So things like nested references had to be removed, and certain chained iterator constructions had to get turned into for-loops. These changes are not pretty, but they are few and far between, so I tolerated them. As aeneas improves, I expect these edits to go away.

Honing the theorems. The state of the theorems after "just prove everything" was not good. Obviously, the claims you can make about the code are only as strong as the theorems you have proved. So I needed to collect all the theorems into one place, make them as strong as possible, and make them readable. This took a lot of iteration with the LLM, but I ended up with a TopLevelTheorems.lean file that looked very nice, and contained 18 theorems, well really 9 unique ones, since each was duplicated for every security level.

Finally, to make sure there was no cheating, I had the LLM produce a TrustBase.lean file, which contains a list of all the expected axioms used in the Lean project, and throws an error if it finds any axioms in the project not in that list. This was about 25 lines of code and a list of ~30 axioms, all of which fell into the categories of Rust intrinsic or dependency.

§ Optimizations

The codebase was still extremely slow, and I could still not optimize for the life of me. But now I could use an LLM to do it, and use the Lean theorems to keep it honest.

I told the LLM to optimize the hell out of the crate. We took a few different paths, some less fruitful than others. What we landed on was using one of the number-theoretic transforms from a 2020 paper on optimizing Saber. Once the code was written, I asked the LLM to re-extract the Rust to Lean, and fix all the proofs. As long as the specification files, TopLevelProofs.lean, and TrustBase.lean didn't get modified, I could be sure that the optimizations were valid.

I found this to be really cool. If you make Lean your enforcer, you can have an LLM go nuts on your codebase, and it'll still come back with something provably equivalent (so long as it didn't touch your human-only files).

Structural versus behavioral theorems. In reality, TopLevelTheorems.lean did actually need some tweaking during the rounds of optimization. The problem was that the theorems assumed the internals of the Rust and Lean implementations were more or less identical. This stopped being true once the Rust data structures got fancier, e.g., storing cached NTT-domain versions of ring elements.

So, whereas before we had a theorem like "after keygen, the Lean specification's public key matches the Rust's PublicKey internal value", instead I had to define behavioral theorems, sticking to the structure of the API. In this case, we would replace the above theorem with two theorems: 1) "keygen followed by public key serialization produces the same bytestring in Lean and Rust", and 2) "keygen followed by encapsulation produces the same ciphertext and shared secret in Lean and Rust". Written out, these look like:

/-- keygen → pubkey → to_bytes matches the spec -/
theorem keygen_then_to_bytes : ∀ (s : Size) (sk : Array U8 32#usize),
    (do let ksk ← s.skFrom sk
        let kpk ← s.publicKey ksk
        s.toBytes kpk)
      ⦃ (r : Array U8 s.pkLen) =>
          (arrayToBytes r).toList = (Kopis.SkToPk s.ps (arrayToBytes sk)).toList ⦄
  | .k512, sk => Kopis.Properties.kopis512_keygen_to_bytes_spec sk
  | .k768, sk => Kopis.Properties.kopis768_keygen_to_bytes_spec sk
  | .k1024, sk => Kopis.Properties.kopis1024_keygen_to_bytes_spec sk

/-- keygen → pubkey → encapsulate matches the spec -/
theorem keygen_then_encapsulate : ∀ (s : Size) (sk randomness : Array U8 32#usize),
    (do let ksk ← s.skFrom sk
        let kpk ← s.publicKey ksk
        s.encap kpk randomness)
      ⦃ (ct : Array U8 s.ctLen) (ss : RustKopisSerial.kem.SharedSecret) =>
          let (spec_ss, spec_ct) := Kopis.KemEncap s.ps (arrayToBytes randomness)
                                      (Kopis.SkToPk s.ps (arrayToBytes sk))
          arrayToBytes ct = s.ctSize ▸ spec_ct ∧
          arrayToBytes ss = spec_ss ⦄
  | .k512, sk, randomness => Kopis.Properties.kopis512_keygen_encap_spec sk randomness
  | .k768, sk, randomness => Kopis.Properties.kopis768_keygen_encap_spec sk randomness
  | .k1024, sk, randomness => Kopis.Properties.kopis1024_keygen_encap_spec sk randomness

I modified all the theorem statements to just talk about the composition of the functions in the KEM API. You can see them here. You can also see the Lean spec here and the English spec here.

I'll also point out one neat thing about the theorems using Aeneas. The x ⦃ p ⦄ notation means that the operation x succeeded and its output has postcondition p. So all the theorems, as stated, also prove that the Rust implementation is panic-free, since the operation never fails.

Adding SIMD. To make vectorized backends, I followed the same process as the optimization loop.³ I asked the LLM to make AVX2 and NEON backends for the crate, and prove the theorems. There were some small annoyances, such as the fact that aeneas does not support unsafe SIMD intrinsics. The solution was to have the LLM create a formal Lean model for the couple dozen SIMD instructions we use in the implementation, axiomatize them, produce test vectors for those instructions in Rust, and make sure everything passes. This was pretty straightforward, but annoying and difficult to audit. It is very possible I skipped or misunderstood an instruction, or did not catch one of its edge cases. In the future, I would like aeneas to have a way for me to use these instructions with less fear. At the end of this process I had nearly 300 axioms, most of which are vector intrinsics.

The SIMD backends drastically improved performance on supported systems. I iterated on this further, and ended up with a small TurboSHAKE implementation in AVX2, since it can do 4-way parallel hashing really quickly. Also, though optimization, I had a different NTT for each of the three backends. I eventually realized that it was just as fast to make them all use the same NTT, which incidentally makes the code nicer too. Finally, I cleaned up the build script so that backend selection is easier to reason about, and easy to configure using environment variables.

§ Checking Constant-Timeness

One thing that Lean cannot prove is whether the Rust implementation has a timing side channel. This is problematic, because at this point, most of the Rust code was LLM-written.

There are two primary sources of non-constant-timeness: (1) an explicit branch over a secret value, and (2) use of a non-constant-time instruction, such as integer division. We can catch (1) using a tool like Valgrind with taint testing, and we can catch (2) by scanning compiled binaries for banned instructions. I asked the LLM to create harnesses for both of these. I was able to review the Valgrind solution pretty easily, since it's small and straightforward.

Scanning for non-CT instructions was way harder. I know to check for integer division, from BearSSL docs and KyberSlash, but I wasn't sure what else to check for. In the first iteration of the scanner, I used a denylist consisting of whatever instructions I and the LLM thought to include on the list. In later iterations for x86, I switched to an allowlist, based off of Intel's own list (called "DOIT") of constant-time instructions. This is a pretty small list, though, and ends up excluding lots of instructions. From a maintainer of AWS s2n-bignum:

... the official DOIT list is pretty conservative and excludes a few instructions where all our empirical evidence on recent uarchs suggests they are constant-time - notably BSR which is used critically in bignum_modinv and a few other places.

So there's reason to believe that DOIT is not exhaustive. LLVM outputs a few AVX2 instructions not on the DOIT list: the vector versions of DOIT instructions, legacy SSE-forms of vector DOIT instructions, floating point forms of DOIT integer fixed lane shuffles, and no-op instructions. A bunch of these do not appear to have any known non-constant-time behavior, are pretty hard to live without, and are generated by LLVM whether I want them or not. So I put them on an allowlist.⁴ I did a similar thing for AArch64 instructions.⁵ I think this is the right choice, but please correct me if I'm wrong.

§ Github CI

The finishing touch on the crate was to make sure that it was possible to see if you broke the proofs via Github CI. So I had the LLM create a CI pipeline that would do a Lean build for pull requests, caching as much as possible. A full build still takes 20+ minutes, but I don't mind too much. I'm kind of just amazed that this is possible.

§ Future Work

I've got formally-verified code, with theorems, specs, and axioms I understand, mechanized constant-time checking, and a CI pipeline. This is about as good as slop can be. Some questions I still have, and would be interested in seeing solutions for:

• Expanding past KEM. Key encapsulation is a really simple primitive. It would be interesting to see these techniques used for more complex primitives, and even for interactive protocols.
• Knowing which theorems to use. All of this is useless if top-level theorems are weak. I hope that the set of theorems I picked sufficiently constrain the implementation, but it's hard to know. It would be really neat if there were a formalization of which set of equivalence theorems needed to be proved in order to demonstrate that two KEMs are identical.
• What's the smallest number of things that need human review? It'd be good to figure out what you can and cannot get away with slopping out. For example, did it suffice to skim my Python reference impl as long as the test vectors passed in my early Rust implementation? A general procedure for cryptographic libraries would be nice.
• What should the canonical spec be? Now that I have an English spec and a Lean spec, which one is the source of truth? I think it should be Lean, but this feels pretty new. Should all cryptographic standards have a formally defined source of truth?

§ Plugs

A colleague and I are building a library for readable, human-audited, heavily tested Lean specifications of cryptographic primitives. It's pretty small right now, but it's growing. We would love to have submissions!