Ordinateur

I Proved Leftpad

January 25, 2026

I’ve been orbiting around the concept of formal methods AKA formal verification AKA automated reasoning for a few years now. This year I’ve come up with a more concrete plan to study the topic from the ground up. When reading an early release of Hillel Wayne’s book Logic for Programmers, I learned about the project Let’s Prove Leftpad. The Verus verification framework has been a hot topic at work over the past year so I decided to give it a try on a fairly straightforward proof.

Leftpad Proof

use vstd::invariant;
use vstd::math::max;
use vstd::prelude::*;

verus! {
    // Trivial recursive implementation of leftpad 
    spec fn leftpad_spec(c: char, n: nat, s: Seq<char>) -> Seq<char>
        decreases n - s.len() // required to signal to Verus that this recursion terminates
    {
        if s.len() >= n {
            s
        } else {
            let next = leftpad_spec(c,(n - 1) as nat, s);
            next.insert(0, c)
        }
    }

    // Verifies each property is validated all the way down through the base case
    proof fn leftpad_proof(c: char, n: nat, s: Seq<char>)
        ensures
            result_has_correct_length(leftpad_spec(c, n, s), n, s),
            prefix_is_only_padded_characters(c, n, s, leftpad_spec(c, n, s)),
            suffix_is_original_string(c, n, s, leftpad_spec(c, n, s)),
        decreases
            n - s.len()
    {
        if s.len() < n {
            leftpad_proof(c, (n - 1) as nat, s)
        } else { }
    }

    // Verifies that the length of the output is max(n, len(str))
    spec fn result_has_correct_length(result: Seq<char>, n: nat, s: Seq<char>) -> bool {
        result.len() == max(n as int, s.len() as int)
    }

    // Verifies that the prefix of the output is padding characters and nothing but padding characters
    spec fn prefix_is_only_padded_characters(c: char, n: nat, s: Seq<char>, result: Seq<char>) -> bool {
        let pad_len = max(n as int - s.len() as int, 0);
        forall|i: int| 0 <= i < pad_len ==> result[i] == c
    }

    // Verifies that the suffix of the output is the original string.
    spec fn suffix_is_original_string(c: char, n: nat, s: Seq<char>, result: Seq<char>) -> bool {
        forall|i: int| 0 <= i < s.len() ==> result[max(n as int - s.len() as int, 0) + i] == s[i]
    }

    // Iterative implementation of leftpad
    exec fn leftpad_impl(c: char, n: usize, s: Vec<char>) -> (result: Vec<char>)
        ensures
            // verifies that the iterative implementation is equivalent to the proven recursive one
            result@ == leftpad_spec(c, n as nat, s@), 
    {
        let pad_length = n.saturating_sub(s.len());
        let mut idx = 0;
        let mut result = s;
        while idx < pad_length
            invariant
                0 <= idx <= pad_length,
                // checks the expected result before and after each iteration
                result@ == leftpad_spec(c, s@.len() + idx as nat, s@),
            decreases pad_length - idx
        {
            result.insert(0, c);
            idx = idx + 1;
        }
        result
    }
} // verus!

Takeaways

Admittedly, I would not have been able to implement this without reviewing the existing proofs in the leftpad repo. It’s been a number of years since I had to write a proof. What I appreciate about this implementation is the process of proving something simple and then connecting it to something slightly more complex. This reminds me of Gall’s law:

A complex system that works is invariably found to have evolved from a simple system that worked. A complex system designed from scratch never works and cannot be patched up to make it work. You have to start over with a working simple system.

I see this as a recurring theme. For example, my team at work has built a differential testing harness to validate that our production service produces the same output as our simplified model representation.

Next, I’ll be following some coursework I found online to learn some of the fundamentals about formal methods.