Introduction

Vest generates secure, performant parsers and serializers for binary data formats, formally verified in Verus. It provides a concise format DSL for non-experts, as well as a combinator library for experts who want to build formats directly in Verus.

Given a high-level format description, Vest automatically emits efficient, idiomatic Rust that is memory-safe, arithmetically safe, panic-free, and terminating on any input. More importantly, Vest parsers and serializers are proven to satisfy a suite of desirable security properties, making them immune to entire classes of attacks that have historically plagued unverified, hand-written code.

With Vest, we have built the first production-grade formally verified ASN.1 library (supporting both DER and BER, which we leverage to implement the first verified CMS codec), and a verified prototype for both general and deterministic CBOR.

Who this is for

Vest is for anyone who needs to parse or serialize binary data formats, especially when correctness and security are critical. This includes: network security protocols such as TLS and IKE, which parse handshake messages and serialize authenticated responses; cryptographic message formats such as X.509 and CMS, which encode certificates, signed objects, keys, and algorithm parameters; executable and secure-update formats carrying code alongside authenticated metadata; and RPC and distributed-systems frameworks, which marshal typed application objects onto wire formats such as Protocol Buffers.

Vest is still a research tool. It does not cover every format in the wild, and its current features and limitations are documented.

As of now, this book covers the nitty-gritty of the DSL and the ASN.1 compiler. We are working on a guide to the underlying combinator library, as well as a more complete support for CBOR.

Choose your path

The project repository holds the source code for the combinator library, the DSL compiler, the ASN.1 library and frontend, and the CBOR codec.

Getting started

In this tutorial, we’ll use Vest to build a parser and a serializer for a small binary message format. Along the way, we’ll see the typical workflow for using Vest:

• describing a binary format in the Vest DSL,
• compiling the DSL format to Rust,
• parsing raw bytes into Rust values,
• serializing Rust values into bytes,
• and (for verified clients) checking and using the proofs that come with the generated code.

We assume the reader has some basic familiarity with Rust, but no prior knowledge of Verus, the program verifier used by Vest.

What we’re building

Many data formats encode messages as tag-length-value (TLV) structures. In a TLV, a tag says what kind of message follows, a length says how many bytes it takes, and the rest of the message is interpreted according to the tag. Our format follows this pattern: it’s a tiny protocol that a sensor might use to report to a server. Every message starts with a fixed three-byte header followed by a variable-length body:

 byte 0     bytes 1-2          the next `len` bytes
+--------+------------------+--------------------------+
|  tag   |       len        |         content          |
+--------+------------------+--------------------------+
  1 byte   16-bit integer,     interpreted according
           little-endian            to the tag

There are three kinds of messages:

Note that there are two implicit dependencies/constraints concealed in the above informal format description. First, the content’s structure depends on the tag: a Hello message has a different layout than a Reading or a Log. Second, the content’s byte length must agree with len exactly: a Reading, for example, always has len = 7 (1 + 2 + 4 bytes).

A hand-written parser for this seemingly simple format can easily go wrong. It might forget to check len against the input it actually received, let a message body read past its declared length, or silently accept a tag it doesn’t know. A hand-written serializer can also easily write a len that doesn’t match the content. We’ll see how Vest takes care of each of these for us.

Setting up

Install the compiler

You’ll need a stable Rust toolchain with cargo and rustc on your PATH. Install the Vest DSL compiler from crates.io:

cargo install vest

This puts vest on your PATH. You can run vest --version to check that it worked.

Create a project

Next, let’s create a new Rust project and add Verus and Vest as dependencies:

cargo new msg-demo
cd msg-demo
cargo add vest_lib
cargo add vstd@=0.0.0-2026-10-04-0306 --no-default-features

Your Cargo.toml should now contain something like this:

[dependencies]
vest_lib = "0.2"
vstd = { version = "=0.0.0-2026-10-04-0306", default-features = false }

vest_lib and vstd: vest_lib is Vest’s combinator library underlying the generated code. It provides the parser and serializer building blocks, together with their specifications and proofs. vstd is the Verus standard library that vest_lib depends on.

To avoid subtle version mismatch issues, it’s advised to use the exact version shown above: Verus and vstd move quickly, and each Vest release tracks one release of Verus. We’ll keep this page up to date as new versions come out.

vest_lib supports no_std (core-only and alloc), so you can use it in embedded or kernel code. See Feature configurations.

Writing your first format

Vest formats live in .vest files. We’ll write msg.vest in the project’s root directory, building it one piece at a time.

The tag: an enum

Let’s start with the tag:

msg_type = enum {
  Hello = 1,
  Reading = 2,
  Log = 3,
}

Every format definition has the shape name = format. Here, msg_type is an enum: a named set of variants, each with a numeric value. The values are the bytes that appear on the wire. Vest picks the smallest unsigned integer type that holds every value, so this tag takes exactly one byte. To force a specific integer type, use integer literals with type suffixes like 1u8 or 2u16 for the variants.

This enum is closed: the generated parser rejects every other byte value, such as 4, as an invalid tag. If your protocol needs to keep unknown tags around instead, add ... after the variants to make the enum open.

The content: three structs

Now let’s describe the three kinds of content from the table above:

hello = {
    version: u8,
    mac: [u8; 6],
}
reading = {
    sensor: u8,
    value: u16,
    timestamp: u32,
}
log = {
    level: u8,
    text: Tail,
}

Each definition describes a struct: named fields laid out back to back on the wire, with no padding in between. We’ve used three kinds of building blocks:

• u8, u16, and u32 are unsigned integers of 1, 2, and 4 bytes.
• [u8; 6] is exactly six raw bytes: here, a MAC address.
• Tail means “whatever is left.” In log, the text field takes all the bytes that remain after level.

The message: putting it together

Finally, the message itself:

msg = {
  @tag: msg_type,
  @len: u16,
  content: [u8; @len] >>= choose(@tag) {
    Hello => hello,
    Reading => reading,
    Log => log,
  },
}

Let’s decode it line by line:

• @tag: msg_type specifies the tag with the enum format we defined earlier. The @ marks tag as a dependency, which means that later fields can refer to its value as @tag. It’s otherwise the same as an ordinary field: it’s on the wire, and it will be part of the Rust value type that gets generated.
• @len: u16 specifies the 16-bit length as an unsigned integer, which is also a dependency.
• [u8; @len] carves out exactly len bytes of input for the content.
• >>=, read as “and then,” parses those bytes (and only those bytes) in [u8; @len], with the format on its right-hand side. We’ll see its role in serialization later.
• choose(@tag) { ... } picks that format based on the tag: a Hello tag selects the hello format, and so on.

The >>= operator is important: it “separates” the content from the rest of the input. The content format only ever sees the len bytes carved out for it, so it can’t read past the end of its message. It also has to use all of them: leftover bytes are a parsing error.

Byte order

Our protocol spec said that len is little-endian. That’s Vest’s default, so we don’t need to write anything. For a big-endian protocol, put !BIG_ENDIAN at the top of the file; it applies to every definition in the file. See Byte order for details.

The complete file

msg_type = enum {
  Hello = 1,
  Reading = 2,
  Log = 3,
}

hello = {
    version: u8,
    mac: [u8; 6],
}
reading = {
    sensor: u8,
    value: u16,
    timestamp: u32,
}
log = {
    level: u8,
    text: Tail,
}

msg = {
  @tag: msg_type,
  @len: u16,
  content: [u8; @len] >>= choose(@tag) {
    Hello => hello,
    Reading => reading,
    Log => log,
  },
}

Generating Rust

Now let’s compile the format to a Rust module and save it in src/msg.rs.

$ vest msg.vest -o src/msg.rs
📜 Parsing the vest file...
🔨 Elaborating the AST...
🔍 Type checking...
📝 Generating the verus file...
👏 Done!

The generated module is a normal Rust file. To use it, declare it at the top of src/main.rs:

mod msg;

Tip: Instead of rerunning the compiler by hand whenever the format changes, you can call it from build.rs to keep the generated code up to date automatically.

What got generated?

If you open src/msg.rs, you’ll find that it’s quite long (but hopefully still readable!). That’s because it contains specifications and proofs as well as executable code. The parts you’ll interact with are a Rust value type for each definition, plus a format type that does the parsing and serializing:

pub enum MsgType { Hello = 1, Reading = 2, Log = 3 }

pub struct Hello<'i> { pub version: u8, pub mac: &'i [u8] }
pub struct Reading   { pub sensor: u8, pub value: u16, pub timestamp: u32 }
pub struct Log<'i>   { pub level: u8, pub text: &'i [u8] }

pub enum MsgContent<'i> { Hello(Hello<'i>), Reading(Reading), Log(Log<'i>) }

pub struct Msg<'i> {
    pub tag: MsgType,
    pub len: u16,
    pub content: MsgContent<'i>,
}

// carries the executable parser, serializer, as well as the specs and proofs for the `msg` format
pub struct MsgFmt;

// ... specifications, proofs, and the implementations of the APIs

There’s a few things to note:

