What PKI Can Learn from Dependent Types

June 29, 2026

What PKI Can Learn from Dependent Types

If you’ve spent any time near a certificate authority, you know the ritual. You build a cert, you run it through zlint or certlint, you fix whatever the linter screams about, and you ship. The linter is treated as a load-bearing part of the pipeline. Nobody questions it. It’s just how PKI works now.

I want to argue that the linter is a symptom, not a cure. It exists because we encoded the rules of PKI in the wrong place, and dependent types show us where they should have gone.

The actual problem

A certificate is supposed to be a precise object. RFC 5280 tells you what an X.509 certificate is. The CA/Browser Forum Baseline Requirements layer more rules on top. RFC 6125 covers how identifiers in certs map to what you’re actually authenticating. There are rules about DNS name syntax, about which extensions are critical, about serial number entropy, about the exact shape of a SAN, about what’s allowed in a subject DN when a SAN is present.

Here’s the catch: all of those rules live in English. They live in prose, spread across documents, written by committees over decades, with “SHOULD” and “MAY” and “is RECOMMENDED” scattered through them like landmines. The validity of a certificate is a proposition, and we wrote that proposition in a natural language that no machine can check and no two engineers read the same way.

So what happens? Every CA re-implements its interpretation of the rules. Every browser re-implements its interpretation. Every TLS library, every linter, every validation path is a separate, partial, slightly-wrong translation of the same prose. The gaps between those translations are exactly where the bugs live, and the bugs are exploitable.

The classic examples are almost boring at this point. Null bytes in CN fields that one parser truncates and another doesn’t, so evil.com\0.good.com validates as good.com on the attacker’s side and evil.com on the CA’s. SAN parsing that disagrees on IA5String encoding. Name constraints that one stack enforces and another silently ignores. Every one of these is the same underlying failure: two pieces of code that were supposed to agree on what a valid certificate is, didn’t, because the definition was never written down in a form they could share.

Linting is a patch over a hole in the type system

The industry’s response to this has been linting. Take the prose, hand-translate it into a few thousand discrete checks, run those checks over the finished certificate, and reject the ones that fail. zlint alone has hundreds of lints. It works, sort of. It catches a lot.

But look at what linting actually is. It’s a separate program that re-derives, after the fact, whether a bytestring satisfies properties that the thing producing the bytestring should have guaranteed by construction. You build an object that has no idea whether it’s valid, then you ask a second object to grade it. That’s a strange architecture if you stop and look at it. We don’t validate that a u32 is in range after we construct it; the type makes the invalid states unrepresentable. We do exactly that for certificates because the type we use to represent a certificate is something like “a bag of bytes” or, if we’re lucky, “a struct with optional fields,” and that type permits millions of certificates that no RFC would ever bless.

The linter is a runtime check standing in for a property the type system should have enforced at construction time. It’s a patch over a hole. The hole is that “valid certificate” is not a type in any of our systems.

What dependent types let you say

This is the part where dependent types stop being an academic curiosity and start being the obvious tool.

In an ordinary type system, a type can’t depend on a value. Vec<u8> is Vec<u8> whether it has 3 elements or 300. You can’t write a type that means “a byte string that is a syntactically valid DNS name.” You can write a struct and a constructor that validates, but the validity isn’t in the type; it’s in your discipline about always going through the constructor, which the compiler can’t enforce against a hostile or careless caller.

In a dependently typed language (Idris, Agda, Lean, Coq, F*), a type can depend on a value, which means a type can encode an arbitrary proposition. You can write a type whose inhabitants are, by definition, only the valid DNS names. You can write a type ValidCertificate such that the only way to produce a value of that type is to also produce a proof that every relevant rule holds: the SAN is well-formed, the name constraints are satisfied, the critical extensions are the right ones, the serial has enough entropy, the subject DN doesn’t contradict the SAN, and so on.

