Informalizing Cryptographic Proofs

Marc Ilunga · Swiss Crypto Day · 4 September 2026

Randomness Expansion with CBC

CBC proof

(1.5 min)

Let me briefly go through the proof. How much time do I have? Only 5 minutes left, so I'll have to skim over it!

We want to establish the following distinguishing advantage.

Note the theta on both sides: it restricts the input space to values producing q blocks with CBC. And the filter [q] restricts the random function R to q queries.

First, given that theta, the [q] filter is unnecessary.

Next, define a game with a binary output that starts at 0 and becomes 1 if there is a non-trivial collision at the input of any call to R.

Conditioned on the game bit being zero, the two systems have the same behavior.

The conditional-equivalence lemma then lets us focus on bounding the advantage of winning the collision game blindly, that is, non-adaptively.

One can work out that this is at most the value shown.

Gluing everything together gives the intended result.

Correctness vs Presentation

Intuition	Complete correctness
Human-written paper	Formalization in a proof assistant
Can be slightly incorrect, usually readable	Machine-checked, mostly unreadable

Must we choose?

human intuition

checked certainty

configurable tradeoff

I have just done a bad job of explaining a proof, which I could blame on having only 10 minutes.

Regardless of the medium and of how much time one is given, there is an inherent tension between being thorough and conveying intuition.

On one hand, hand-written proofs present material at an abstraction level chosen by the author. At the risk of being ambiguous or slightly incorrect, they are well suited to conveying ideas and intuition.

On the other hand, formalizing in a proof assistant gives very strong guarantees but produces artifacts that are extremely difficult to read.

So I wanted to explore whether there is a configurable lever to get the best of both worlds.

CBC proof, bare

How it works

Adaptation of the Lean informalization1 by Patrick Massot and Kyle Miller.
Own formalization of Random Systems2 in Lean.
LLM-driven implementation, variable level of manual scrutiny.

checked sourceLean theoremproof termInfoTrees

proof treeevidence graphproof dependenciesgoals and contexts

semantic planentities and relationsapplied rulescanonical proof plan

renderingdiscourse and realizationExplanation JSONinteractive reader

language designRandom Systems ontology · grammar · presentation rules

1 Kyle Miller, From Lean to Natural Language and Back, ICERM 2025. https://kmill.github.io/informalization/icerm_talk.pdf

2 Ueli Maurer, Cryptography Foundations, lecture notes, ETH Zürich, Spring 2018.

Why do I care?

AI-generated maths and crypto
- Increasingly trustworthy thanks to formal verification
- Currently unsuitable for human consumers
- Informalization: enforce a presentation style decided by humans.

Consumers of cryptographic literature have different needs
- Advancing science, implementation considerations
- Informalization would let each reader pick their level of detail.

AI-generated math and cryptographic content is on the rise. AI's growing use of proof assistants makes these results more trustworthy, but at the cost of understanding.

I am positive about this trend but do not expect everyone to be. Nevertheless, there is a world where non-trivial results are produced and formalized by AI, and humans verify that the statement is meaningful without gaining insight from the proof. A human-defined way to render formalized results could be one of many approaches to staying deeply connected to a field we care about.

[click]

Besides AI, there are various consumers of cryptographic literature: some advancing science, others implementing. Each could benefit from a rendering at the level of detail they need.

Informal or Fully Correct? Why not both.

Random Systems in Lean: github.com/trailofbits/constructive-cryptography/RandomSystems
CBC-MAC proof: github.com/trailofbits/cbc-mac-cc
CBC-MAC informalization: github.com/trailofbits/constructive-cryptography/informalization
Informal Lean (Massot & Miller): kmill.github.io/informalization/ContinuousFrom.html
Get in touch: marc.ilunga@trailofbits.com