• Names follow Rust conventions: msg_type becomes MsgType, and msg becomes Msg.
• Byte fields such as mac: [u8; 6] and text: Tail become &'i [u8] (byte slices) that borrow from the input buffer, so parsing them is zero-copy.
• Integer fields such as value: u16 and timestamp: u32 become native Rust integers, so parsing them would perform “small” copies. Vest does this because
  1. integers might be mis-aligned in wire and attempting to read them directly would be unsafe, and
  2. integer types are small and cheap enough to copy (size_of::<u16>() is 2 bytes, while size_of::<&u16>() is 8 or 4 bytes)
• The choose becomes a Rust enum, MsgContent, named after the struct and the field it appears in. Each variant holds one of our content structs.
• Each named definition gets its own format type, such as ReadingFmt. This is a zero-sized type that implements certain traits to provide the parser, serializer, as well as the specifications and proofs for that format. In this tutorial, we’ll only need MsgFmt, which handles the whole message.

The Construct-to-Rust mapping shows how every DSL construct corresponds to a Rust type.

Parsing a message

Now it’s time to parse some bytes! Replace the contents of src/main.rs with this program:

mod msg;

use msg::*;
use vest_lib::core::exec::Parser;

fn main() {
    let wire: &[u8] = &[
        0x02,                   // tag       = 2 (Reading)
        0x07, 0x00,             // len       = 7
        0x03,                   // sensor    = 3
        0x66, 0x08,             // value     = 2150 (0x0866)
        0x00, 0xF1, 0x53, 0x65, // timestamp = 1700000000 (0x6553F100)
    ];

    let (consumed, msg) = MsgFmt.parse(&wire).unwrap();
    println!("consumed {consumed} bytes: {msg:?}");
}

Notice the byte order: because integers are little-endian, value = 0x0866 is stored as 66 08, with the least significant byte first.

Run it with cargo run, and you should see:

consumed 10 bytes: Msg { tag: Reading, len: 7, content: Reading(Reading { sensor: 3, value: 2150, timestamp: 1700000000 }) }

parse returns a pair when it succeeds: how many bytes it consumed, and the parsed value. In general, Vest doesn’t require full consumption of the input. If you’re reading messages from a stream, the count tells you where the next message begins.

The parsed value is an ordinary Rust value, so you can inspect it however you like:

assert_eq!(consumed, 10);
assert_eq!(msg.tag, MsgType::Reading);
assert_eq!(msg.len, 7);
assert_eq!(msg.content, MsgContent::Reading(Reading { sensor: 3, value: 2150, timestamp: 1700000000 }));

Try breaking the parser

Let’s poke at the parser with some bad input. We’ll make a mutable copy of the message, change it, and parse it again:

let mut bad = wire.to_vec();
bad[0] = 0x04; // not a valid tag
println!("{:?}", MsgFmt.parse(&bad.as_slice()));

Here’s what happens for this change and a few others:

Every malformed input produced an error that the caller can handle. In fact, no input can make the parser panic, read out of bounds, or loop forever: these are among the properties Vest proves.

Serializing a message

In Vest, serializing a value according to a binary format normally takes two steps:

1. prepare checks that the value is fully compliant with the format and computes how many bytes it will take on the wire.
2. serialize writes the value into a buffer of exactly that size.

Let’s first bring the relevant traits into scope:

use vest_lib::core::exec::{Parser, Prepare, SerializerExt};

Then serialize the message we just parsed:

let len = MsgFmt.prepare(&msg).unwrap(); // might fail if the value is inconsistent with the format or the length is too large
let mut output = vec![0u8; len];
MsgFmt.serialize(&msg, &mut output);
assert_eq!(output, wire);

We get back exactly the bytes we started with.

Why does Vest separate preparation from serialization? There are several key benefits:

1. Infallible serialization: It allows the caller to check for potential errors (such as a value that doesn’t satisfy the format’s constraints or integer overflows) before allocating a buffer. A fallible serialization would instead perform the checks while writing to the buffer, which could lead to partial writes and more complex error handling.
2. Zero-reallocation: It allows the caller to pre-allocate a buffer of the (provably) correct size, which can be more efficient than growing a buffer during serialization.

Always call prepare first. Because serialize is designed to be infallible, it doesn’t recheck the value or the buffer size; it relies on what prepare has already established. In ordinary Rust, nothing enforces this. If you skip prepare, the output is not guaranteed to match the format, and an undersized buffer may cause undefined behavior. In verified code, Verus prevents you from calling serialize without first establishing those proof obligations.

Building a message from scratch

Apart from parsed values, we can also build the same message by hand and serialize it:

let fresh = Msg {
    tag: MsgType::Reading,
    len: 7, // sensor + value + timestamp = 1 + 2 + 4 bytes
    content: MsgContent::Reading(Reading { sensor: 3, value: 2150, timestamp: 1700000000 }),
};

let len = MsgFmt.prepare(&fresh).unwrap();
assert_eq!(len, 10); // 3 header bytes + 7 content bytes

let mut output = vec![0u8; len];
MsgFmt.serialize(&fresh, &mut output);
assert_eq!(output, wire); // the same bytes we parsed earlier

When prepare fails

What if a value breaks the format’s constraints?

let wrong_len = Msg { len: 99, ..fresh };
println!("{:?}", MsgFmt.prepare(&wrong_len));

prepare refuses:

Err(PreSerializeError { kind: NotCompliant(LengthInconsistent), failed_format: None })

A tag that doesn’t match the content is rejected too:

let wrong_tag = Msg { tag: MsgType::Log, ..fresh }; // the content is a Reading
println!("{:?}", MsgFmt.prepare(&wrong_tag));

Err(PreSerializeError { kind: NotCompliant(InvalidTag), failed_format: Some("msg_content") })

Here, format dependencies work in the opposite direction. When parsing, @tag and @len decide how to read the content. When serializing, they are constraints that the value has to satisfy, and prepare is where Vest checks them. Without that check, you could send a header that misdescribes its content, and the receiver would misread the message.

Checking the proofs (recommended)

So far, we’ve used src/msg.rs as ordinary Rust. The file also contains specifications of what the parser and serializer should do, together with proofs that they are functionally correct and secure with respect to the specification.

Technically, you don’t need Verus to use Vest. If you’re working in unverified Rust and just want to parse and serialize more safely, you can stop here. Still, we highly recommend checking the proofs with Verus. That way, you don’t have to trust the Vest DSL compiler: Verus confirms that the generated code really satisfies the promised properties.

Each Vest release works with one exact Verus release, recorded in verus.json. Follow the Verus installation instructions for that version, or let a script from the Vest repository install it for you:

git clone https://github.com/secure-foundations/vest.git
./vest/scripts/install-verus.sh
export PATH="$PWD/vest/.verus:$PATH"

Next, add this section to your crate’s Cargo.toml so that cargo verus knows to verify it:

[package.metadata.verus]
verify = true

Then, from your project directory, run:

cargo verus verify

Verus checks in order vstd, vest_lib, and then your crate, which can take a minute or two. Each one prints a line like this:

verification results:: 121 verified, 0 errors

When you see 0 verification errors, all of the proofs in the generated module have been checked, and congrats that Vest’s guarantees hold for your format and its generated parser and serializer.

Using Vest from verified Rust

So far, we’ve called the generated code from ordinary Rust. If your application is also verified with Verus, it can go one step further and use Vest’s theorems in its own proofs. Real applications can be more complex, but here’s a small example: a function that proves that parsing a serialized value gives back the original value.

use crate::msg::*; // Vest-generated module
use vest_lib::prelude::*; // Bring the `vest_lib` specification and proof traits into scope

verus! {

fn roundtrip(value: &Msg<'_>) -> Result<(), PreSerializeError> {
    let len = MsgFmt.prepare(value)?;
    let mut output = vec![0u8; len];
    MsgFmt.serialize(value, &mut output);

    proof {
        MsgFmt.theorem_serialize_parse_roundtrip(value.deep_view()); // invoke Vest-provided theorem in Verus's proof block
    }
    let (consumed, parsed) = MsgFmt.parse(&output.as_slice()).unwrap();
    assert(consumed == len); // Verus assertion
    assert(parsed.deep_view() == value.deep_view());
    Ok(())
}

} // verus!

Let’s walk through it:

1. prepare checks that the value is consistent with the format and tells us exactly how much space to allocate for the serialized output, just like before.
2. serialize fills that space with the value’s binary encoding. Here, Verus verifies that the value is consistent and the buffer has exactly the required size (because we just called prepare).
3. The proof block calls Vest’s roundtrip theorem. It tells Verus that parsing output (the serialized value) succeeds, consumes all len bytes, and returns the same logical contents. That’s enough for Verus to prove both asserts, and to prove that the unwrap can never panic.

Note that the proof block and the Verus assert(...) statements are checked at compile time and add no work at run time. Use Rust’s assert!(...) if you also want a check at run time.

In the above example, we used Vest’s theorem to reason about the values abstractly/symbolically. To prove more subtle facts about particular fields, or to work out concrete serialized lengths, see Reasoning about generated values.

Summary

Congratulations, you’ve built and verified your first Vest format! Along the way, you’ve seen how to:

• describe a binary format with enums, structs, dependencies (@), bounded regions ([u8; @len] >>= ...), and choices (choose);
• compile it with vest and use the generated types from Rust;
• parse with parse, which returns the parsed value and how many bytes it consumed when successful, or an error when it fails;
• serialize with prepare followed by serialize, and in particular, how prepare efficiently checks that the value is consistent with the format and computes the exact number of bytes needed for serialization;
• check the generated proofs with cargo verus verify, and use Vest’s theorems in your own verified code.

