DEV Community: Prasanna Gautam

MiniLisp C++: A Compile-Time Lisp Interpreter in C++20

Prasanna Gautam — Fri, 26 Dec 2025 14:10:00 +0000

TL;DR : I built a Lisp interpreter that evaluates expressions at compile-time using C++20 constexpr. The same code works at runtime too—no duplication needed. Along the way, I discovered that macOS adds ~28KB of constant overhead to all C++ binaries, and that Mach-O is surprisingly more efficient than Linux ELF for small programs.

Try it right now — this runs the same interpreter compiled to WebAssembly (27KB):

Lisp Expression:
Eval

Result:

Loading WASM...

Try: (* 6 7) ·(car '(10 20 30)) ·(cdr '(1 2 3))

Some weeks back I saw that Dan Lemire had a PR open on simdjson that added an expression to parse whole JSON. That intrigued me and took the challenge to see if I could write a LISP Interpreter. Here’s a minimal godbolt playground if you’re interested to play around. I don’t have this problem as much anymore but I used to need a little DSLs in programs all the time. Maybe long term Lua is right choice but I can see something like this to be useful in a very small form factor like some kind of verified binary that you want to minimize your dependencies and adding a whole new lib will add more complexity.

The Magic: Compile-Time Lisp

Here’s what this looks like:

// This is evaluated by the compiler, not at runtime!
constexpr auto val = "(+ 10 (* 2 5))"_lisp;
static_assert(val == 20);
constexpr auto head = "(car '(10 20 30))"_lisp;
static_assert(head == 10);

If the Lisp expression is invalid, your code won’t compile. The compiler becomes your Lisp interpreter.

Why This Matters

Catch errors at compile time - Invalid Lisp expressions fail during build, not at 3 AM in production
Zero runtime cost - The result is baked directly into the binary
Type safety - The compiler verifies your Lisp code before you ship

The C++20 Features That Make This Possible

C++20 made compile-time programming dramatically more powerful:

constexpr everything - Vectors, algorithms, and even memory allocation now work at compile-time
User-defined literals - The _lisp suffix creates elegant syntax
std::variant - Type-safe unions for representing S-expressions
std::span - Zero-copy parameter passing for operand lists
consteval - Forces compile-time-only evaluation

Implementation Highlights

The interpreter is built on a few key components:

FixedString - A template struct that captures string literals at compile-time:

template <size_t N>
struct FixedString {
char data[N];
consteval FixedString(const char (&str)[N]) {
std::copy(str, str + N, data);
}
constexpr std::string_view get() const {
return std::string_view(data, N - 1);
}
};

S-Expression Types - The classic Lisp data structures:

// An "Atom" is either a number or a symbol
using Atom = std::variant<long, std::string_view>;
// A "List" is a vector of S-Expressions
using List = std::vector<SExpr>;
// An S-Expression is either an Atom or a List
struct SExpr {
std::optional<Atom> atom;
std::optional<List> list;
};

The User-Defined Literal - The magic entry point:

template <FixedString S>
consteval auto operator""_lisp() {
std::string_view s = S.get();
auto ast = MiniLisp::parse(s);
auto result_sexpr = MiniLisp::eval(ast);
// Extract and return the final long value
return std::get<long>(*result_sexpr.atom);
}

Functional Arithmetic - Using std::transform_reduce for clean, constexpr-compatible operations:

if (op == "+") {
long result = std::transform_reduce(
operands.begin(), operands.end(),
0L, // Initial value
std::plus<long>(), // Reduce operation
[](const SExpr& e) { return get_long(e); } // Transform
);
return SExpr{Atom{result}};
}

Comparison with Other Approaches

Approach	Example	Pros	Cons
Runtime OOP	ofan’s Lisp	Simple, ~200 lines	Runtime only
Template metaprogramming	Crisp, Templisp	Compile-time	Ugly syntax, hard to debug
constexpr (this project)	minilisp-cpp	Clean, dual-mode, debuggable	Requires C++20

The ofan gist shows a classic runtime interpreter in ~200 lines of clean C++. But with C++20 constexpr, we get the same readable code that also works at compile time —that’s the key insight.

Extending the Interpreter

Adding new functions is straightforward. Here’s how to add a max function:

else if (op == "max") {
p_assert(!operands.empty(), "'max' requires at least one argument");
long result = get_long(operands[0]);
for (size_t i = 1; i < operands.size(); ++i) {
long val = get_long(operands[i]);
if (val > result) result = val;
}
return SExpr{Atom{result}};
}

This automatically works at both compile-time and runtime—no extra effort needed.

The Binary Size Deep Dive

While optimizing the interpreter for size, I learned two lessons that would have saved me hours if I’d known them upfront.

Lesson 1: Know When to Stop

After applying every optimization I could find, the macOS binary sat stubbornly at 34KB. I spent time trying to squeeze out more bytes before realizing: 34KB is the floor. On macOS, the Mach-O binary format has ~28KB of unavoidable overhead. Once you hit that limit, further code optimization is wasted effort.

