F* Is the Verified Code Already Hiding in Your Stack

F* hit the Hacker News front page again this week, and the recurring ritual says something interesting: every year or two, a few thousand developers discover a fifteen-year-old language and react like it launched yesterday. F* isn't new — Microsoft Research and Inria have been building it since 2011. What's genuinely newsworthy is quieter and more surprising: F* is probably the most widely deployed formal verification technology in existence, and almost nobody running its code knows it's there.

If you've opened Firefox, hashed a string in Python 3.12+, or sent packets through WireGuard, you've executed machine-checked code that started life as an F* proof. That deployment story — not the dependent types — is the reason this language deserves your attention.

The trick: verify here, ship there

F* made one architectural decision that separated it from decades of academic verification work: you don't run F*. You write and prove code in F*, then extract it to something your build system already understands — OCaml or F# for high-level code, C via the KaRaMeL compiler, or optimized assembly via Vale. The proofs stay behind; the artifact that ships is boring, portable C that a security auditor can read.

That's how HACL*, the verified crypto library built on F*, ended up everywhere. Mozilla started pulling HACL* primitives into NSS back in 2017, beginning with Curve25519, and Firefox still ships them. The Linux kernel, mbedTLS, and the ElectionGuard voting SDK all carry HACL*-derived code. Since Python 3.12, CPython's hashlib uses HACL*'s verified implementations for MD5, SHA-1, SHA-2, and SHA-3 whenever the linked OpenSSL doesn't provide them — so hashlib.sha3_256(b"hello") on a stock build may be running code with a machine-checked proof of memory safety and functional correctness behind it. Microsoft ships EverCrypt and EverParse, both Everest-project descendants of the same toolchain, inside Hyper-V and Windows networking.

The verified properties are worth spelling out because they're exactly the bug classes that keep producing crypto CVEs: no buffer overruns, no integer overflow surprises, functional correctness against an RFC-level spec, and secret-independent timing. You don't get "this code is perfect." You get "this code cannot have a Heartbleed."

Why F* escaped the lab

Rocq (né Coq), Isabelle, and Lean are all older or better known in academia, and none of them has anything close to this production footprint for systems code. Two decisions explain the gap.

First, automation. F* discharges most proof obligations by compiling them to queries for the Z3 SMT solver. Where a Rocq proof of array-bounds safety is something you write, an F* proof is usually something you don't — the solver grinds through the arithmetic. Refinement types like x:int{x > 0} get checked the way ordinary types do. Tactics exist for the hard cases, but the default mode is "annotate and let Z3 work," which puts the effort curve closer to writing very strict TypeScript than to doing interactive theorem proving. The honest caveat: when Z3 times out, you're suddenly debugging a solver's search heuristics, and proof brittleness across F* versions is a real maintenance cost that teams like Mozilla have simply accepted.

Second, verticals. The F* ecosystem never tried to verify your web app. It went after two domains where specs are small, stable, and brutally unforgiving: cryptographic primitives and parsers. That focus is the whole ballgame. A ChaCha20 spec fits on a page and hasn't changed since the RFC; a business rule changes every sprint. Lean conquered mathematics with mathlib, Rocq's flagship is the CompCert compiler, AWS used Dafny for its Encryption SDK — every verification success story picked a narrow domain with a frozen spec. F* just picked the one that ships in everyone's browser.

Pulse, hax, and the Rust convergence

The current release cycle shows where this is heading. F*'s v2026.04.17 release folded in Pulse, a separation-logic sublanguage (built on PulseCore, with clear Iris ancestry) for proving concurrent, mutable-state programs — the successor to the aging Low* embedding that HACL* was written in. Pulse code extracts to C or Rust.

Rust is the tell. The more interesting motion is Cryspen's hax toolchain, which runs the pipeline backwards: you write ordinary Rust, and hax translates it into F* for verification. That's how libcrux's ML-KEM implementation — the NIST-standardized post-quantum KEM from FIPS 203 — got verified for panic freedom, correctness, and secret independence. The verification effort helped surface KyberSlash, a real timing leak that hit multiple unverified Kyber implementations. As the industry rewrites its crypto stack for the post-quantum migration anyway, "verified from day one" is suddenly a live option rather than a retrofit, and Cryspen has been landing that code in NSS.

This is the right strategic read for the whole field: stop asking developers to move to a proof language, and instead verify the language they already chose. Verus is making the same bet natively for Rust. F*'s advantage is fifteen years of deployed evidence that the extraction model survives contact with real release engineering.

Should you care?

A clear-eyed verdict: F* is production-proven as a component factory and unproven as an application language, and the team seems to know it. Nobody should write a service in F*. But if you maintain code where a memory bug is a career event — crypto, parsers for hostile input, consensus-critical serialization — the adoption path is concrete: prove the component in F*/Pulse, extract C or Rust with KaRaMeL, vendor the generated code, and keep the proofs in CI. That's not hypothetical; it's what Mozilla, Microsoft, and CPython already do, and the generated C sits in their trees like any other dependency.

The costs are equally concrete: a hiring pool measured in the hundreds, SMT flakiness as a build-breaking failure mode, and specs that are only as good as your reading of the RFC. For the 95% of your codebase where bugs are cheap, none of this pays. For the 5% where they aren't, F* stopped being a research bet years ago — the evidence is already running on your machine.