Where next

• What Vest proves: Vest’s formal guarantees in detail.
• Language reference: every format construct in the Vest DSL, and the current limitations.
• Generated Rust Code: the full shape of what comes out of the DSL compiler, including more of the generated API and reasoning about values in Verus proofs.
• ASN.1 compiler: generate DER or BER codecs from an ASN.1 module instead of writing a .vest file.

What Vest proves

Binary parsers and serializers are a classic source of security vulnerabilities, due to the conflicting goals of high performance and adherence to complex binary formats. The most common implementation mistakes are:

• Memory safety issues, such as use-after-free, double-free, and out-of-bounds accesses
• Arithmetic issues, such as integer overflow and underflow
• Improper Input Validation
• Deserialization of Untrusted Data
• Uncontrolled Resource Consumption
• Uncontrolled Recursion

There are also more subtle issues that root in the format itself, such as:

• Format confusion. It occurs when objects from different semantic domains, or distinct objects from the same semantic domain are encoded with the same byte representation. In this case, a parser fundamentally cannot distinguish between the two objects, making it vulnerable to cross-protocol attacks.
• Format malleability. It occurs when a single object can be encoded in multiple ways, and a parser accepts all of them. In this case, a parser can be tricked into accepting a modified input that is semantically equivalent to the original, but would yield completely different hash values or signatures. This is a common source of signature forgery or transaction malleability attacks.

Vest addresses these risks with proofs of safety, correctness, and security. The DSL generates these proofs alongside the executable code.

This page describes Vest’s formal guarantees in plain words. For the formal definitions, see the core specs in vest_lib.

Safety, for every format

These hold for every format Vest generates.

• Memory safety. Parsers and serializers are written in safe Rust, so Rust’s ownership and borrowing rules rule out use-after-free and double-free. Verus adds proofs that there are no out-of-bounds accesses.
• Arithmetic safety. No integer overflow or underflow, including in length/offset calculations — the classic place where a hand-written parser goes wrong.
• Termination and panic freedom. Parsing and serializing terminate and never panic, on any input.

Correctness and security

These are the properties that prevent format confusion and malleability. Most, but not every format can satisfy all of them, and Vest is explicit about which properties hold for which formats.

• Parser soundness. If parsing succeeds, the result is a valid instance of the format, and the number of bytes consumed is exactly the formally specified wire length of that instance.
• Parser completeness. Every valid instance of the format can be successfully parsed from its byte representation.
• Parser non-malleability. Each value has a unique byte representation accepted by the parser. Modifying or truncating its consumed bytes changes the outcome — it fails, or yields a different value.
• Parser non-extensibility. Appending bytes to an accepted input does not change what was already parsed.
• Parser productivity. A successful parse consumes at least one byte, making “progress” on the input.
• Serializer non-ambiguity. Two distinct valid values never serialize to the same bytes.
• Round trips. Together, for unambiguous, non-malleable formats, parsing and serializing are mutual inverses: parse-then-serialize reproduces the consumed bytes, and serialize-then-parse recovers the value.

When a format cannot be non-malleable

While non-malleability is the gold standard in cryptographic systems, it violates Postel’s law: be conservative in what you do; be liberal in what you accept. Many foundational security standards explicitly rely on malleability for backwards-compatibility, extensibility, and interoperability. Concise Binary Object Representation (CBOR) permits multiple valid encodings and separately defines deterministic serialization as required; Cryptographic Message Syntax (CMS) permits the malleable Basic Encoding Rules (BER) for many structures and requires Distinguished Encoding Rules (DER) only at particular authenticated boundaries; and Internet Key Exchange (IKE) allows flexible ordering of payloads and defines explicit rules for ignoring payloads to preserve forward compatibility.

In Vest, malleable formats are explicitly marked (those that do not carry the NonMalleable proof trait or only carry it conditionally), so you cannot accidentally rely on uniqueness that is not there. The practical consequence is that if your application needs byte-faithful round trips (e.g., verifying a signature over the bytes you parsed), add NonMalleable as a requirement (trait bound) to your format.

The DSL currently only accepts and produces non-malleable formats, and we are working on bringing malleable features into the DSL securely.

Vest’s Trusted Computing Base (TCB)

The guarantees above rely on the correctness of the following components:

• rustc, the Rust compiler;
• Verus and the Z3 solver;
• vstd’s trusted specifications;
• top-level theorem statements in vest_lib.

Vest also says nothing about whether your format is the right format. That it parses/serializes safely and securely does not mean it matches the RFC you are reading. For now, we recommend testing your format against real-world corpora. In the future, we hope to provide an automated testing framework that checks a format against its RFC or other authoritative specification, and flags any discrepancies.

Vest language reference

Overview

How each construct is described

Every format construct is given as what it means on the wire, plus how it behaves under Vest’s three core executable APIs:

• parse reads bytes and returns a value together with the number of bytes consumed;
• prepare checks that a value is consistent with the format (its dependencies, constants, and refinement constraints all hold) and returns the exact number of bytes it will occupy;
• serialize writes a prepared value into a caller-owned buffer of exactly that size, without failing or allocating.

The generated Rust code guide explains the Rust types, format types, executable APIs, and specs/proofs that the compiler emits for each construct. The construct-to-Rust table provides a quick reference for the DSL constructs and their corresponding Rust types.

Limitations

• The DSL does not support polymorphic or “higher-kinded” formats that take other formats as parameters.
• The DSL does not support arbitrary semantic transformations or parsing actions on the data.
• The DSL does not support expressing backward dependencies (e.g., a field that depends on a later field like footers).
• The DSL does not have a module/namespace system (so you cannot “import” a format from another .vest file).
• The DSL does not support declaring “trusted”/“external” formats that are implemented in Rust/Verus and used in the DSL.

File structure and lexical rules

A .vest file is a sequence of top-level definitions in any order: format definitions, constant definitions, macro definitions, and at most one byte-order (endianness) directive.

Identifiers and reserved words

Identifiers start with a letter or _ and continue with letters, digits, or _. Format names, field names, and enum variants all use this form.

These words are reserved and cannot be used as identifiers:

macro   const   enum   choose   wrap
Option  Vec     Tail   Nothing  Never
btc_varint      uleb128

Integer type names are also reserved: any u or i followed by digits, so u8, u16, u3, i32 and so on are unavailable as names.

Field names and parameters become Rust variables in the generated code, so a few more names are unavailable for them:

• Rust keywords, such as type, match, self, and box, and the Verus keywords ghost, tracked, and exec;
• names the generated code uses for its own variables: ibuf, obuf, old_obuf, v, rest, total_n, parse_spec, gas, and n or l followed by digits (n1, l2, …);
• in a bits format, also n, and the names of the helpers generated for it: pack_<format>, unpack_<format>, <format>_bounds, and <enum>_to_bits, <enum>_from_bits, <enum>_wf for any enum.

The following identifier forms have extra syntax:

Comments

Only line comments exist:

// this is a comment

There is no block comment syntax (/* ... */).

Byte order

!BIG_ENDIAN

or

!LITTLE_ENDIAN

Note:

• Little-endian is the default. A file with no directive is little-endian.
• The directive is file-global, wherever it appears. Putting !BIG_ENDIAN on the last line still applies it to every definition in the file.

Byte order applies only where it is meaningful: multi-byte integers. It does not affect u8, byte arrays, or an 8-bit bits block.

Integer literals

There are three forms, usable anywhere a constant integer is expected — enum values, constraints, constant fields, array lengths:

Similar to Rust, enum values may carry a type suffix that fixes the underlying representation:

kind = enum { A = 0u16, B = 1u16, }

Constant arrays

Byte-array constants take either a string or a list form, and the list form has a repeat shorthand:

const MAGIC: [u8; 4] = "vest"
const ZEROS: [u8; 4] = [0; 4]
const BYTES: [u8; 3] = [0x01, 0x02, 0x03]

Whitespace

Whitespace, including newlines, is insignificant. Fields and enum variants are comma-terminated — including the last one:

msg = {
    a: u8,
    b: u16,     // trailing comma required
}

Vim and Neovim highlighting

The repository includes vest/vest.vim. Copy it to ~/.vim/syntax/vest.vim (or ~/.config/nvim/syntax/vest.vim) and add this to your Vim configuration:

autocmd BufRead,BufNewFile *.vest setfiletype vest

Primitive formats

Primitive formats are the leaves from which larger formats are composed.

Unsigned integers

A fixed-width big- or little-endian integer.

!BIG_ENDIAN

header = {
    kind: u8,
    length: u16,
    sequence: u24,
    timestamp: u32,
    nonce: u64,
}

u8, u16, u24, u32, and u64 are supported. Multi-byte integers follow the file’s byte order. The generated Rust types are the matching unsigned integer types, except that u24 is represented as u32 (with proper value constraints specified in Verus).

Parsing. Reads exactly the declared number of bytes and interprets them in the specified byte order. Fewer bytes remaining than the width is a parse error.

Preparation and serialization. Preparation reports the fixed width. For u24, it also checks that the u32 value fits in 24 bits; values above 0xFFFFFF are rejected. Preparation for the other widths always succeeds. Serialization writes that many bytes in the same byte order.