Lesson 2: Measure the Right Thing

File size (ls -l) is misleading—it’s dominated by format overhead you can’t control. What you can control is actual code size, measured with the size command. My real win was a 32% reduction in executable code (10.7KB → 7.3KB), even though the file size barely budged.

Build Configurations

Build	macOS	Linux	WASM	Techniques
Default	39KB	-	-	`-O2`
Small	36KB	-	-	`-Os`, LTO, strip
Ultra-small	34KB	66KB (10KB UPX)	27KB	POSIX I/O, no iostream, wasm-opt

What We Actually Removed

Here’s the real code reduction (measured with size):

DEFAULT BUILD (with iostream):
Code section: 8,484 bytes
Exception tables: 844 bytes
Total code: 10,753 bytes
ULTRA-SMALL BUILD (POSIX I/O):
Code section: 5,752 bytes (32% reduction!)
Exception tables: 288 bytes (66% reduction!)
Total code: 7,273 bytes (32% reduction!)

The techniques:

Replace <iostream> with POSIX write()/read()
Replace std::string with fixed buffers
Simplify exception handling

Build flags: -Os -flto -fno-rtti -ffunction-sections -fdata-sections -Wl,-dead_strip

Why macOS Has a 34KB Floor

Let’s dig into why you can’t go below 34KB on macOS—understanding this saves you from chasing impossible optimizations.

Mach-O Segment Layout

Running size -m lisp_repl reveals the structure:

Segment __PAGEZERO: 4294967296 (4GB virtual, catches NULL pointers)
Segment __TEXT: 16384 (contains ~7KB code + padding)
Segment __DATA_CONST: 16384 (contains 328 bytes + padding)
Segment __LINKEDIT: varies (symbols, code signature)

Full output of `size -m lisp_repl`

Segment __PAGEZERO: 4294967296 (zero fill)
Segment __TEXT: 16384
Section __text: 8484
Section __stubs: 336
Section __gcc_except_tab: 844
Section __cstring: 737
Section __unwind_info: 352
total 10753
Segment __DATA_CONST: 16384
Section __got: 328
total 328
Segment __LINKEDIT: 16384
total 4295016448

The key insight : Mach-O uses 16KB segment alignment. Each segment must start on a 16KB boundary, so even tiny segments consume 16KB of disk space.

3 on-disk segments × 16KB = ~48KB baseline
After strip: ~34KB (removes some __LINKEDIT)

This means 34KB is essentially the floor for any C++ program on macOS —even “hello world” is ~33KB.

The Counter-Intuitive Comparison

Metric	macOS Mach-O	Linux ELF
Stripped size	35,016 bytes	67,952 bytes
Actual code (text)	~7KB	~11KB
Format overhead	~28KB	~56KB
Page alignment	16KB	4KB

Despite 16KB pages, Mach-O is MORE efficient than ELF!

Why ELF is larger:

More section headers and metadata
Debug info remnants even after strip
Symbol table overhead

Inspecting Your Own Binaries

# macOS - see segment sizes
size -m your_binary
# macOS - detailed Mach-O structure
otool -l your_binary | grep -A5 "segname"
# Linux - section sizes
size your_binary
# Linux - detailed sections
readelf -S your_binary

The UPX Factor (Linux Only)

UPX (Ultimate Packer for eXecutables) compresses binaries:

Algorithm	Size	Compression
Uncompressed	67,952 bytes	-
UPX NRV (default)	10,288 bytes	85% reduction
UPX LZMA	11,528 bytes	83% reduction

NRV beats LZMA for small binaries by 11%! This surprised me—I expected LZMA to always win.

Why not macOS?

UPX is officially unsupported for Mach-O
Code signing conflicts with compressed binaries
--force-macos often causes segfaults

WebAssembly Build

The interpreter also compiles to WebAssembly, producing a 27KB binary after optimization.

wasi-sdk vs Emscripten

I chose wasi-sdk over Emscripten for one reason: no JavaScript bloat.

Toolchain	Output Size	What You Get
wasi-sdk + wasm-opt	27KB	Single `.wasm` file
Emscripten	100KB+	`.wasm` + JavaScript runtime

Emscripten provides a full POSIX-like environment with filesystem emulation. For a simple eval function, that’s overkill. wasi-sdk produces a minimal WASI-compliant binary that only needs stub implementations for a handful of syscalls.

Build Flags

# Compile with wasi-sdk
clang++ -std=c++20 -Os -fno-exceptions -Wl,--no-entry -Wl,--export-dynamic
# Optimize with wasm-opt (from Binaryen)
wasm-opt -Oz --strip-debug --strip-producers lisp.wasm -o lisp.wasm

Key choices:

-fno-exceptions - Errors via __builtin_trap(), reduces binary size
-Wl,--export-dynamic - Export the eval function for JS access
-Wl,--no-entry - Library mode, no main()

