TL;DR

nelli is a testing library for Nim. It started as a property-based tester, but the architecture underneath it (a choice-sequence engine, the same idea behind Python’s Hypothesis) turned out to generalize far past property testing. Because a test input is nothing more than a recorded sequence of typed primitive choices, the same engine drives property testing, coverage-guided fuzzing, and SMT-backed symbolic execution, plus a stack of verification techniques on top: bounded model checking, bisimulation, linearizability, metamorphic testing, mutation testing, and Daikon-style invariant mining. One engine, one API.

This post is about why that one design decision pays off so many times.

Why

Nim’s existing property-testing options are QuickCheck-style: you write a generator that produces a value, and a separate shrinker that makes a failing value smaller. The two are decoupled, which means the moment you compose generators, shrinking either breaks or quietly stops shrinking. Map a generator through a function, filter it, chain it with flatMap, and the hand-written shrinker no longer knows how to walk the result. You end up either writing bespoke shrinkers for every derived type or accepting that your counterexamples come back full-size and unreadable.

That is the wrong trade, and Hypothesis showed there’s a better one. I wanted it in Nim, so I built it.

Shrinking is a property of the recording

The mechanism is small. A Strategy[T] never manufactures a value out of thin air. It only ever draws primitive choices (an integer here, a boolean there, a byte, a float) from a DataSource. The DataSource records every draw as it happens, into a typed sequence I call the choice sequence.

Because generation is a deterministic function of that recorded sequence, shrinking never has to understand your type at all. To shrink a failing example, the engine minimizes the recorded sequence of choices (make integers smaller, delete spans, lower values lexicographically) and re-runs the generator over the smaller recording. Whatever type comes out the other end, it comes out shrunk.

import std/[unittest, algorithm]
import nelli

suite "list properties":
  property "reversing a list twice is the identity":
    given xs in lists(integers(0, 9))
    ensure xs.reversed.reversed == xs

  property "addition commutes":
    given a in integers(-50, 50), b in integers(-50, 50)
    ensure a + b == b + a

That compiles, it runs under std/unittest, and it shrinks, with no shrinker code anywhere. map, filter, flatMap, oneOf, auto-derived strategies for your own object variants and recursive types: all of them shrink, because none of them are what gets shrunk. The recording is.

A couple of consequences fall out of this that are worth naming, because they come back later:

  • Reproducibility lives in the recording, not the seed. A failing example is a byte sequence you can store, replay, and minimize independently of the RNG that first produced it.
  • The choice sequence is a universal interchange format. Anything that can produce or mutate a sequence of typed choices can drive the entire strategy layer. That matters in a minute.

Inputs are just data

Once a test input is a recorded sequence of typed choices, the question “where did that sequence come from?” has more than one answer. Random draws are just the first. Everything below reads from the same sequence.

Coverage-guided fuzzing

A fuzzer hands you a raw byte buffer. So point the DataSource at bytes instead of at an RNG, and fuzzOnce(strategy, property, bytes) turns any property into a libFuzzer or AFL target, with the same strategies, shrinking, and example database behind it. The property you already wrote is now a fuzz harness.

Mutation is the part worth explaining. A naive fuzzer flips bits in the raw byte stream. When that stream is really a length-prefixed encoding of typed choices, a flipped bit in a length byte usually decodes into an out-of-range length that the strategy clamps or rejects, and the iteration is wasted. nelli’s default mutation mode (fmIR) mutates the typed choice sequence directly instead of the bytes: every mutant still respects the constraints the strategy declared (an integer’s min and max, a boolean’s probability, a span’s alignment), so mutations land as structurally valid inputs rather than as noise the decoder throws away. Raw byte mutation is still available when you actually want libFuzzer-style input, but the IR-aware mode is what makes fuzzing a Nim data structure productive.

Coverage closes the loop. Annotate the code under test with a {.cover.} pragma and nelli injects edge recording into an AFL-style bitmap. Then coverage becomes just another optimization target for the same targeted-testing machinery (a multi-objective search with a Pareto front, greedy hill-climbing, and simulated-annealing escape) that nelli already uses for user-defined target scores. The instrumentation costs nothing unless you turn recording on.

SMT-backed symbolic execution

Random search and coverage feedback both struggle with the same thing: a branch you only take when input == 0xDEADBEEF. Fuzzing can bang on that door for a very long time. A solver opens it in one query.