Signed counterparts are supported in the vest_lib backend, but not yet exposed in the DSL (currently rejected during type checking, but we plan to support them soon). Widths other than the five listed above are rejected too. See bitfields for ways to specify bit-sized integers inside a bits block.

Variable-width integers

btc_varint is Bitcoin’s CompactSize unsigned integer and maps to u64 in Rust. The encoding is one byte for small values and a tagged 3-, 5-, or 9-byte form otherwise, so its width depends on the value.

input = {
    flags: u8,
}

transaction_prefix = {
    @input_count: btc_varint, // 1, 3, 5, or 9 bytes
    inputs: [input; @input_count],
}

Parsing. Reads the leading tag byte, then the remaining bytes according to the tag. Interprets the result as a u64. Only the shortest encoding of a value is accepted — a value padded into a wider form is rejected, which is what keeps the format non-malleable.

Preparation and serialization. Preparation reports the width of the shortest encoding for that value. Serialization writes exactly that form.

The vest_lib backend also supports other variable-length integers such as uleb128, base128 (VLQ), and base256. We plan to expose them in the DSL soon.

Bytes and arrays

[u8; length] is a run of raw bytes of a known length, mapping to a Rust byte slice (&[u8]) to avoid unnecessary copying.

digest = [u8; 32]

Parsing. Takes exactly length bytes and borrows them from the input.

Preparation and serialization. Preparation checks that the slice is exactly length bytes long and reports that length; a slice of any other size is an error. Serialization copies the bytes through unchanged.

For non-byte elements, [format; count] is a repeated format, and a constant count produces a Rust array:

words = [u16; 8]

Lengths and counts may also use runtime dependencies and arithmetic; see Structures and dependencies, and Collections for the repetition semantics.

Tail, Nothing, and Never

payload = {
    header: u16,
    body: Tail,
}

empty = Nothing
reject = Never("this branch is reserved")

Tail can be used to “under-specify” a format, leaving the rest of the input uninterpreted. Nothing can be used as the “do-nothing” branch of a choice; Never marks a branch that must never be taken, and gives the resulting parse error a message you choose. See Choices.

Refinements

A refinement narrows an existing format to a subset of its values. The wire encoding and the Rust type are unchanged, only the set of accepted values shrinks.

Parsing. Parses the underlying format, then tests the predicate. A value outside the refinement is a parse error.

Preparation and serialization. Preparation tests the same predicate on the value and fails if it does not hold. Length and serialization are those of the underlying format.

The predicate is therefore enforced in both directions.

Integer constraints

constrained = {
    exact: u8 | 7,
    range: u16 | 1..1024,
    lower_bounded: u32 | 1..,
    upper_bounded: u16 | ..4096,
    selected: u8 | {1, 4, 9},
    except: u8 | !{0, 255},
}

Vest ranges include both supplied endpoints: 1..1024 accepts 1 through 1024. Either endpoint may be omitted. A set uses braces and commas; prefixing a constraint with ! takes its complement. Values and range endpoints must fit the underlying integer type.

Enum constraints

Named enum formats can be restricted by variant:

kind = enum {
    Request = 1,
    Response = 2,
    Error = 3,
}

messages = {
    request: kind | Request,
    not_error: kind | !Error,
    terminal: kind | {Response, Error},
}

Every named variant must belong to the referenced enum. The generated field still has type Kind; the refinement changes only which values are consistent with the format.

Structures and dependencies

A struct is a fixed sequence of fields laid out back to back on the wire (without padding). The DSL generates a Rust struct with the same field names, in the same order (though Rust may add padding for alignment or reorder fields for better layout).

record = {
    kind: u8,
    flags: u16,
    payload: [u8; 8],
}

Every field is followed by a comma, including the last one.

Parsing. Parses each field in definition order. The bytes consumed are the sum of the fields’ wire lengths. The parsed value is Record { kind, flags, payload }.

Preparation and serialization. Preparation prepares each field, adds up the lengths with an overflow check, and fails if any field fails. Serialization writes the fields in the same order, back to back.

Dependency fields

Prefix a field name with @ to let later fields refer to its value:

packet = {
    @length: u16,
    payload: [u8; @length],
}

The generated value is Packet { length, payload }. The @ field is present on the wire and in the Rust value.

Parsing. @length is parsed like any other field; its value is then in scope, so [u8; @length] knows how many bytes to take.

Preparation and serialization. The direction reverses: @length is now a consistency requirement. Preparation checks that the payload really is length bytes and fails otherwise. Serialization then writes both fields normally.

A dependency may refer only to a preceding field or a format parameter. Dotted field access is supported for nested structs:

header = {
    kind: u8,
    payload_length: u32,
}

framed = {
    @header: header,
    body: [u8; @header.payload_length],
}

Constant fields

A field whose value is fixed by the format — a magic number or version byte:

message = {
    const version: u8 = 1,
    const magic: [u8; 4] = "vest",
    body: Tail,
}

Parsing. Reads the field and requires it to equal the declared constant; anything else is a parse error.

Preparation and serialization. Constant fields are still present in the generated struct, so preparation rejects a caller value whose field differs, and serialization writes the declared bytes. Use wrap when framing constants should be absent from the value type entirely.

Top-level constants can name byte, integer, or enum constants for reuse:

const MAGIC: [u8; 4] = "vest"

message = {
    const magic: MAGIC,
    body: Tail,
}

Length expressions

Array and byte-string lengths support integer literals, dependencies, static format sizes, parentheses, and arithmetic:

header = {
    @total: u16 | 8..,
    flags: u8,
}

body(@header: header) = {
    payload: [u8; @header.total - |header|],
}

|format| is the static serialized size of a fixed-width named or primitive format. It is rejected for dynamically sized or parameter-dependent formats.

Parsing and preparation. The expression is evaluated the same way in both directions — to decide how many bytes to read, and to check how many bytes a value must occupy. The arithmetic is checked for overflow and underflow in the executable code (statically by Verus for parsing, and at runtime for preparation).

Enums

An enum is an integer on the wire with a name for each meaningful value. It corresponds to a Rust enum with the same discriminants. The generated Rust type is #[repr(uN)] where N is the backing width.

Closed enums

message_type = enum {
    Request = 1,
    Response = 2,
    Error = 3,
}

This emits a MessageType Rust enum. Values must be distinct and fit the inferred backing width.

Parsing. Reads the backing integer and maps it to a variant. Any other value is a parse error.

Preparation and serialization. Preparation always succeeds and reports the backing width. Serialization writes the variant’s discriminant as the backing integer.

Open enums

Add ... after the variants to preserve unknown values:

message_type = enum {
    Request = 1,
    Response = 2,
    ...
}

Parsing. A recognised value maps to its variant, and anything else is kept as Unknown(value).

Preparation and serialization. Same width as the closed form. Known variants serialize as before; Unknown(value) serializes as value.

Choosing the backing width

The backing width is what actually determines how many bytes appear on the wire. Without a suffix, Vest selects the smallest unsigned width containing every value. A suffix on any enumerator fixes the type; all supplied suffixes must agree:

wide_type = enum {
    Request = 1u16,
    Response = 2,
}

The supported executable backing widths are u8, u16, u24, u32, and u64.

Inside a bits block, a suffix such as 0u3 instead selects a three-bit enum. See Bit fields.

Choices

A choice is a format that can take one of several shapes. It generates a Rust enum, so the alternative that matched is recorded in the value. Vest has dependent choices, where an earlier field selects the branch, and non-dependent choices, where branches are tried in order.

Enum-dependent choices

kind = enum {
    Short = 1,
    Long = 2,
}

body(@kind: kind) = choose(@kind) {
    Short => u16,
    Long => u64,
}

Parsing. The dependency has already been parsed, so the branch is chosen directly — no backtracking, and no ambiguity about which arm applies.

Preparation and serialization. Preparation checks that the variant in your value matches the branch the dependency selects; a Long body under a Short tag is rejected before any bytes are written. It then prepares that branch. Serialization writes the selected branch only.

A closed enum choice must cover every declared variant unless it has a final wildcard. An open enum choice requires a final _ branch. Branch names must be unique and belong to the enum.

Integer-dependent choices

body(@kind: u8) = choose(@kind) {
    1 => u16,
    2..10 => u32,
    _ => Never("unknown body kind"),
}

Integer patterns use the same values and ranges as refinements. Explicit patterns must not overlap, and a final wildcard is mandatory because the integer domain is otherwise open. Semantics are as above: the dependency picks the arm, and the value must match that arm.

Byte-string-dependent choices

record = {
    @magic: [u8; 2],
    body: choose(@magic) {
        [0x01, 0x02] => u16,
        [0x03, 0x04] => u32,
        _ => Nothing,
    },
}

Every explicit byte pattern must have the same length as the dependency, and a final wildcard is required.

Variant names

Each branch becomes a variant of the generated Rust enum. An enum-dependent choice names its variants after the enum’s, and its _ branch Default. Integer and byte-string patterns have no name of their own, so a branch whose format is a named definition is named after that definition, and any other branch is Variant1, Variant2, … by position (Default for _):

request = {
    id: u32,
}

reply = {
    status: u8,
}

message = {
    @magic: [u8; 2],
    body: choose(@magic) {
        [0x01, 0x02] => request,  // MessageBody::Request
        [0x01, 0x03] => u16,      // MessageBody::Variant2
        _ => reply,               // MessageBody::Reply
    },
}