wasm-opt Optimization

Stage	Size	Reduction
After wasi-sdk compile	33KB	—
After wasm-opt -Oz	33KB	~0% (already optimized)
After –strip-debug	28KB	15%
After –strip-producers	27KB	18% total

The -Oz flag alone doesn’t help much since wasi-sdk already optimizes well, but stripping debug info and producer metadata saves ~6KB.

Try It Yourself

Clone and Build

git clone https://github.com/prasincs/minilisp-cpp
cd minilisp-cpp
# Default build
make
# Size-optimized
make small
# Ultra-small (POSIX I/O)
make ultra-small

Verify Compile-Time Evaluation

The static_assert statements in main.cpp prove compile-time evaluation works:

constexpr auto val = "(+ 10 (* 2 5))"_lisp;
static_assert(val == 20); // Fails to compile if wrong!
constexpr auto val3 = "(car '(10 20 30))"_lisp;
static_assert(val3 == 10);

Try introducing an error—the compiler will catch it:

// This fails at compile time with a parse error
constexpr auto bad = "(+ 1"_lisp;

Cross-Compile for Linux (from macOS)

./build-linux.sh
# Uses Docker to build Linux ARM64 binary
# Shows size comparison automatically

Measure Binary Sections

# macOS
size -m lisp_repl
otool -l lisp_repl | grep -A5 "segname"
# Linux
size lisp_repl
readelf -S lisp_repl

Key Takeaways

On binary size optimization:

Know when to stop - macOS has a ~34KB floor due to Mach-O format overhead. Once you hit it, further code optimization is wasted effort.
Measure actual code size - Use size, not ls -l. File size is dominated by format overhead; code size is what you can control.
iostream is expensive - Removing it saved 32% of actual executable code. If size matters, use POSIX I/O.

On C++20:

constexpr is powerful - A full Lisp interpreter at compile time in readable code
Same code, dual modes - No template metaprogramming gymnastics required

Conclusion

Building a compile-time Lisp interpreter turned out to be a journey through modern C++ and binary format archaeology. The compile-time evaluation is genuinely useful for catching errors early, but the binary size investigation taught me more about platform-specific behavior than I expected.

The source code is available at github.com/prasincs/minilisp-cpp, as well as a standalone playground. Try adding new operations—they’ll automatically work at both compile-time and runtime.

Sometimes the journey of optimization teaches more than the destination.

Neovim for Blog Writing: Plugins, Keymaps, and a Cheatsheet

Prasanna Gautam — Fri, 26 Dec 2025 13:25:00 +0000

My Neovim config has always been coding-focused—LSP, treesitter, language-specific keymaps for Zig, Rust, and Go. But I recently wanted to use the same setup for writing blog posts. Here’s what I added to make Neovim a solid prose environment.

The full config is at github.com/prasincs/vim-config.

Writing-Focused Plugins

Zen Mode

zen-mode.nvim removes distractions by centering your buffer and hiding UI elements.

{
"folke/zen-mode.nvim",
opts = {},
keys = {
{ "<leader>z", "<cmd>ZenMode<cr>", desc = "Zen Mode" },
},
},

Press <Space>z to toggle. The buffer centers itself, line numbers fade, and you’re left with just your text.

The screenshot below shows what zen-mode looks like

Twilight

twilight.nvim dims inactive portions of your file. When combined with Zen Mode, it auto-activates to keep your focus on the current paragraph.

{
"folke/twilight.nvim",
opts = {},
},

The screenshot above also shows the dimming.

Render Markdown

render-markdown.nvim renders markdown decorations directly in the buffer—headings get background colors, code blocks are highlighted, lists show proper bullets.

{
"MeanderingProgrammer/render-markdown.nvim",
dependencies = { "nvim-treesitter/nvim-treesitter", "nvim-tree/nvim-web-devicons" },
ft = { "markdown" },
opts = {},
keys = {
{ "<leader>mr", "<cmd>RenderMarkdown toggle<cr>", desc = "Toggle markdown rendering" },
},
},

Press <Space>mr to toggle rendering on/off. This is optional if you’re using Hugo’s live server for previews—sometimes the raw markdown is easier to edit.

This was a big new and confusing to me, so here’s a helper

Markdown Configuration

Treesitter Parsers

Add markdown and markdown_inline to your treesitter config for proper syntax highlighting:

{
"nvim-treesitter/nvim-treesitter",
opts = {
ensure_installed = { "markdown", "markdown_inline", --[[other languages]] },
},
},

Prose-Friendly Settings

Markdown files need different settings than code. This autocmd enables word wrap, spell checking, and hides markdown syntax:

vim.api.nvim_create_autocmd("FileType", {
pattern = "markdown",
callback = function()
vim.opt_local.wrap = true
vim.opt_local.linebreak = true
vim.opt_local.spell = true
vim.opt_local.conceallevel = 2
end,
})