The shift is this. Instead of:

  1. Build a certificate (any bytes will do).
  2. Run a linter to check whether it’s valid.
  3. Hope your linter agrees with everyone else’s.

you get:

  1. Build a certificate. If it isn’t valid, it doesn’t typecheck and you cannot build it.

The proposition “this is a valid certificate” stops being prose, stops being a linter ruleset, and becomes a type. You write the type once. Everyone who imports it gets the exact same definition of validity, checked by the compiler, with no room for two implementations to drift apart. The CA can’t issue a malformed cert because the function that issues certs only accepts a ValidCertificate, and the only way to get one is to satisfy the proof obligations.

The most useful property here is that a proof is portable in a way an implementation is not. F* and friends let you extract executable code from verified definitions, so the same specification that the CA uses to construct a cert is the one a relying party uses to check it. There’s a single source of truth that is simultaneously machine-checkable and executable. That’s the thing PKI has never had: one definition of “valid” that both sides provably share.

A concrete sketch

Pseudocode, Idris-flavored, to make it less abstract. A DNS label is between 1 and 63 octets and draws from a restricted alphabet. Today that rule lives in RFC 1035 prose and gets re-checked in a dozen places. As a type:

data ValidLabel : List Char -> Type where
  MkLabel : (cs : List Char)
         -> {auto nonEmpty : NonEmpty cs}
         -> {auto bounded  : length cs `LTE` 63}
         -> {auto alphabet : All IsLDHChar cs}
         -> ValidLabel cs

A value of ValidLabel cs cannot exist unless cs is non-empty, at most 63 characters, and made entirely of letters-digits-hyphens. There is no “construct it and check later.” The check is the construction. Stack these up through labels into names, names into SANs, SANs into the cert, and “valid certificate” becomes a type you cannot inhabit by accident.

You’ll notice the rules didn’t get simpler. RFC 1035 is still RFC 1035. What changed is that the rule is stated once, in a form the machine enforces, instead of stated in English and re-enforced by hand in every consumer.

The honest objections

I’m not going to pretend this is free, because the places where it’s hard are the interesting part.

Writing these specs is genuinely hard. Encoding the full Baseline Requirements as dependent types is a large, painful formalization effort, and the people who can do it well are rare. The X.509 grammar is ASN.1, which is its own swamp; proving things about DER encoding and canonicalization is real work. There’s a reason this hasn’t already happened, and it isn’t that nobody thought of it.

Adoption is the bigger wall. PKI is the most path-dependent corner of computing. OpenSSL is C. The installed base is enormous. You are not going to convince the ecosystem to rewrite its certificate handling in Lean. That’s not the realistic pitch.

The realistic pitch is narrower and, I think, more defensible. You formalize the spec once, in a dependently typed language, as the reference definition of validity. You extract a verified validator from it. Then the linters and the C libraries become things you can check against a machine-checkable ground truth, instead of against each other and against prose. The formal spec doesn’t have to replace the ecosystem to be valuable. It has to become the thing the ecosystem is measured against. Even partial formalization (just the name-parsing rules, just the SAN handling, just the parts with the worst exploit history) would close the highest-value gaps.

There’s prior art worth pointing at here. Project Everest and the verified TLS stack (miTLS, the HACL* crypto, the F* toolchain behind them) already showed that you can take a security protocol with a long history of implementation bugs and produce a formally verified implementation that ships in real browsers. The certificate validation layer is a natural next target and a smaller one than the full TLS state machine.

The point

Linting works around the fact that we never wrote down what a valid certificate is in a form a machine can enforce. We wrote it in English, re-implemented it everywhere, and now we run a separate grader to catch the inevitable disagreements. Dependent types let you write the definition once, as a type, and make invalid certificates unconstructible instead of merely detectable.

The industry’s instinct has been to add more lints. The better instinct is to ask why we need a grader at all, and to put the rules where the rules belong: in the type of the thing itself.