If two branches invoke the same definition, both fall back to positional names.

Non-dependent ordered choices

Without (@dependency), there is no tag to dispatch on, so the branches are distinguished by their own content:

small = choose {
    Tiny(u8 | 0..9),
    Medium(u8 | 10..100),
}

// or equivalently
small_arrow = choose {
    Tiny => u8 | 0..9,
    Medium => u8 | 10..100,
}

Parsing. Branches are attempted in source order and the first success wins. A failed attempt consumes nothing, so the next branch starts from the same position.

Preparation and serialization. Preparation checks whichever branch the value holds; serialization writes it.

Note that for non-dependent choices, the variant names (Tiny and Medium) are not part of the wire. In this case, Vest requires that the branches are non-overlapping, which is required for the parser to be able to unambiguously select the correct branch.

Wildcard rules

• _ may appear at most once and must be the final branch.
• Integer and byte-string choices require it.
• Open-enum choices require it.
• A closed-enum choice is normally written exhaustively, but a final _ is allowed to “catch all” other variants.

Collections

Fixed and dependency-sized arrays

A repetition of one format a known number of times.

fixed_words = [u16; 8]

counted = {
    @count: u16,
    words: [u32; @count],
}

A constant count generates a Rust array. A dependency-sized repetition generates a Vec, because its length is known only at runtime. [u8; length] is specialized to a borrowed byte slice.

Parsing. Parses the element format exactly count times, one after another.

Preparation and serialization. Preparation checks that the collection holds exactly count elements, prepares each element, and sums the lengths. Serialization writes the elements back to back.

Nested arrays are supported:

matrix = {
    @rows: u16,
    @columns: u16,
    cells: [[u8; @columns]; @rows],
}

Vec

A repetition with no count: zero or more occurrences of a format. The result is a Vec in Rust.

item = { value: u16, }

items = Vec<item>

Parsing. Repeats the element format until it errors (e.g., the input is exhausted).

Preparation and serialization. Preparation prepares every element and sums the lengths. Serialization writes the elements in order.

Because there is no count, the element must be productive — every successful element parse must consume at least one byte. Otherwise repetition could loop forever. Verus will check this property in the emitted Rust code and reject the format if productivity cannot be proven for the element format.

Option

Zero or one occurrence of a format.

tagged = wrap(u8 = 1, u16)
maybe_tagged = Option<tagged>

Parsing. Tries the inner format. On success the result is Some(v); on failure the result is None and no input is consumed, so parsing continues from the same position.

Preparation and serialization. Some(v) prepares and writes the inner format; None has length 0 and writes nothing.

Notes on Vec and Option

Because a Vec can be empty and an Option can be absent, the surrounding format must make their presence distinguishable from what follows — a tagged or otherwise disjoint inner format is the usual pattern. A chain of ambiguous Vec or Option fields will fail the generated unambiguity proof obligations.

>>=

left >>= right means “take the region left describes, then parse right against it.”

The corresponding Rust value type of the whole expression is the same as right’s.

Parsing. Extract a bounded region from the input defined by left, then parse right from that region. right must consume the region entirely — leftover bytes are an error.

Preparation and serialization. Preparation prepares right and requires its length to equal the region left declares. Serialization writes right’s bytes directly.

Currently, the left side must be [u8; length] or Tail. We’re working on generalizing this to any format that can be reinterpreted within a bounded region.

Bounding Vec with a length field

item = { value: u16, }

list = {
    @byte_length: u16,
    values: [u8; @byte_length] >>= Vec<item>,
}

Here, Vec<item> repeats until its region ([u8; @byte_length]) runs out. Because the region is exactly byte_length bytes, the repetition will eventually stop. Preparation checks that the items really do add up to byte_length.

Reinterpreting the remainder of a region

Tail names everything left in the enclosing region, which turns >>= into “reinterpret the remainder”:

item = { value: u16, }

items = Tail >>= Vec<item>

This is the idiom for a message that ends in an unknown number of records. It also composes: inside a format already bounded by a length field, Tail means the rest of that region, not the rest of the original input buffer.

Bit fields

bits { ... } describes several small unsigned fields packed into one fixed-width integer on the wire. The block as a whole is a single integer; the fields are slices of its bits. The DSL compiler exposes them as ordinary integer-typed Rust fields.

ipv4_first_byte = bits {
    version: u4,
    ihl: u4,
}

Fields are laid out from the most significant bit of the integer, in declaration order. The total width must be exactly 8, 16, 24, 32, or 64 bits; otherwise the compiler reports an invalid total width. Each individual width must be positive and no larger than 64.

Parsing. Reads the integer according to the specified byte order, then splits it into fields from the most significant bit down, and checks each field’s constraint.

Preparation and serialization. Preparation checks that each field fits its declared bit width and satisfies its constraint, and reports the integer’s width. Serialization packs the fields back into one integer and writes it in the specified byte order.

Cross-byte fields and byte order

!BIG_ENDIAN

packed = bits {
    prefix: u3,
    value: u10,
    suffix: u3,
}

Fields may straddle byte boundaries; only the integer as a whole is required to be byte aligned. Byte endianness controls how that multi-byte integer is decoded/encoded. It has no effect on abstract ordering of the fields, which is always from the most significant bit down. For example, the packed format above specifies a 16-bit integer with three bit fields.

| prefix (3 bits) |      value (10 bits)      | suffix (3 bits) |

In big-endian order, the first byte is the most significant, so the fields are encoded as follows:

|b00|b01|b02|b03|b04|b05|b06|b07|b08|b09|b10|b11|b12|b13|b14|b15|
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|   prefix  |                 value                 |   suffix  |

In little-endian order, the first byte is the least significant, so the fields are encoded as follows:

|b00|b01|b02|b03|b04|b05|b06|b07|b08|b09|b10|b11|b12|b13|b14|b15|
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|    value (low 5)  |  suffix   |   prefix  |   value (high 5)  |

Constraints and enums

Bit-sized integers use the ordinary refinement syntax, with the same two-way enforcement described in Refinements. Enum suffixes may select an exact bit width:

payload_kind = enum {
    Raw = 0u3,
    Words = 1u3,
    ...
}

header = bits {
    @kind: payload_kind,
    @count: u5 | 1..31,
    @length: u8,
}

packet = {
    @header: header,
    body: choose(@header.kind) {
        Raw => [u8; @header.length],
        Words => [u16; @header.count],
        _ => [u8; @header.length],
    },
}

Only unsigned integers and enums with unsigned bit-sized integer types are allowed as bit fields. Dependency fields and dotted access work exactly as in ordinary structures: @kind is unpacked while parsing the integer and is then in scope for later fields, and preparation enforces it as a constraint in the other direction.

Composition

Format aliases

A definition may directly reuse another format:

header = { kind: u8, length: u16, }
header_alias = header

The alias receives its own generated format name while using the referenced value type. Parsing, preparation, and serialization are those of the referenced format; the alias adds no wire bytes.

Framing with wrap

wrap surrounds a format with fixed bytes that carry no semantic information (e.g., a magic prefix, a terminator, or padding) and keeps them out of the value.

framed_word = wrap(
    u8 = 0xAA,
    u16,
    [u8; 2] = [0x0D, 0x0A]
)

The generated value type for framed_word is just u16.

Parsing. Recognizes the prefix constants, parses the inner format, then recognizes the suffix constants. A constant that does not match is a parse error. The framing bytes are consumed but discarded.

Preparation and serialization. Preparation reports the inner length plus the widths of all the constants. Serialization writes the prefix, the inner value, and the suffix.

This is the difference from a const structure field, which stays part of the generated struct and must be supplied by the caller during preparation and serialization.

wrap accepts any number of constant integer, byte-string, or enum formats before and after its one non-constant inner format.

Parameterized formats

payload(@length: u16) = [u8; @length]

packet = {
    @length: u16,
    body: payload(@length),
}

Parameters are values supplied by the enclosing format. They are not part of the generated value type.

Parsing and preparation. A parameter contributes no bytes of its own. It behaves exactly like a dependency but is required to be bound externally in the enclosing format.

When invoked, arguments must be @ dependencies in scope and must match the declared parameter format.

Macros

Macros substitute format arguments before type checking:

macro length_prefixed!(length_format, body_format) = {
    @length: length_format,
    body: [u8; @length] >>= body_format,
}

words = length_prefixed!(u16, Vec<u32>)

Macro arguments are format expressions. Macros are purely syntactic and have no semantics of their own. The expansion behaves exactly as if you had written it out.

Recursion

Named formats may refer to themselves directly or through other definitions:

list_kind = enum {
    Nil = 0,
    Cons = 1,
}

list = {
    @kind: list_kind,
    value: choose(@kind) {
        Nil => Nothing,
        Cons => {
            head: u8,
            tail: list,
        },
    },
}

The compiler finds strongly connected components (SCCs), so mutually recursive definitions are supported too. It emits owned Box links where Rust needs indirection in the value type.

Parsing. Recurses as the input demands, up to a fixed depth bound statically picked by the format. Exceeding the bound is a parse error.

Preparation and serialization. Preparation walks the value to the same bound, summing lengths, and fails if the value nests deeper than the format allows. Serialization traverses the value and writes the bytes in order.

Note