wrap + linebreak: Text wraps at word boundaries instead of mid-word
spell: Highlights misspellings (use z= to see suggestions)
conceallevel = 2: Hides markdown syntax like **bold**, showing just bold

Adding Images and Screenshots

One friction point in markdown blogging is adding images. You either need to manually copy files and write the markdown tag, or leave Neovim entirely. I added helpers to streamline this.

Setup: pngpaste

For clipboard paste support on macOS, you need pngpaste. I use my fork with error handling:

git clone -b error-handling https://github.com/prasincs/pngpaste.git
cd pngpaste
make && sudo make install

Or use the original via Homebrew: brew install pngpaste

Image Helper Functions

The config auto-detects your images directory (static/images, assets/images, etc.) and provides three ways to add images:

Action	Keymap/Command
Paste from clipboard	`<Space>mi`
Paste with custom name	`<Space>mn`
Insert from file path	`<Space>mI`
Insert via command	`:MarkdownInsertImage ~/path/to/image.png`

When you paste, it:

Saves the clipboard image to static/images/screenshot-YYYYMMDD-HHMMSS.png
Inserts ![screenshot-YYYYMMDD-HHMMSS](/static/images/screenshot-YYYYMMDD-HHMMSS.png) at cursor

The :MarkdownInsertImage command copies an external file into your images directory and inserts the tag—useful for images from Downloads or other projects.

Screen Recordings

For screen recordings, there’s a dedicated workflow that converts videos to GIF automatically:

Action	Keymap
Fuzzy find recording from Desktop	`<Space>mR`
Insert via command	`:MarkdownInsertRecording <path> <name>`

The search directories are configurable:

local markdown_media_config = {
image_search_dir = "~/Downloads", -- Where to search for images with <Space>mI
recording_search_dir = "~/Desktop", -- Where to search for recordings with <Space>mR
image_search_depth = 2, -- How deep to search for images
recording_search_depth = 1, -- How deep to search for recordings
}

The <Space>mR keymap opens Telescope filtered to video files (.mov, .mp4, .webm) in your configured directory—~/Desktop by default, where macOS saves screen recordings.

The command handles spaces in filenames naturally:

:MarkdownInsertRecording ~/Desktop/Screen Recording 2025-12-26 at 4.52.47 AM.mov my-demo

The last word without / is treated as the output name, everything before it is the path. This converts the video to GIF using ffmpeg and inserts the markdown tag.

For static images, the keymaps use Telescope for fuzzy finding:

Action	Keymap
Fuzzy find image	`<Space>mI`
Paste from clipboard	`<Space>mi`
Paste with custom name	`<Space>mn`

AI-Assisted Writing with Claude Code

I use claudecode.nvim for AI assistance while writing. It integrates Claude directly into Neovim.

{
"coder/claudecode.nvim",
dependencies = { "folke/snacks.nvim" },
opts = {
terminal_cmd = vim.fn.expand("~/.claude/local/claude"),
},
keys = {
{ "<leader>ac", "<cmd>ClaudeCode<cr>", desc = "Toggle Claude" },
{ "<leader>af", "<cmd>ClaudeCodeFocus<cr>", desc = "Focus Claude" },
{ "<leader>as", "<cmd>ClaudeCodeSend<cr>", mode = "v", desc = "Send to Claude" },
{ "<leader>ab", "<cmd>ClaudeCodeAdd %<cr>", desc = "Add current buffer" },
},
},

Select text, hit <Space>as, and Claude sees your selection. Useful for rephrasing paragraphs or getting feedback on technical explanations.

Cheatsheet

Starting a Writing Session

Action	Keymap
Open file finder	`<Space>ff`
Toggle Zen Mode	`<Space>z`
Toggle file tree	`<Space>e`
Toggle markdown rendering	`<Space>mr`

Navigating Content

Action	Keymap
Search in files	`<Space>fg`
Switch buffers	`<Space>fb`

Editing

Action	Keymap
Move line down	`J` (visual mode)
Move line up	`K` (visual mode)
Yank to clipboard	`<Space>y`
Toggle comment	`gc`

AI Assistance

Action	Keymap
Toggle Claude	`<Space>ac`
Send selection to Claude	`<Space>as` (visual)
Add buffer as context	`<Space>ab`

Spell Checking

Action	Keymap
Next misspelling	`]s`
Previous misspelling	`[s`
Suggest corrections	`z=`
Add word to dictionary	`zg`

Images & Recordings

Action	Keymap
Paste image from clipboard	`<Space>mi`
Paste with custom name	`<Space>mn`
Fuzzy find image from home	`<Space>mI`
Fuzzy find recording from Desktop	`<Space>mR`

Conclusion

This setup gives me distraction-free writing with in-buffer markdown rendering, spell checking, and AI assistance—all without leaving Neovim.

It’s been over a decade since I wrote about Perfect Vim Setup for Go. The tooling has evolved dramatically, but the core idea remains: configure your editor to fit how you work.

Full config: github.com/prasincs/vim-config

