This is a public draft. It's a draft in the sense that I haven't posted about it anywhere, and that I may make arbitrarily deep edits before I do. You're welcome to share it around with that caveat in mind.

The 2026 Rust Verification Workshop just wrapped up. I attended for the first time this year, as I (along with my zerocopy co-maintainer and others at Google) am working on a bit of outsider art. I come from a security background, and so while I've always admired formal verification at a distance, I've never considered myself a practitioner.

Something that's often hard to appreciate from outside of a field is the field's conception of its virtues. Why, for example, is it expected that jazz musicians will cover one another's songs and learn the standards, while a "cover" in Hip Hop would be completely verboten? One thing I hadn't realized before attending the workshop is the extent to which the academics who work on formal verification prize the ability to verify a project in situ without having to modify that project whatsoever to fit the needs of the verification process.

From what I can tell, this derives from the incentive structure of academic verification work. Academics have new techniques that they want to try out, but in order to do that, they need to demonstrate that those techniques are useful in the "real world" of industry. It's infeasible to rewrite an industrial software project from scratch in order to demonstrate this, and even if you did, it would be an apples-to-oranges comparison – you wouldn't have demonstrated that your technique is useful to actual practitioners. Instead, many verification projects demonstrate their value by approaching teams in industry and offering their services to verify a team's work post-hoc. The relationship is imbalanced: the engineers get what, to them, is a minor benefit (verification of properties they were relatively sure of to begin with, or uncovering bugs that they consider to be just the cost of doing business), while the academics rest their entire careers on the ability to prove that their work is useful to the engineers. As a consequence, the engineers have little incentive to change their practices to work around the requirements of verification. If the academics want to get their work published, they have to meet the engineers where they are.

This even shows up in their language: a term I hadn't heard much before the workshop is "proof engineer" a person, usually an academic, who takes more responsibility for the proof about the behavior of a codebase than for the codebase itself. A virtuous proof engineer is one who bothers the industry engineers as little as possible, with the occasional exception of notifying them when genuine bugs or opportunities for improvement are found.

The reason that I was so surprised by this realization is that I, as an industry practitioner, was expecting to be the one more concerned with pragmatism and "making it work in the real world". The "outsider art" I referred to above is a formal verification toolchain called Anneal, which lets you write and prove formal specifications of behavior in Lean, adding inline specification and proof annotations to your Rust code just like you do with safety doc and non-doc comments today. For example:

/// ```anneal
/// isValid self := self.val.val > 0
/// ```
pub struct PositiveUsize {
    val: usize,
}

Our goal with Anneal is pragmatic: to improve the developer velocity of teams of Rust engineers at Google and in the industry, and to improve the soundness, correctness, and performance of their code. Formality is useful only insofar as it serves that end.

To be fair, there were some forms of pragmatism that I was more concerned about. I have spent nearly all of my effort over the past few weeks working on infrastructural stability with the goal of making installing, using, and developing on Anneal as seamless as possible. I get the sense that that level of focus on infrastructure is uncommon in academia.

But when it came to the relationship between the tool and its users, I found myself more willing to make demands of my users than the academics I was talking to.

I was expressing my surprise about this dynamic to a friend, and his characterization has subtly shifted how I think about the work that we're doing, and how it relates to the field of formal verification. Paraphrasing:

The existing, academic approach to formal verification is closer to static analysis than to typing. It's something that you apply after the fact to an existing artifact, and it will tell you about properties that that artifact already has. By contrast, Anneal seems to think of its role as being part of the type system. Formal requirements are considered a first-class citizen of the API, and are evolved along with the API just like its documentation and type signature would be.

Seen in this light, it seems silly to apply formal verification post-hoc. It would be akin to writing an entire program in a dynamically typed language with the intention of only adding types once the program was complete.

This begs the question: Why hasn't formal verification already positioned itself in this way? Part of the answer, I think, is the incentive structure that I described above. But part of the answer is more foundational: If your tool is okay, it has to meet people where they are. If your tool is amazing, people will come to your tool.

Bluntly, I think that it's only just become possible for formal verification to be amazing. And I think it will change how we write software across the entire industry.