Though vest_lib defines a bounded fixpoint format combinator that can express arbitrary recursion, the compilation of recursive formats in Vest DSL is experimental: the implementation is incomplete and there is some engineering work remaining for a more robust support.

Construct-to-Rust mapping

A quick-lookup table from DSL construct to the Rust type it generates.

Names are converted to UpperCamelCase: msg_type becomes MsgType. Alongside each value type, the compiler emits a zero-sized format type — MsgTypeFmt — that carries the parser, serializer, and proofs. See Generated Rust Code for the full set of emitted names.

Generated Rust Code

This page is the reference for the Rust/Verus code that Vest emits from a DSL definition. It first takes a complete tour of a generated file, then covers the API for calling the generated code and for reasoning about it in Verus.

We’ll use a variable-length message format as the running example. The DSL definition is

message = {
    @length: u16,
    payload: [u8; @length],
}

Compiling src/message.vest to src/message.rs gives these two user-facing types:

#[derive(Debug, PartialEq, Eq, Clone, Copy)]
pub struct Message<'i> {
    pub length: u16,
    pub payload: &'i [u8],
}

pub struct MessageFmt;

If you are only interested in invoking the generated code, you can skip ahead to Calling the generated code.

Inside the generated file

The shape of an emitted file

The file starts with a comment identifying the vest compiler version and warning against manual edits: change the .vest source and regenerate instead. The whole module is a single verus! block behind a fixed use preamble. It is divided into six sections:

use vest_lib::prelude::*;                // common APIs, combinators, and Verus prelude
// ...additional imports for generated mapping and recursion helpers
verus! {

// ============================================================
// Data Types
// ============================================================
// ============================================================
// Structural Mappers
// ============================================================
// ============================================================
// Format Specifications
// ============================================================
// ============================================================
// Derived Parser, Serializer, Length, and Consistency Specifications
// ============================================================
// ============================================================
// Proven Format Properties
// ============================================================
// ============================================================
// Executable Implementations
// ============================================================

} // verus!

Each section covers every definition in the file. A file with nine definitions emits all nine value types, then all nine nominal format types, then all the derived specifications, and so on. The last three sections only implement traits for the format types, so they are wrapped in private modules (derived_specs, derived_proofs, and exec_impls).

The compiler pretty prints its output in the style of rustfmt/verusfmt, so generated files need no separate formatting pass (in fact, verusfmt would hang on those deeply nested combinator expressions that the compiler emits).

Data Types

Besides Message, Vest emits an abstract value type (MessageSpec), a structural representation (MessageInner), and a DeepView implementation that maps the executable value to its abstract value:

#[verifier::ext_equal]
pub struct MessageSpec<T0 = u16, T1 = Seq<u8>> {   // abstract view of Message
    pub length: T0,
    pub payload: T1,
}

pub type MessageInner = (u16, Seq<u8>);           // what the Vest combinators operate on

impl<'i> DeepView for Message<'i> {               // exec value -> abstract value
    type V = MessageSpec;
    #[verifier::opaque]
    open spec fn deep_view(&self) -> Self::V { /* field-wise */ }
}

MessageSpec has the same fields as Message, but the borrowed payload becomes a Seq<u8>. Vest specs and proofs talk about these abstract values.

Structural Mappers

The vest_lib combinators operate on the structural representation (MessageInner), while the “view” of Message is the more ergonomic nominal type MessageSpec. This section converts between the two. It also declares two empty structs, MessageForward and MessageReverse, which name the conversion for the Mapped combinator:

impl<T0, T1> MessageSpec<T0, T1> {                // abstract value <-> nested tuple
    #[verifier::opaque] pub open spec fn from_structural(input: (T0, T1)) -> Self { /* .. */ }
    #[verifier::opaque] pub open spec fn into_structural(self) -> (T0, T1) { /* .. */ }
    pub proof fn lemma_from_into(self) { /* .. */ }
    pub proof fn lemma_into_from(input: (T0, T1)) { /* .. */ }
}

// The bijection between the structural tuple and the nominal abstract value
#[doc(hidden)] pub struct MessageForward;
#[doc(hidden)] pub struct MessageReverse;

For a choose, the same items appear with enum instead of struct, and MessageInner becomes nested Sums rather than a nested tuple.

Format Specifications

spec_inner() describes the DSL definition as a tree of vest_lib format combinators:

pub type MessageFmtSpec =
    Named<Mapped<Bind<U16Le, spec_fn(u16) -> Varied<u16>>, BiMap<MessageForward, MessageReverse>>>;

impl MessageFmt {
    pub open spec fn spec_inner() -> MessageFmtSpec {
        Named("message", Mapped {
            inner: Bind(U16Le, |length: u16| Varied(length)),
            mapper: BiMap(MessageForward, MessageReverse),
        })
    }
}

Each DSL construct has a matching combinator: @length: u16 becomes Bind(U16Le, |length: u16| ...), and [u8; @length] becomes Varied(length). The Named wrapper gives the format a human-readable name for error reporting.

Derived Specifications

Because spec_inner() is built from vest_lib combinators, the format’s formal specifications can be derived from it:

impl SpecParser        for MessageFmt { type PVal   = MessageSpec; /* spec_parse */ }
impl Consistency       for MessageFmt { type Val    = MessageSpec; /* consistent */ }
impl SpecSerializer    for MessageFmt { type SVal   = MessageSpec; /* spec_serialize */ }
impl SpecByteLen       for MessageFmt { type T      = MessageSpec; /* byte_len */ }

For MessageFmt, the parser, serializer, and byte-length specs are marked #[verifier::opaque], while value consistency spec is transparent. Together with the opaque deep_view, these define what a verified client can see by default. A proof can reveal the public length calculation without opening the structural conversion or the parser and serializer specs, as we’ll see in Concrete fields and byte lengths.

Proven Format Properties

The proofs of format properties are also mostly derived from spec_inner():

broadcast use {
    vest_lib::combinators::disjoint::disjointness_lemmas,
    MessageSpec::lemma_from_into,
    MessageSpec::lemma_into_from,
};

impl SafeParser  for MessageFmt { /* .. */ }
impl Productive  for MessageFmt { /* .. */ }
impl SoundParser for MessageFmt { /* .. */ }
impl SPRoundTripDps for MessageFmt { /* .. */ }
impl NonMalleable for MessageFmt { /* .. */ }
// ...plus more auxiliary proof traits, depending on the format

Each proof reveals the opaque specifications it needs, then hands off to the corresponding lemma on spec_inner(). disjointness_lemmas is a broadcast group of lemmas that compositionally establish that certain combinators are unambiguous, which serialize-then-parse roundtrips require.

You won’t find emitted implementations of SPRoundTrip, PSRoundTrip, or NonAmbiguous: the library derives them once-and-for-all from the generated proof traits through blanket implementations. Together, these traits provide the theorems that client proofs call:

• theorem_serialize_parse_roundtrip comes from SPRoundTrip.
• theorem_parse_serialize_roundtrip comes from PSRoundTrip.
• lemma_parse_non_malleable comes from NonMalleable.
• lemma_serialize_injective comes from NonAmbiguous.

Executable Implementations

Finally, the file implements the executable Parser, Serializer, and Prepare traits. These implementations are not derived from spec_inner(). They are written as idiomatic imperative Rust, which keeps them fast and avoids any potential combinator overhead:

impl<'i> Parser<&'i [u8]> for MessageFmt {
    type PT = Message<'i>;
    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> { /* .. */ }
}