nelli includes a symbolic-execution walker over a fragment of Nim. It walks the code under test, builds up the path constraints for a branch you want to reach, and asks Z3 for a concrete input that satisfies them, using my own nim-z3 bindings. The design decision I’m proudest of is how it treats integers. Nim’s integers are fixed-width machine words, which map to SMT bit-vectors. Bit-vector reasoning is precise but slow. Unbounded mathematical integers (Z3Int) are much faster to solve but unsound for code that can overflow. nelli abstracts a fixed-width integer to Z3Int only when a static range analysis proves the abstraction sound: it proves that the bit-vector and integer semantics agree over every value the variable can take, and falls back to bit-vector semantics the moment that proof fails. You get the speed of integer reasoning without the unsoundness, and the verdict is never a silent wrong answer.

And because a solved input is just a set of primitive choices, the witnesses symbolic execution finds are fed straight back into the choice sequence as seeds. A solver-discovered input then runs under the property engine and shrinks like any other example. The three techniques aren’t bolted together. They’re the same pipeline reading from the same buffer.

Beyond inputs: verification

The choice sequence generalizes in another direction too: from what input to what sequence of operations. That’s the door to stateful and verification techniques.

  • Stateful / model-based testing. A StateMachine[S] is an initial state and a set of rules. nelli generates a plan (a sequence of rule firings with drawn arguments) and checks an invariant against the resulting state. The plan itself is part of the recorded choice sequence, so the shrinker minimizes the command sequence the same way it minimizes an integer: by deleting steps and lowering choices until you’re left with the shortest sequence that still fails.
  • Bounded model checking. Where the stateful runner samples one plan per example, bmcCheck enumerates every reachable plan up to a depth bound. A clean run is a verification claim (the invariant holds for every plan of length ≤ N), not merely the absence of a counterexample.
  • Bisimulation. Given a reference implementation and an optimized one, bisim decides observational equivalence by walking the product of their state spaces in lockstep and reporting the first plan that distinguishes them. This is how you prove a fast rewrite behaves exactly like the slow original, up to the depth bound.
  • Linearizability. A Wing-Gong checker decides whether a concurrent history could have happened under some sequential ordering, and the companion parallel runner draws its scheduling jitter from the choice sequence. So when a race is found, the shrinker pulls the schedule toward the minimal interleaving that exposes it.
  • Metamorphic testing for functions with no oracle (checking relations between outputs under input transforms), mutation testing that scores your properties by seeding synthetic bugs into the code under test and counting how many the properties catch, and Daikon-style invariant mining that runs a function across many inputs and reports the properties that always held.

Every one of these is a consumer of the same engine. None of them needed its own generator, its own shrinker, or its own reproducibility story, because those live in the choice sequence and the example database, one layer down.

Why one engine is the point

It would have been easy to build these as separate tools. Most ecosystems do: a property-testing library over here, a fuzzer over there, a symbolic-execution research project that never touches either. The cost of that separation is duplicated machinery and inputs that can’t move between tools.

nelli’s bet is the opposite. Shrinking, the example database, coverage instrumentation, and seeding are shared infrastructure, and each technique is a consumer of the choice-sequence IR rather than a fork of it. The property runner itself is a pluggable pipeline of phases (database reuse, explicit seeds, random generation, targeted search, shrinking, explanation, finalization), so adding a capability means adding a phase, not rewriting the runner. A fuzzer-found crash, a solver-found witness, and a hand-pinned regression seed are all the same kind of object, and they all shrink the same way.

Pick the right representation for a test input, and a pile of techniques that are usually separate tools collapse into features of one library. That’s the idea.

Status and name

nelli is written in Nim, targets the ORC memory manager, and is Apache-2.0. The name is Nahuatl for “truth,” which fits a tool whose job is deciding whether a claim about your code actually holds. It was originally called proptest. The rename came once “property testing” stopped describing half of what it does.

The core property-testing engine is production-ready, and the fuzzing and symbolic-execution layers are the frontier I’m actively building out. Code, docs, and the issue tracker are at github.com/coreyleavitt/nelli .

If you want the deeper cuts, they’re their own posts: how the sound integer abstraction is actually proved , and why nelli mutates the choice sequence instead of the bytes .