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.

The property-testing core has no external dependencies. import nelli never touches Z3. The solver sits behind an explicit import nelli/symex, so you do not install one to get property tests.

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.

Here is what that looks like on a real bug. The function is a checksum whose accumulator is masked to a byte. The property claims that a one-element list checksums to its own element:

proc checksum(xs: seq[int]): int =
  var acc = 0
  for x in xs:
    acc = (acc + x) and 0xFF
  acc

proc prop(xs: seq[int]) =
  let bad = xs.len == 1 and checksum(xs) != xs[0]
  ensure not bad

forAll(lists(integers(0, 10_000), 1, 64), prop,
       Settings(maxExamples: 2000, seed: 20260917'u64))

The first falsifying input the engine found was @[9597]. What it reported after shrinking was @[256], the smallest value the mask can bite. This is the repro() string for the failure:

outcome=otFalsified
examples=8
seed=20260917
counterexample=@[256]
message=: ensure failed: not bad
choices:
  bool!(true) [free]
  int(256) [necessary]
  bool(false) [necessary]

The choices: block is the shrunk recording. The tags say which draws mattered to the failure and which could have been anything. Here the forced first “another element?” draw is free, the value 256 is necessary, and so is the decision to stop at one element.

Shrinking goes through nesting the same way. A take-limit bug that needs two levels of list to trigger was first found at

@[@[1, 0, 6], @[20, 784, 20, 747, 13],
  @[9, 999, 933, 22, 772, 62, 49, 0, 41, 0, 1, 793], @[0], @[0, 0, 0]]

and reported as @[@[0], @[0]]. Nobody wrote a shrinker for lists of lists.

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. I assumed the cost of that was mutants dying at the decoder. Measured, it is something else: on a list of bytes, 83% of byte-level mutations decode fine and produce the value the parent already had, because most bytes of the encoding cannot affect the decoded value. nelli’s fuzz loop mutates the typed choice sequence directly instead. Every node carries the constraint the strategy declared (an integer’s min and max, a boolean’s probability), so a change to a node is a change to the input. On the same budget against a small binary parser, that reaches 18 coverage edges where byte mutation reaches 2. nelli used to ship both loops. The byte one has been removed, and a byte corpus from another fuzzer is decoded into choice sequences on import. The numbers and the mutators are in the fuzzing post . One current gap in the byte door: float draws do not read from the buffer yet.

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 parameter can take, and falls back to bit-vector semantics the moment that proof fails. Measured, that is roughly 2 to 3 times faster on code whose parameters carry ranges and no change on bit-manipulating code. The proof currently covers less than the design calls for, and the abstraction post documents a case where that produces a 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. There is a full trace of that below.

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.

One input, three tools

“One engine” is architecture talk until you watch a single input move through it. This is a real trace. The function under test has a branch guarded by a magic constant, and the property claims that branch is never taken:

const Magic = 0x5A4D          # 23117

proc classify(x: int): int =
  if x == Magic: result = 1
  elif x > 1_000_000: result = 2
  elif x < -1_000_000: result = 3
  else: result = 0

proc prop(x: int) =
  ensure classify(x) != 1

The strategy is integers(-2_000_000, 2_000_000). classify stands in for production code, and nothing in it knows it is being tested. The solver is pointed at the property, with symexFind(prop, tRaisedExn()), which asks whether prop can fail. It walks into classify without being told to.

stage 0 - random property testing
  200000 random examples over [-2e6, 2e6]
  outcome: otPassed

stage 1 - symbolic execution
  query:   can `prop` raise?
  status:  sxRaised  (FalsifiedError)
  witness: x = 23117  (0x5A4D)
  as choice IR: 1 node(s)
    int(23117)

stage 2 - property runner, seeded with the witness
  outcome:        otFalsified
  counterexample: 23117
  examples run:   0
  shrunk choice sequence:
    int(23117)  [nNecessary]

stage 3 - fuzzer, seeded with the same sequence
  iterations:    2000
  corpus:        4 entries
  coverage:      4 distinct edges
  crashes:       1
    message: ensure failed: false
    choices:
      int(23117)
  (unseeded, same budget: 0 crashes, 3 edges)

stage 4 - example database: store, then replay
  run 1 (symex-seeded): outcome=otFalsified counterexample=23117 dbReplays=0
  db contents after run 1:
    one-input-demo.bin  (115 bytes)
  run 2 (db only):      outcome=otFalsified counterexample=23117 dbReplays=1

Random testing runs 200,000 examples and passes. The solver finds the input in one query. That witness is lifted into a one-node choice sequence, which is the only conversion in the whole trace. The property runner takes the sequence as a seed and falsifies before drawing a single random example. The fuzzer takes the same sequence into its corpus and reports the crash, where the same budget without the seed finds nothing. The example database stores it. Run 2 has a different RNG seed, a budget of one example, and no solver, and it fails on the same input because the database replayed it.

Two honest notes on the trace. The fuzzer needs the {.cover.} pragma on something to get coverage feedback, and the symbolic executor currently gives up on any path that crosses a call it treats as opaque, which includes the edge recording that pragma injects. So stage 3 drives a thin instrumented wrapper around the same untouched classify, and the solver sees only the uninstrumented code. That is issue 163 , and it is the biggest gap between this trace and the claim that one function serves all three tools. The second note is smaller: the convenience wrapper for solver seeds does not persist to the database yet, so stage 4 composes the runner’s phase list by hand. Both came out of writing this demo.

What this replaces

The obvious question is what this does that Hypothesis, AFL++, and KLEE wired together do not. Each of those is better at its own job than nelli is. None of them shares a representation with the others. To move the input above between them you write a harness per tool, a converter from KLEE’s test-case files to whatever your property test accepts, and another from an AFL crash file to the same. The crash the fuzzer finds does not shrink through the property tester’s shrinker, because the shrinker does not understand AFL’s bytes. Each handoff is glue you write and then maintain.

In nelli each technique is a consumer of the choice sequence. Shrinking, the example database, coverage instrumentation, and seeding are shared infrastructure. The property runner 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. A fuzzer-found crash, a solver-found witness, and a hand-pinned regression seed are the same kind of object, and they all shrink the same way. The handoffs cost nothing because there is nothing to convert.

Why Nim

Building this in a language with a small user base needs a reason. Nim’s macros see a typed AST at compile time. That is what makes given / ensure, the {.cover.} pragma, and auto-derived strategies ordinary library code, and it is the reason an in-language symbolic executor is feasible at all: symexFind reads the body of the function you hand it, with types resolved, and compiles it to SMT without a separate frontend or a bitcode step.

Status and name

nelli is written in Nim, is developed and tested against 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. The fuzzer and the symbolic executor are younger, and the symbolic executor in particular covers a fragment of Nim, not the language. What it does about that is the part I would point to. A query comes back as a witness, a proof of unreachability, a reachable raise, or sxUnknown with a classified reason attached. Code outside the fragment produces the last one. It does not produce a guess. The cases the walker declines are pinned in the test suite as declines, so a future change that starts answering them turns a test red and has to be looked at.

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 .

Updated 2026-09-17. An earlier version described raw byte mutation as an available fuzzing mode and explained its cost as decoder rejections. The byte loop has been removed and the measured cost is inert mutations. The shrink example, the end-to-end trace, and the measurements were added in this update.