impl<Output: OutputBuf, 'i> Serializer<Output, Message<'i>> for MessageFmt {
    fn serialize_into(&self, v: &Message<'i>, obuf: &mut Output) { /* .. */ }
}

impl<'i> Prepare<Message<'i>> for MessageFmt {
    fn prepare(&self, v: &Message<'i>) -> Result<usize, PreSerializeError> { /* .. */ }
}

parse walks the fields, advancing a cursor and propagating failure with ?. It then assembles the value and asserts that it matches spec_parse:

let (n1, length)  = U16Le.parse(&rest)?;
let rest          = rest.skip(n1);
let (n2, payload) = Varied(length).parse(&rest)?;
// ...
Ok((n1 + n2, Message { length, payload }))

serialize_into walks the same fields, writing each one directly into the output buffer. prepare walks them to check consistency and add up their lengths.

Calling the generated code

From ordinary Rust, you call these implementations through traits in vest_lib::core::exec:

Neither serializer rechecks consistency, so unverified code must call prepare first; see Serializing a message.

Failures return a ParseError or a PreSerializeError. Each records the kind of failure and the innermost named format that reported it. Enable vest_lib’s error-trace feature to also keep the trace of enclosing formats.

Reasoning about generated values

We’ve seen that the getting-started example proves a value serialize-parse roundtrip. This section further covers:

• what each executable API guarantees,
• how to prove facts about fields and lengths,
• and which theorems relate parsing and serialization.

The examples belong inside a verus! block. They use crate::message::* and vest_lib::prelude::*. The prelude brings the executable APIs, specification and proof traits, format combinators, and the Verus prelude into scope.

Values and API contracts

vest_lib’s broadcast group basic_lemmas covers some basic useful facts about byte buffers and serialization lengths, which apply automatically when vest_lib::prelude::* is in scope.

For more facts about parsed values, enable parser_lemmas in the function or proof that needs them:

broadcast use parser_lemmas;

These lemmas tell Verus three things about a successful parse: it stays within the input buffer, it produces a value consistent with the format, and it consumes exactly that value’s byte_len. Roundtrip and non-malleability theorems still have to be called explicitly.

Concrete fields and byte lengths

To prove facts about individual fields or concrete lengths, use Verus’s reveal to open the view and length definitions. This function builds a message, serializes it, parses it back, and proves the exact length and field values:

fn check_message() -> Result<(), PreSerializeError> {
    let value = Message { length: 3, payload: &[0xCA, 0xFE, 0x42] };
    proof {
        reveal(<Message as DeepView>::deep_view);
        reveal(<MessageFmt as SpecByteLen>::byte_len);
    }
    let len = MessageFmt.prepare(&value)?;
    assert(len == 5); // 2 length bytes + 3 payload bytes

    let mut output = vec![0u8; len];
    MessageFmt.serialize(&value, &mut output);
    proof {
        MessageFmt.theorem_serialize_parse_roundtrip(value.deep_view());
    }
    let (consumed, parsed) = MessageFmt.parse(&output.as_slice()).unwrap();
    assert(consumed == 5);
    assert(parsed.length == 3);
    assert(parsed.payload@ == seq![0xCAu8, 0xFE, 0x42]);
    Ok(())
}

The first reveal connects the Rust fields to their logical counterparts, and the second exposes the length calculation. Without either one, Verus can’t prove the assertions. The roundtrip theorem says that parsed has the same deep view as value, and the revealed view turns that into the concrete field values.

Both definitions are opaque by default, which keeps proofs about deeply nested formats manageable. Here, only the public view and length are opened. The parser and serializer specifications stay closed, and the internal structural representation never needs to be revealed.

For a nested format, reveal a child type’s view only when you need to reason about that child’s fields; its format specifications can stay closed.

Fixed-length formats need even less proof code. When the compiler can determine a fixed length, it emits a verified StaticByteLen implementation for the format. For example, compile these definitions to src/lengths.rs:

triple = {
    a: u8,
    const b: [u8; 2] = [0x55, 0x77],
    c: u64,
}

samples = {
    @count: u16,
    values: [u16; @count],
}

Here, a prepared Triple takes 11 bytes (1 + 2 + 8), and proving it needs no reveals:

fn fixed_length(value: &Triple) -> Result<usize, PreSerializeError> {
    let len = TripleFmt.prepare(value)?;
    assert(len == 11);
    Ok(len)
}

Samples has a variable length, but each element is a fixed-width u16. After the usual reveals, we can assert that the length is 2 + 2 * count:

fn samples_length(value: &Samples) -> Result<usize, PreSerializeError> {
    proof {
        reveal(<Samples as DeepView>::deep_view);
        reveal(<SamplesFmt as SpecByteLen>::byte_len);
    }
    let len = SamplesFmt.prepare(value)?;
    assert(len == 2 + 2 * value.values@.len());
    Ok(len)
}

vest_lib also provides the ByteLen::length API for infallible length calculation, but the DSL doesn’t currently generate it. Unlike prepare, length doesn’t check consistency, and it needs a proof that the length fits in usize.

Roundtrips and non-malleability

The getting-started example proves facts in the direction of value –> bytes –> value, leveraging theorem_serialize_parse_roundtrip. theorem_parse_serialize_roundtrip goes the other way, from bytes –> value –> bytes. It is useful for re-encoding a message:

fn reencode(input: &[u8]) -> Result<Vec<u8>, ParseError> {
    broadcast use parser_lemmas;

    let (consumed, value) = MessageFmt.parse(&input)?;
    let mut output = vec![0u8; consumed];
    MessageFmt.serialize(&value, &mut output);
    proof {
        MessageFmt.theorem_parse_serialize_roundtrip(input@);
    }
    assert(output@ == input@[0..consumed]);
    Ok(output)
}

Note that no prepare is needed here. parser_lemmas already establish that value is consistent with the format and that consumed is its exact length. The equality covers only the consumed prefix. It also inherently requires non-malleability: a malleable format, such as ASN.1 BER, may accept several encodings of the same value during parsing and serialize it to a different binary form.

See the proof traits in vest_lib for more details on the roundtrip and non-malleability theorems.

Command-line interface

Synopsis

vest [OPTIONS] <VEST_FILE>

A successful run should print the following five stages and exit zero:

$ vest msg.vest -o src/msg.rs
📜 Parsing the vest file...
🔨 Elaborating the AST...
🔍 Type checking...
📝 Generating the verus file...
👏 Done!

Generating from build.rs

For a project that keeps its .vest schema under version control and regenerates the Rust code on change, we recommend a build.rs that calls the compiler. Add vest as a build dependency and use one of three entry points:

// build.rs
use std::error::Error;
use vest::compile_to;

fn main() -> Result<(), Box<dyn Error>> {
    println!("cargo::rerun-if-changed=src/msg.vest");
    compile_to("src/msg.vest", "src/msg.rs")?;
    Ok(())
}

All three report diagnostics to stderr and return Err on failure.

Troubleshooting

TODO. This page is not written yet.

It will cover the Vest DSL compiler, Verus verification, and runtime errors you are most likely to hit.

Using vest_lib

TODO. This page is not written yet.

Most applications should use the Vest DSL or the ASN.1 frontend, which generate parsers and serializers for you, composed with format combinators in vest_lib. This page will cover the case where you prefer writing them by hand: when a format is too complex to express in the DSL.

Until then, the combinators module documentation lists every primitive and higher-order format with its semantics and vest_dev/src/formats holds some handwritten examples that demonstrate how to use them.

Feature configurations

vest_lib supports three runtime environments:

[dependencies]
vest_lib = { version = "0.2", default-features = false, features = ["alloc"] }

std enables alloc. Without alloc, one can still use fixed-width formats, formats with raw byte fields, and serialization into caller-provided slices. Heap-backed collection parsers, owned string values, serialize_with_vec, and the generic CBOR codec require alloc (or std).

Error traces

ParseError and PreSerializeError always retain the failure kind and, when available, the innermost named format that reported it. This does not require allocation.

Enable error-trace to also record a stack of enclosing named formats.

[dependencies]
vest_lib = { version = "0.2", features = ["error-trace"] }

This diagnostic feature is off by default, even with std. It enables alloc but does not require std, so it also works with default-features = false, features = ["error-trace"]. Errors may allocate and become heavier when propagating, so leave it disabled for production builds.

Verus compatibility

Vest and vest_lib must be used with the Verus and vstd versions this release pins. The Verus version is in verus.json and the vstd version is in the workspace Cargo.toml.

ASN.1 Compiler

vest_asn1 parses an ASN.1 module and emits verified formats backed by vest_lib::asn1. DER is the default; BER and definition-level rule overrides are available.

cargo run -p vest_asn1 -- schema.asn1 -o generated.rs
cargo run -p vest_asn1 -- --rules ber schema.asn1 -o generated_ber.rs

Similar to the Vest DSL, each supported ASN.1 definition becomes a user-facing Rust value type and a nominal format type whose specification, proof, and executable implementation are all derived from the inner combinator representation.

Start with the ASN.1 tutorial, then see the generated Rust code and the support table. The backend API is documented under vest_lib::asn1.

DER, BER, and rule overrides

--rules der or --rules ber authoritatively selects the module default. A definition override changes that definition and the transitive children it needs under the selected rule; parents remain under the module default.

cargo run -p vest_asn1 -- --rules ber \
  --der-definition SignedAttributes \
  --der-definition CertificateSet \
  schema.asn1 -o generated_mixed.rs

Every ASN.1 definition is emitted exactly once with one global rule. A BER definition may contain a DER child because a DER encoding is valid BER. However, a DER definition cannot depend on a BER definition without violating DER canonicality. Conflicting transitive overrides are rejected and require an explicit rule boundary.

ASN.1 tutorial

This walkthrough generates a small DER codec from an ASN.1 module and uses it to parse and serialize a message.

Define a module

Create message.asn1:

Message DEFINITIONS EXPLICIT TAGS ::= BEGIN
    Kind ::= ENUMERATED {
        request(0),
        response(1)
    }