Don't Unwrap in Production: A Formal Verification Guide

Prasanna Gautam — Thu, 25 Dec 2025 06:13:04 +0000

TL;DR : On November 18, 2025, a single .unwrap() call caused a 3-hour global Cloudflare outage. Formal verification tools like Verus could have caught this at compile time—before it reached production. This post shows how Verus’s built-in specifications for Option::unwrap() and Result::unwrap() can mathematically prove panic-freedom, with working examples you can run today.

The Bug

On November 18, 2025, Cloudflare experienced a 3-hour global outage. The root cause? A panic in Rust code:

const MAX_FEATURES: usize = 200;
fn load_bot_features(file_path: &Path) -> Result<BotFeatures, Error> {
// 💥 PANIC: parse_feature_file can return Err, but we unwrap anyway
let features = parse_feature_file(file_path).unwrap();
if features.len() > MAX_FEATURES {
return Err(Error::TooManyFeatures); // Never reached!
}
BotFeatures { features }
}

What went wrong:

The developer knew the file size mattered and wrote a check: if features.len() > MAX_FEATURES.
However, they placed this check after the unwrap().
When the config file accidentally doubled in size during deployment, parse_feature_file failed internally (returning Err) due to buffer limits.
The .unwrap() triggered immediately.
The manual safety check was dead code—it was never reached.

The frustrating part: This code looked safe. It had error handling below. It passed code review. It had tests. But the .unwrap() was in the wrong place.

Here’s how Verus would have caught this at compile time.

How Verus Catches This

❌ Unsafe Version (Cloudflare’s Bug)

fn load_bot_features(file_path: &Path) -> Result<BotFeatures, Error> {
let features = parse_feature_file(file_path).unwrap(); // 💥
if features.len() > MAX_FEATURES {
return Err(Error::TooManyFeatures);
}
Ok(BotFeatures { features })
}

Verus output:

error: precondition not satisfied
--> src/bot_manager.rs:42:52
|
42 | let features = parse_feature_file(file_path).unwrap();
| ^^^^^^^^
|
= note: cannot prove `parse_feature_file(file_path).is_Ok()`
= help: unwrap() requires proof that Result is Ok

Translation: “I cannot prove this won’t panic. Fix it or I won’t compile.”

✅ Safe Version (Verus-Approved)

Option 1: Proper error propagation

fn load_bot_features(file_path: &Path) -> Result<BotFeatures, Error> {
let features = parse_feature_file(file_path)?; // ✅ Propagate error
if features.len() > MAX_FEATURES {
return Err(Error::TooManyFeatures);
}
Ok(BotFeatures { features })
}

Option 2: Explicit proof

fn load_bot_features(file_path: &Path) -> Result<BotFeatures, Error> {
let result = parse_feature_file(file_path);
if result.is_ok() {
let features = result.unwrap(); // ✅ Verus proves: is_ok() → unwrap() safe
if features.len() > MAX_FEATURES {
return Err(Error::TooManyFeatures);
}
Ok(BotFeatures { features })
} else {
Err(Error::ParseFailed)
}
}

Verus output: ✅ Verification successful

But how does Verus know .unwrap() is safe after an is_ok() check? The answer lies in Verus’s built-in specifications.

How Verus Works: Built-In Proofs for Unwrap Safety

Verus is a formal verification tool for Rust developed at CMU and VMware Research. It leverages Rust’s ownership system and uses SMT solvers to prove panic-freedom.

The Secret Sauce: Unwrap Is Conditionally Safe

Here’s the key insight—Verus already knows that .unwrap() is safe if and only if you have Some or Ok:

Option::unwrap() specification (source):

impl<T> Option<T> {
#[verifier::external_body]
pub fn unwrap(self) -> T
requires self.is_Some(), // ← MUST prove this!
{
// ...
}
}

Result::unwrap() specification (source):

impl<T, E> Result<T, E> {
#[verifier::external_body]
pub fn unwrap(self) -> T
requires self.is_Ok(), // ← MUST prove this!
{
// ...
}
}

What this means:

✅ If Verus can prove option.is_Some() → .unwrap() is safe
✅ If Verus can prove result.is_Ok() → .unwrap() is safe
❌ If Verus cannot prove it → Compilation fails

No runtime overhead. No test coverage gaps. Just mathematical certainty.

Now that you’ve seen how Verus works, let’s try it yourself.

Working Examples You Can Try Today

I’ve created a repository with runnable Verus examples showing panic detection in practice:

🔗 formal-verification-experiments/verus

Examples included:

Array bounds checking
Division by zero
Integer overflow
Option/Result unwrapping

Each example shows:

The unsafe version (Verus rejects)
The safe version (Verus approves)
The exact verification error message
How to fix it

How to run:

# Install Verus
git clone https://github.com/verus-lang/verus.git
cd verus && ./tools/get-z3.sh && source ./tools/activate
# Clone examples
git clone https://github.com/prasincs/formal-verification-experiments.git
cd formal-verification-experiments/verus
# Verify examples
verus examples/panic_detection.rs
# See it catch bugs
verus examples/unsafe_unwrap.rs # ❌ Fails verification
verus examples/safe_unwrap.rs # ✅ Passes verification

The Developer Experience: VSCode Integration

Formal verification used to mean batch runs and cryptic error messages. Not anymore.

Verus VSCode extension provides real-time feedback:

Instant verification : See errors as you type (like clippy)
Inline diagnostics : Red squiggles under unsafe code
Helpful messages : “Cannot prove i < bytes.len()”
Counterexamples : Verus often shows the exact input that would cause panic

Example workflow:

fn parse_first_byte(bytes: &[u8]) -> u8 {
bytes[0] // ⚠️ Red squiggle appears immediately
}

Hover over the warning:

❌ Verification failed
Cannot prove: 0 < bytes.len()
Counterexample: bytes = []
Suggestion: Add `requires bytes.len() > 0`

Fix it:

fn parse_first_byte(bytes: &[u8]) -> u8
requires bytes.len() > 0
{
bytes[0] // ✅ Green checkmark
}

This is a game-changer. You don’t run verification in CI and wait 20 minutes. You get instant feedback, right in your editor , as you write code.

What Verus Doesn’t Prove (And Why That’s OK)

Let’s be honest about limitations:

❌ Verus does NOT prove:

Business logic correctness
Performance
Liveness (yet)
Full functional correctness (unless you specify it)

✅ What Verus DOES prove:

Panic-freedom : No unwrap/bounds/overflow/div-by-zero panics
Memory safety : Already guaranteed by Rust, but Verus can verify unsafe code too
Custom invariants : You can prove application-specific properties

The key insight: Even proving just panic-freedom is hugely valuable. Studies show:

~40% of production outages involve panics, crashes, or overflows
Cloudflare : 3-hour outage from single unwrap
Ethereum : $150M+ lost to integer overflow (The DAO hack, 2016)
Knight Capital : $440M loss from uncaught exception (2012)

Eliminating 40% of outages is not “just” anything.

When Should You Use Verus?

✅ Use Verus when:

Parsing untrusted input
Arithmetic on money/tokens
Safety-critical code
High-leverage code
Compliance requirements

*Important note: seL4’s verified kernel has had zero vulnerabilities, but the broader ecosystem (musllibc, userspace) has had bugs like CVE-2020-28928. Lesson: Formal verification only covers what you verify, not dependencies.

❌ Skip Verus when:

Prototyping
Rapid iteration
Glue code / scripts
You already have robust testing

Decision Tree:

flowchart TD
A[Is this code safety-critical<br/>or high-leverage?] -->|No| B[Skip Verus<br/>use tests]
A -->|Yes| C[Can bugs cause outages<br/>or financial loss?]
C -->|No| D[Skip Verus<br/>use tests]
C -->|Yes| E[Is the codebase stable?]
E -->|No| F[Wait, use tests for now]
E -->|Yes| G[Use Verus]

This also matches the approach that Amazon AWS has adopted called Verification Guided Development in the talk by Mark Hicks where they first require properties to be documented and verified by using Property-based Testing and then once this is verified, a mathematical proof starts to make sense.

Comparison: Other Rust Verification Tools

Verus isn’t the only game in town:

Tool	Approach	Best For	Maturity	Backed By
Verus	SMT-based	Systems code, panic-freedom	2 OSDI Best Papers 2024	CMU, VMware
Kani	Bounded model checking	Unsafe code, bit-level	Production-ready	AWS
Prusti	Viper backend	Safe Rust, functional correctness	Research-grade	ETH Zurich
Creusot	Why3 backend	Algorithms, faster verification	Research-grade	Inria

Quick guide:

Verifying unsafe code? → Kani
Proving algorithms correct? → Creusot or Prusti
Preventing production panics? → Verus
Multiple tools? → They’re complementary, not exclusive

Real-World Success Stories

1. OSDI 2024 Best Papers (Both Used Verus)

Anvil: Verified liveness properties in Kubernetes controllers

Found bugs in real production controllers
Proved they can’t deadlock or livelock

VeriSMo: Verified security module for confidential VMs

Found security bug in AMD SVSM
Proved memory isolation properties

Both papers used Verus. Both won Best Paper. This isn’t theory—it’s validated research.

2. IronFleet (Microsoft Research, 2015)

Verified distributed systems (Paxos, chain replication):

100x fewer bugs than unverified implementations
Proved safety and liveness properties
Paper: SOSP 2015

3. Amazon Web Services (Ongoing)

From “How Amazon Web Services Uses Formal Methods”:

“We have used TLA+ on 10 large complex real-world systems. In every case, it has found bugs.”

Different tool (TLA+), same principle: Proofs catch bugs testing misses. Amazon has also built Dafny Programming Language that builds static verification into the development process.

4. Asterinas OS (December 2025)