Consider Rust. A common refrain is that "it has a steep learning curve, but once you get over the hump, it will teach you to be a better programmer." Languages that are ahead of their time, or are overly academic, push people away by how much they demand. Rust, by contrast, was able to be good enough that people were willing to meet Rust's demands, and they found themselves better off for it. Far from pushing people away, Rust's overly-strict type system is now one of its main selling points.

At the surface, the comparison is simply that if formal verification is beneficial enough, people will tolerate its indiosyncricies. But the comparision is deeper, I think. You can think of Rust's opinionated, strict nature as being a form of truth claim: That the details which Rust encodes in its type system are a form of inherent rather than incidental complexity, and that being aware of them earlier leads to better design choices, and to better engineering overall.

In this light, Anneal is making a similar truth claim: That there are details beyond what Rust's type system can capture which are a form of inherent complexity, and that being aware of them earlier will lead to better design choices, and to better engineering overall.

On its own, this is not a new idea. I've been advocating for richer, more semantically-precise APIs for some time now, and I'm far from the only one.

What has changed is not that people are aware that this is a good idea. What has changed is what we can do about it.

For years, my zerocopy co-maintainer, Jack Wrenn, and I have been practicing this form of engineering. The only difference – but of course, it's the difference that makes all the difference – is that we've enforced it via self-discipline and norms rather than via tooling. We have absurd impls, functions with inscrutable bounds, the apex preditor of the turbofish food chain, and the safety (doc) comment to end all safety comments. The problem with this approach is that it's extremely labor-intensive. Consider this single PR which took three months to merge from its initial authorship. Reading its commit message, you can see why:

We generalize our existing support in util::macro_util, now relying on PMEs to detect when transmutes cannot be supported. In order to continue to support sized reference transmutation in a const context, we use the autoref specialization trick to fall back to our old (const-safe) implementation when both the source and destination type are Sized.

The main challenge in generalizing this support is making a trait implementation available conditional on a PME. We do this using the unsafe_with_size_eq! helper macro, which introduces #[repr(transparent)] wrapper types, Src and Dst. Internal to this macro, we implement SizeEq<Src<T>> for Dst<U>, with the implementation of SizeEq::cast_from_raw containing the PME logic for size equality. The macro's caller must promise to only use the Src and Dst types to wrap the T and U types for which this PME logic has been applied (or else the SizeEq impl could "leak" to types for which it is unsound).

In addition, we generalize our prior support for transmuting between unsized types. In particular, we previously used the SizeEq trait to denote that two types have equal sizes in the face of a cast operation (in particular, that *const T as *const U preserves referent size). In this commit, we add support for metadata fix-up, which means that we support casts for which *const T as *const U does not preserve referent size. Instead, we compute an affine function at compile time and apply it at runtime - computing the destination type's metadata as a function of the source metadata, dst_meta = A + src_meta * B. A and B are computed at compile time.

We generalize SizeEq to permit its cast_from_raw method to perform a runtime metadata fix-up operation.

A major reason that it took three months to land this PR is that it took us that long – working sporadically, of course – to convince ourselves that our "pointer metadata fix-up" implementation was sound. Here's the core implementation, safety comments included, in all its horrifying glory:

/// Implements [`<Dst as SizeEq<Src>>::cast_from_raw`][cast_from_raw].
///
/// # PME
///
/// Generates a post-monomorphization error if it is not possible to satisfy
/// the soundness conditions of [`SizeEq::cast_from_raw`][cast_from_raw]
/// for `Src` and `Dst`.
///
/// [cast_from_raw]: crate::pointer::SizeEq::cast_from_raw
//
// FIXME(#1817): Support Sized->Unsized and Unsized->Sized casts
pub(crate) fn cast_from_raw<Src, Dst>(src: PtrInner<'_, Src>) -> PtrInner<'_, Dst>
where
    Src: KnownLayout<PointerMetadata = usize> + ?Sized,
    Dst: KnownLayout<PointerMetadata = usize> + ?Sized,
{
    // At compile time (specifically, post-monomorphization time), we need
    // to compute two things:
    // - Whether, given *any* `*Src`, it is possible to construct a `*Dst`
    //   which addresses the same number of bytes (ie, whether, for any
    //   `Src` pointer metadata, there exists `Dst` pointer metadata that
    //   addresses the same number of bytes)
    // - If this is possible, any information necessary to perform the
    //   `Src`->`Dst` metadata conversion at runtime.
    //
    // Assume that `Src` and `Dst` are slice DSTs, and define:
    // - `S_OFF = Src::LAYOUT.size_info.offset`
    // - `S_ELEM = Src::LAYOUT.size_info.elem_size`
    // - `D_OFF = Dst::LAYOUT.size_info.offset`
    // - `D_ELEM = Dst::LAYOUT.size_info.elem_size`
    //
    // We are trying to solve the following equation:
    //
    //   D_OFF + d_meta * D_ELEM = S_OFF + s_meta * S_ELEM
    //
    // At runtime, we will be attempting to compute `d_meta`, given `s_meta`
    // (a runtime value) and all other parameters (which are compile-time
    // values). We can solve like so:
    //
    //   D_OFF + d_meta * D_ELEM = S_OFF + s_meta * S_ELEM
    //
    //   d_meta * D_ELEM = S_OFF - D_OFF + s_meta * S_ELEM
    //
    //   d_meta = (S_OFF - D_OFF + s_meta * S_ELEM)/D_ELEM
    //
    // Since `d_meta` will be a `usize`, we need the right-hand side to be
    // an integer, and this needs to hold for *any* value of `s_meta` (in
    // order for our conversion to be infallible - ie, to not have to reject
    // certain values of `s_meta` at runtime). This means that:
    // - `s_meta * S_ELEM` must be a multiple of `D_ELEM`
    // - Since this must hold for any value of `s_meta`, `S_ELEM` must be a
    //   multiple of `D_ELEM`
    // - `S_OFF - D_OFF` must be a multiple of `D_ELEM`
    //
    // Thus, let `OFFSET_DELTA_ELEMS = (S_OFF - D_OFF)/D_ELEM` and
    // `ELEM_MULTIPLE = S_ELEM/D_ELEM`. We can rewrite the above expression
    // as:
    //
    //   d_meta = (S_OFF - D_OFF + s_meta * S_ELEM)/D_ELEM
    //
    //   d_meta = OFFSET_DELTA_ELEMS + s_meta * ELEM_MULTIPLE
    //
    // Thus, we just need to compute the following and confirm that they
    // have integer solutions in order to both a) determine whether
    // infallible `Src` -> `Dst` casts are possible and, b) pre-compute the
    // parameters necessary to perform those casts at runtime. These
    // parameters are encapsulated in `CastParams`, which acts as a witness
    // that such infallible casts are possible.

    /// The parameters required in order to perform a pointer cast from
    /// `Src` to `Dst` as described above.
    ///
    /// These are a compile-time function of the layouts of `Src` and `Dst`.
    ///
    /// # Safety
    ///
    /// `offset_delta_elems` and `elem_multiple` must be valid as described
    /// above.
    ///
    /// `Src`'s alignment must not be smaller than `Dst`'s alignment.
    #[derive(Copy, Clone)]
    struct CastParams {
        offset_delta_elems: usize,
        elem_multiple: usize,
    }

    impl CastParams {
        const fn try_compute(src: &DstLayout, dst: &DstLayout) -> Option<CastParams> {
            if src.align.get() < dst.align.get() {
                return None;
            }

            let (src, dst) = if let (SizeInfo::SliceDst(src), SizeInfo::SliceDst(dst)) =
                (src.size_info, dst.size_info)
            {
                (src, dst)
            } else {
                return None;
            };

            let offset_delta = if let Some(od) = src.offset.checked_sub(dst.offset) {
                od
            } else {
                return None;
            };

            let dst_elem_size = if let Some(e) = NonZeroUsize::new(dst.elem_size) {
                e
            } else {
                return None;
            };

            // PANICS: `dst_elem_size: NonZeroUsize`, so this won't div by zero.
            #[allow(clippy::arithmetic_side_effects)]
            let delta_mod_other_elem = offset_delta % dst_elem_size.get();

            // PANICS: `dst_elem_size: NonZeroUsize`, so this won't div by zero.
            #[allow(clippy::arithmetic_side_effects)]
            let elem_remainder = src.elem_size % dst_elem_size.get();

            if delta_mod_other_elem != 0 || src.elem_size < dst.elem_size || elem_remainder != 0
            {
                return None;
            }

            // PANICS: `dst_elem_size: NonZeroUsize`, so this won't div by zero.
            #[allow(clippy::arithmetic_side_effects)]
            let offset_delta_elems = offset_delta / dst_elem_size.get();

            // PANICS: `dst_elem_size: NonZeroUsize`, so this won't div by zero.
            #[allow(clippy::arithmetic_side_effects)]
            let elem_multiple = src.elem_size / dst_elem_size.get();

            // SAFETY: We checked above that `src.align >= dst.align`.
            Some(CastParams {
                // SAFETY: We checked above that this is an exact ratio.
                offset_delta_elems,
                // SAFETY: We checked above that this is an exact ratio.
                elem_multiple,
            })
        }

        /// # Safety
        ///
        /// `src_meta` describes a `Src` whose size is no larger than
        /// `isize::MAX`.
        ///
        /// The returned metadata describes a `Dst` of the same size as the
        /// original `Src`.
        unsafe fn cast_metadata(self, src_meta: usize) -> usize {
            #[allow(unused)]
            use crate::util::polyfills::*;

            // SAFETY: `self` is a witness that the following equation
            // holds:
            //
            //   D_OFF + d_meta * D_ELEM = S_OFF + s_meta * S_ELEM
            //
            // Since the caller promises that `src_meta` is valid `Src`
            // metadata, this math will not overflow, and the returned value
            // will describe a `Dst` of the same size.
            #[allow(unstable_name_collisions)]
            unsafe {
                self.offset_delta_elems
                    .unchecked_add(src_meta.unchecked_mul(self.elem_multiple))
            }
        }
    }

    trait Params<Src: ?Sized> {
        const CAST_PARAMS: CastParams;
    }

    impl<Src, Dst> Params<Src> for Dst
    where
        Src: KnownLayout + ?Sized,
        Dst: KnownLayout<PointerMetadata = usize> + ?Sized,
    {
        const CAST_PARAMS: CastParams =
            match CastParams::try_compute(&Src::LAYOUT, &Dst::LAYOUT) {
                Some(params) => params,
                None => const_panic!(
                    "cannot `transmute_ref!` or `transmute_mut!` between incompatible types"
                ),
            };
    }

    let src_meta = <Src as KnownLayout>::pointer_to_metadata(src.as_non_null().as_ptr());
    let params = <Dst as Params<Src>>::CAST_PARAMS;

    // SAFETY: `src: PtrInner`, and so by invariant on `PtrInner`, `src`'s
    // referent is no larger than `isize::MAX`.
    let dst_meta = unsafe { params.cast_metadata(src_meta) };

    let dst = <Dst as KnownLayout>::raw_from_ptr_len(src.as_non_null().cast(), dst_meta);

    // SAFETY: By post-condition on `params.cast_metadata`, `dst` addresses
    // the same number of bytes as `src`. Since `src: PtrInner`, `src` has
    // provenance for its entire referent, which lives inside of a single
    // allocation. Since `dst` has the same address as `src` and was
    // constructed using provenance-preserving operations, it addresses a
    // subset of those bytes, and has provenance for those bytes.
    unsafe { PtrInner::new(dst) }
}

That safety comment is the reason that Anneal exists today. Not only did it take us three months to land this change, but a subsequent generalization (to support "shrinking transmutes", in which the pointer metadata fix-up operation is permitted to shrink rather than preserve the size of the referent) has been in review since June of last year. Every time Jack and I sit down to take another stab at reviewing the proof, we can't quite convince ourselves that it's sound.

Hopefully you can appreciate why "write your safety comments in Lean" is such an exciting idea to us.

The promise of Anneal is twofold:

1. Encode all of the inherent complexity in your types, just as Jack and I have been doing in zerocopy for years
2. Use tooling to make sure you get it right

As I said above, that second point is the difference that makes all the difference. Tooling which enforces corrrectness is what separates a C codebase from a Rust one. At the risk of committing a faux pas by quoting myself, "everything [you can do in Rust] can be done and is done in C and C++. The only difference there is that it's very unsafe, and you, the programmer, have to verify a lot of properties yourself." I choose to commit that faux pas to point out that we, as a community, have been singing Rust's praises for this reason for many years.

I said above:

What has changed is not that people are aware that this is a good idea. What has changed is what we can do about it.

What, exactly, has changed? Two things: Lean and AI.