    Packet ::= SEQUENCE {
        kind Kind,
        payload [0] IMPLICIT OCTET STRING (SIZE (1..32)) OPTIONAL
    }
END

Generate DER

vest_asn1 is currently a repository tool rather than a published crate:

cargo run -p vest_asn1 -- message.asn1 -o src/message.rs

DER is the default. Use --rules ber for BER, or definition overrides for a module with canonical DER substructures inside a BER envelope; see DER, BER, and rule overrides.

The generator emits Kind and Packet<'i> value types. Unlike the Vest DSL, their verified format values are KIND::Fmt and PACKET::Fmt. Uppercase format names avoid collisions with the idiomatic Rust value names. Tagged formats also store their effective tag to support IMPLICIT retagging.

Parse and serialize

use vest_lib::core::exec::{Parser, Prepare, SerializerExt};
use crate::message::{Kind, PACKET};

let encoded: &[u8] = &[
    0x30, 0x07,             // SEQUENCE, seven content octets
    0x0a, 0x01, 0x00,       // Kind::Request
    0x80, 0x02, 0xaa, 0xbb, // [0] IMPLICIT OCTET STRING
];

let (consumed, packet) = PACKET::Fmt.parse(&encoded).unwrap();
assert_eq!(consumed, encoded.len());
assert_eq!(packet.kind, Kind::Request);
assert_eq!(packet.payload, Some(&[0xaa, 0xbb][..]));

let size = PACKET::Fmt.prepare(&packet).unwrap();
let mut output = vec![0u8; size];
PACKET::Fmt.serialize(&packet, &mut output);
assert_eq!(output, encoded);

DER byte strings and UTF-8-compatible character strings borrow from the input. BER string formats concatenate constructed fragments into owned values. BMPString and UniversalString are always owned because their wire encodings must be converted to UTF-8.

What is checked

TODO. Discuss the proof obligations for format non-ambiguity, etc.

Generated Rust Code

An ASN.1 definition such as Packet becomes a Rust value type Packet and a verified nominal format type PACKET, used as PACKET::Fmt. The screaming-case format name avoids colliding with the idiomatic value name.

SEQUENCE and supported heterogeneous SET definitions become structs; CHOICE becomes an enum carrying the alternatives; and ENUMERATED becomes a closed typed enum. Anonymous composites receive deterministic private helper definitions. IMPLICIT tagging replaces the outer tag; untagged CHOICE and ANY have no single tag to replace, so the generator tags those explicitly.

The examples below come from the module in the tutorial:

Kind   ::= ENUMERATED { request(0), response(1) }
Packet ::= SEQUENCE {
    kind    Kind,
    payload [0] IMPLICIT OCTET STRING (SIZE (1..32)) OPTIONAL
}

The shape of an emitted file

Unlike a DSL-generated module, an ASN.1 module has no banner sections. It is one flat verus! block holding every definition’s types and schema, followed by one small private module per definition outside the block:

use vest_lib::asn1::der::{...};          // preamble selected by the encoding rules
verus! {

    // per definition: value type, abstract type, predicates, mappers,
    // combinator representations, and the nominal format type

} // verus!

mod __impl_kind   { use super::*; vest_lib::impl_der!(...); }
mod __impl_packet { use super::*; vest_lib::impl_der!(...); }

That last part is the biggest structural difference. Where the DSL writes out derived_specs, derived_proofs, and exec_impls explicitly, the ASN.1 backend emits one macro call per definition and lets vest_lib expand the specifications, proofs, and executable code.

Value and abstract types

This matches the DSL closely — a value type and a generic abstract type, bridged by DeepView:

pub struct Packet<'a> {
    pub kind: Kind,
    pub payload: Option<&'a [u8]>,
}

#[verifier::ext_equal]
pub struct PacketSpec<T0 = KindSpec, T1 = Option<Seq<u8>>> {
    pub kind: T0,
    pub payload: T1,
}

impl<'a> DeepView for Packet<'a> {
    type V = PacketSpec;
    #[verifier::opaque]
    open spec fn deep_view(&self) -> Self::V { /* field-wise */ }
}

For a definition whose value type is already Copy and structural — an ENUMERATED, for instance — there is no separate abstract type at all.

#[repr(i16)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, StructuralEq)]
pub enum Kind { Request = 0, Response = 1 }

pub type KindSpec = Kind; // the abstract type is the same as the value type

impl DeepView for Kind { type V = Self; /* *self */ }

Predicates and mappers

ASN.1 constraints become named predicate structs used in both the specification and implementation, rather than the inline closures the DSL emits:

#[derive(Clone, Copy)]
pub struct KindPredicate;

impl SpecPred<i16> for KindPredicate { /* value == 0 || value == 1 */ }
impl Pred<i16>     for KindPredicate { /* the executable test */ }

ENUMERATED values are built on the verified i16 integer-content backend, which is why the predicate is over i16. Larger enumerations are currently not yet supported.

Mappers follow the DSL’s Forward/Reverse pattern, with one addition — they implement the executable Map as well as SpecMap.

pub struct KindForward;
pub struct KindReverse;

impl SpecMap for KindForward { /* .. */ }
impl SpecMap for KindReverse { /* .. */ }
impl Map<i16> for KindForward { /* executable */ }
impl Map<Kind> for KindReverse { /* executable */ }

The nominal format type

/// DER format for ASN.1 `Kind`.
type KIND__ = Mapped<Refined<Enumerated16TlvFmt, KindPredicate>, BiMap<KindForward, KindReverse>>;

#[derive(Clone, Copy)]
#[verifier::ext_equal]
pub struct KIND(pub Class, pub u64); // tag class, tag number

impl KIND {
    pub const Fmt: Self = Self(Class::Universal, 10u64);

    #[verifier::allow_in_spec]
    pub const fn schema() -> KIND__
        returns (Mapped { inner: Refined(ENUMERATED16, KindPredicate),
                          mapper: BiMap(KindForward, KindReverse) }),
    { /* the same representation */ }

    proof fn lemma_schema_unambiguous(&self) { /* .. */ }
}

Several things differ from the DSL here.

Tagged format types carry their effective tag. Unlike the zero-sized MessageFmt in our DSL example, KIND is a tuple struct holding the effective tag class and number, so an IMPLICIT tag can replace the outer tag without rebuilding the format. KIND::Fmt is the associated constant carrying the definition’s own tag — Class::Universal, 10 for ENUMERATED, 16 for SEQUENCE, etc. Untagged CHOICE and ANY format types are zero-sized instead: they have no single outer tag to store or replace.

schema() is dual spec-exec. The DSL’s spec_inner() is pub open spec fn — specification only. schema() here is a const fn marked #[verifier::allow_in_spec] with a returns clause, so the same definition serves both worlds (there are valid reasons for the DSL to separate them, such as to allow for more flexible executable implementations).

lemma_schema_unambiguous has no DSL counterpart. It proves the ASN.1 schema unambiguous (needed for serialize-then-parse roundtrip) by leveraging a sound over-approximation of each ASN.1 combinator’s parsing domain. On the other hand, the DSL’s constructs disambiguate themselves largely by construction, so the DSL does not need to emit this lemma.

Specifications, proofs, and executable code

Everything else arrives from one macro invocation, placed outside verus!:

mod __impl_packet {
    use super::*;
    vest_lib::impl_der!(
        tagged_exact(true),   // this definition contributes an outer tag
        borrowed,             // the value type borrows from the input
        PACKET, PACKET__,     // nominal type and its combinator type alias
        PacketSpec, Packet,   // abstract and executable value types
        PacketForward, PacketReverse
    );
}

Both macros implement the specification traits (SpecParser, SpecSerializer, SpecByteLen, Consistency), compositional proof traits (SafeParser, Productive, NonTailFmt, GoodSerializer, SPRoundTripDps, etc.), and executable APIs (Parser, Prepare, Serializer).

impl_der! additionally implements SoundParser, NonMalleable, and allocation-free DerOrd. impl_ber! deliberately omits those traits: BER may accept several encodings of the same logical value, with different lengths.

Calling it

Calling the parser, serializer, and the prepare methods is almost identical in shape to DSL-generated code, except that the format value is the ::Fmt constant:

use vest_lib::core::exec::{Parser, Prepare, SerializerExt};

let (consumed, packet) = PACKET::Fmt.parse(&encoded).unwrap();

let size = PACKET::Fmt.prepare(&packet).unwrap();
let mut output = vec![0u8; size];
PACKET::Fmt.serialize(&packet, &mut output);

Supported ASN.1 and limitations

What vest_asn1 accepts today. Anything listed as not supported is rejected by the compiler with an error.

Primitive types

Constructed types

Tagging

Components and constraints

Module-level

Additional notes

SET OF ordering. DER requires the values to be sorted by their complete DER TLV encoding. The generated prepare rejects an unsorted vector without allocating, so sorting is the caller’s job (the provided comparison abstraction is non-allocating so sorting should be efficient as well). Duplicate encodings are allowed. BER SET OF imposes no canonical order and writes values in their vector order.

Heterogeneous SET. BER lets a SET carry its components in any order, so a BER parser would have to accept every permutation of the fields. DER instead fixes them in ascending tag order. vest_asn1 currently emits SET only under DER, and only when the schema already lists the fields in canonical order. The vest_lib backend supports a group of Permute combinators that can be used to implement BER SET, but the generator does not yet emit them.

Borrowing and alloc. DER byte strings and UTF-8-compatible character strings borrow from the input. BER strings may arrive fragmented across constructed encodings and are flattened into owned values, which is why BER modules need the alloc feature where the equivalent DER module may not. BMPString and UniversalString are always owned, since their wire form is not UTF-8.

High tag numbers and disjointness. CHOICE, OPTIONAL, and DEFAULT need alternatives/adjacent fields to be provably disjoint. The generated proof covers the 256 possible leading identifier octets: tags 0 through 30 are exact, but all high-tag-number forms sharing a class and constructed bit collapse onto one bit. Two such tags cannot be proven disjoint from their later tag-number octets alone, so a schema that distinguishes alternatives only by high tag numbers is conservatively rejected.

General and deterministic CBOR

TODO. This page is not written yet.

vest_lib::cbor is a verified prototype codec for the RFC 8949 generic data model, covering both general well-formed CBOR and the deterministic profile. This page will cover the value model, the borrowing and allocation behaviour, and which parts of the deterministic profile are enforced today.

Until then, the cbor module documentation describes the formats and their proof interfaces.