Verified page table implementation in general-purpose OS using Verus:

Proved memory safety properties
Showed Verus scales to OS-level code
Blog: Asterinas Formal Verification

With this growing adoption, the question becomes: what’s driving the timing?

The AI Connection: Why Now?

Martin Kleppmann (author of Designing Data-Intensive Applications) made a bold prediction in December 2025:

“Prediction: AI will make formal verification go mainstream.”

His argument:

LLMs are good at proof scripts (formal reasoning)
Hallucinations don’t matter (proof checker rejects invalid proofs)
AI + Verus = powerful combo (human intent + machine rigor)

Early evidence:

ChatGPT/Claude can write Verus annotations (with guidance), in fact Claude helped me write and validate lot of examples in this blog post.
GitHub Copilot learns from verified code
Proof assistants are a perfect fit for LLMs (discrete, verifiable output)

My take:

Promising, not proven (as of Dec 2025)
Current AI helps with boilerplate annotations
Still need human expertise for complex proofs
But the trajectory is clear: AI lowers the barrier to entry

Think of it like this:

2015: Write proofs by hand (PhD required)
2024: Verus + VSCode (expert-friendly)
2025+: Verus + AI + VSCode (accessible to senior engineers)

We’re not there yet, but we’re getting close.

The ROI Question: Is It Worth It?

Cost of Verification

Time investment:

Learning curve: 1-2 weeks to basic proficiency
Annotation overhead: +10-30% development time (initially)
Refactoring: Proofs need updates when code changes

When it pays off:

Code with long lifespan (>1 year in production)
High-blast-radius bugs (outages affect millions)
Financial or safety-critical systems

Cost of NOT Verifying

Let’s do the math for Cloudflare:

Conservative estimate:

Outage duration: 3 hours
Revenue impact: ~$1.2M (based on $1.5B annual revenue)
Reputation damage: Priceless (trust erosion)
Engineer time: 50+ engineers × 3 hours = 150 engineer-hours
Incident response, postmortem, fixes: Another 200 hours
Total visible cost: $1.2M+ revenue + 350 hours

What if they’d used Verus?

Time to annotate load_bot_features: 15 minutes
Compilation would have failed: “Cannot prove unwrap is safe”
Fix: Change .unwrap() to ?: 30 seconds
Total cost: 15.5 minutes

ROI: $1.2M / 15 minutes = $4,645 per minute of verification time.

Even if verification added 50 hours to their development cycle, the ROI is absurd.

The Boring Case For Verification

Forget Cloudflare. Here’s the boring truth:

Formal verification is insurance.

You pay a small premium (development time) to avoid catastrophic loss (outages). Just like:

Fire insurance: Hope you never need it, but worth it
Backups: Boring, essential, pays off when disaster strikes
Tests: Everyone does them, verification is the next level

Who benefits most:

Infrastructure companies (Cloudflare, AWS, Datadog)
Blockchain/crypto (The DAO: $150M lost to overflow)
Financial services (Knight Capital: $440M lost to exception)
Medical devices, aerospace (FDA/FAA requirements)

If your company’s revenue depends on uptime, verification isn’t optional—it’s actuarial.

Criticisms and Rebuttals

“This is cherry-picking—one outage doesn’t prove anything”

Fair point. Let’s look at the data:

Study: “Simple Testing Can Prevent Most Critical Failures” (OSDI 2014)

Analyzed 198 production failures
77% could be prevented by checking error codes
40% involved uncaught exceptions or panics

Translation: Verus-level checks could prevent ~40% of major outages.

Is 40% worth it? You decide. But it’s not cherry-picking.

“Formal verification slows down development”

True… initially.

Learning curve:

Week 1-2: Frustrating (proofs don’t go through)
Week 3-4: Productive (patterns emerge)
Month 2+: Faster (proofs guide refactoring)

Long-term benefit:

Proofs act as executable documentation
Refactoring is safer (proofs break if you violate invariants)
Bugs caught at compile time, not in production

Think of it like types:

Initially: “Why do I need to annotate types? Just use any!”
Later: “Types caught 10 bugs before I even ran the code.”

Verification is types for behavior , not just data.

“Too immature / unproven”

I have believed for over 10 years since I first came across Isabelle proof that the grind of writing provers is what prevents us from adopting these methods for more safety critical systems.

Counter evidence:

seL4: 15 years in production, zero vulnerabilities in verified code
IronFleet: Deployed at Microsoft (2015)
Amazon: Uses TLA+ for 10+ years
Verus: 2 OSDI Best Papers (2024)

“Unproven” was true in 2015. Not anymore.

Getting Started: A Practical Path

Phase 1: Experiment (1-2 weeks)

Install Verus :
Try the examples :

I wrote the run script to build the container and run the commands so that it only takes time once and not potentially wreck your workstation.

Read the tutorial : Verus Guide
Install VSCode extension : verus-analyzer [YMMV but I had to stop rust-analyzer extension to get verus-analyzer to run]

Phase 2: Low-Hanging Fruit (2-4 weeks)

Pick one small, high-value module in your codebase:

Arithmetic with financial values
Parsing untrusted input
Array/slice indexing

Goal: Verify one function. Get the workflow down.

Phase 3: Expand (Ongoing)

Once you’ve verified one module:

Expand to related functions
Document patterns that work
Train team members
Integrate into CI (optional)

Phase 4: Cultural Shift (6+ months)

Formal verification becomes part of code review:

“Did you verify this panic path?”
“Can we prove this array access is safe?”
Proofs as first-class artifacts

Conclusion: The Future Is Verified

Here’s what we know:

Panics cause real outages (Cloudflare: 3 hours, millions affected)
Testing alone isn’t enough (Cloudflare had tests, code review, staging)
Verus can prove panic-freedom (mathematical certainty, not probabilistic)
Built-in proofs make it practical (Option/Result unwrap safety is already specified)
Tooling is maturing (VSCode integration, instant feedback)
ROI is compelling (15 minutes of verification vs. $1.2M outage)

The question isn’t:

“Should formal verification replace testing?” (No.)
“Is verification perfect?” (No—it only proves what you verify.)

The question is:

“For my critical code paths, is 99.9% confidence (testing) enough?”
“Or do I need 100% certainty (proof)?”

For Cloudflare’s bot detection? They needed proof. For seL4’s kernel? They needed proof. For your config parser that crashes production? Maybe you need proof too.

Resources

Try It Yourself

Examples repo: formal-verification-experiments/verus
Verus tutorial: Getting Started
VSCode extension: verus-analyzer

Papers

Verus: Verifying Rust Programs using Linear Ghost Types (OOPSLA 2023, SOSP 2024)
Anvil: Verifying Liveness of Cluster Management Controllers (OSDI 2024 Best Paper)
VeriSMo: A Verified Security Module for Confidential VMs (OSDI 2024 Best Paper)

Incident Reports

Other Perspectives

Acknowledgments

CMU and VMware Research for developing Verus
Cloudflare for transparent incident reporting
Martin Kleppmann for bringing formal methods’ potential into forefront
The Rust community for building memory-safe foundations

Corrections? Open an issue or PR on the examples repo. I’m still learning about this tool and limitations, so I am happy to get educated here.

Published: December 2025Last Updated: December 2025

DEV Community: Prasanna Gautam

MiniLisp C++: A Compile-Time Lisp Interpreter in C++20

The Magic: Compile-Time Lisp

Why This Matters

The C++20 Features That Make This Possible

Implementation Highlights

Comparison with Other Approaches

Extending the Interpreter

The Binary Size Deep Dive

Lesson 1: Know When to Stop

Lesson 2: Measure the Right Thing

Build Configurations

What We Actually Removed

Why macOS Has a 34KB Floor

Mach-O Segment Layout

Full output of size -m lisp_repl

The Counter-Intuitive Comparison

Inspecting Your Own Binaries

The UPX Factor (Linux Only)

WebAssembly Build

wasi-sdk vs Emscripten

Build Flags

wasm-opt Optimization

Try It Yourself

Clone and Build

Verify Compile-Time Evaluation

Cross-Compile for Linux (from macOS)

Measure Binary Sections

Key Takeaways

Conclusion

Neovim for Blog Writing: Plugins, Keymaps, and a Cheatsheet

Writing-Focused Plugins

Zen Mode

Twilight

Render Markdown

Markdown Configuration

Treesitter Parsers

Prose-Friendly Settings

Adding Images and Screenshots

Setup: pngpaste

Image Helper Functions

Screen Recordings

AI-Assisted Writing with Claude Code

Cheatsheet

Starting a Writing Session

Navigating Content

Editing

AI Assistance

Spell Checking

Images & Recordings

Conclusion

Don't Unwrap in Production: A Formal Verification Guide

The Bug

How Verus Catches This

❌ Unsafe Version (Cloudflare’s Bug)

✅ Safe Version (Verus-Approved)

How Verus Works: Built-In Proofs for Unwrap Safety

The Secret Sauce: Unwrap Is Conditionally Safe

Working Examples You Can Try Today

Examples included:

How to run:

The Developer Experience: VSCode Integration

What Verus Doesn’t Prove (And Why That’s OK)

❌ Verus does NOT prove:

✅ What Verus DOES prove:

When Should You Use Verus?

✅ Use Verus when:

❌ Skip Verus when:

Decision Tree:

Comparison: Other Rust Verification Tools

Real-World Success Stories

1. OSDI 2024 Best Papers (Both Used Verus)

2. IronFleet (Microsoft Research, 2015)

3. Amazon Web Services (Ongoing)

4. Asterinas OS (December 2025)

The AI Connection: Why Now?

The ROI Question: Is It Worth It?

Cost of Verification

Cost of NOT Verifying

The Boring Case For Verification

Full output of `size -m lisp_repl`