fuzzamoto-libafl: Assertions as feedback by dergoegge · Pull Request #69 · dergoegge/fuzzamoto

dergoegge · 2025-11-28T16:53:42Z

No description provided.

maflcko

nice. left a comment, but feel free to ignore.

maflcko · 2025-12-01T10:50:40Z

doc/src/design/assertions.md

+# Assertions
+
+Fuzzamoto implements a feedback-guided assertion system inspired by
+[Antithesis's sometimes
+assertions](https://antithesis.com/docs/best_practices/sometimes_assertions/),
+designed to both validate program correctness and guide fuzzing toward
+interesting execution states.
+
+The assertion system is only available when fuzzing with
+[`fuzzamoto-libafl`](../usage/libafl.md).


The docs you link to are a bit vague around "sometimes assertions" being able to fail. Also, in the current implementation they are not able to fail, even if the fuzzing completes?

I am thinking, it could make sense to have both:

A macro to guide the fuzz engine to mark a condition as interesting and provide the fuzz engine with some kind of distance to reach it. Maybe this could be called reachability_goal(...) (or coverage_goal(...))

A macro to ensure different interesting "leaf" coverage is hit when iterating over a pre-generated, static set of (minimized) fuzz inputs in one folder. Maybe this could be called reachability_assert(...) (or coverage_assert(...)).

Such "reachability asserts" could help to more reliably trigger major coverage drops (google/oss-fuzz#11398). Not sure if this is in-scope for fuzzamoto, but I wanted to mention it, because it seems interesting in the greater fuzzing scope.

The docs you link to are a bit vague around "sometimes assertions" being able to fail.

The way I understand it, failure for these assertions is defined as "over all tests we ran, the condition was never true", so in the context here, the following assertion would fail if none of the generated testcases ever managed to submit a valid transaction to the mempool.

assert_sometimes!(cond: mempool_size > 0, "Mempool is not empty");

This means that a failed assertion might flip to being satisfied over time as the fuzzing potentially discovers the right input. And in the other direction, a satisfied assertion might flip into failure if for some reason the coverage/state can no longer be reached.

Also, in the current implementation they are not able to fail, even if the fuzzing completes?

Yea in my implementation the sometimes assertions don't fail in a normal sense, but their status for a specific campaign can be inspected by looking at the assertion.txt file that is generated, e.g.:

✗ Sometimes gt(127, 1000): Mempool may contain more than 1000 txs ✓ Always cond(true): One active tip must exist ✓ Always lt(960096, 5000000): Mempool usage does not exceed the maximum ✓ Always lte(525000000000, 2100000000000000): Coin supply is within expected limits ✓ Sometimes cond(true): Block tip may change ✓ Sometimes cond(true): Mempool is not empty ✓ Sometimes cond(true): Node under test should send addr messages

I think I'll export the assertion "results" in a machine readable way, such that surrounding infrastructure can keep track and report issues based on them (e.g. coverage drops). Maybe also add some stats about the assertions to the stdout fuzzer output.

Such "reachability asserts" could help to more reliably trigger

I'll think about your suggested macros but I feel like the macros I have now could already satisfy those needs?

I think I'll export the assertion "results" in a machine readable way, such that surrounding infrastructure can keep track and report issues based on them (e.g. coverage drops). Maybe also add some stats about the assertions to the stdout fuzzer output.

Such "reachability asserts" could help to more reliably trigger

I'll think about your suggested macros but I feel like the macros I have now could already satisfy those needs?

Yes, if your macro is designed so that surrounding infra decides how to treat a coverage miss, then both needs (explicitly assert on coverage, or just set a silent coverage goal) are satisfied. The only difference is that one approach puts the treatment of coverage misses in the source code directly, the other approach puts the treatment in the surrounding infra.

I guess a third option could also be to keep a single macro and set an env var to denote how the macro should behave: COVERAGE_ASSERT=0/1.

But all of this can trivially be implemented later and any approach looks good to me.

Crypt-iQ

Reviewed the code and it's clear and makes sense to me, will run. Left some clarifying questions.

Crypt-iQ · 2026-01-26T22:08:39Z

fuzzamoto/src/assertions.rs

+#[serde(rename_all = "snake_case")]
+pub enum Assertion {
+    Condition(bool),
+    LessThan(u64, u64),


would there ever be a use for supporting signed types?

Crypt-iQ · 2026-01-27T15:59:28Z

fuzzamoto/src/assertions.rs

+                ("Sometimes", detail, msg)
+            }
+            AssertionScope::Always(inner, msg) => {
+                fires = !fires;


wondering why this gets inverted? Is it because it was already inverted when assertion.evaluate calls distance?

Crypt-iQ · 2026-01-27T21:19:25Z

fuzzamoto-libafl/src/feedbacks/assertions.rs

+        let previous = self.assertions.get(&new.message());
+
+        let result = match (previous, &new) {
+            (None, new) => new.evaluate() || !self.only_always_assertions,


why is !self.only_always_assertions needed? Is it so that a Sometimes entry can be put into self.assertions and then later evaluate_assertion calls get closer in distance?

Crypt-iQ · 2026-01-28T17:40:03Z

fuzzamoto-libafl/src/stages/mod.rs

            .map(|m| m.list.clone())
            .unwrap_or(vec![]);

+        if !self.minimizing_crash && novelties.is_empty() {


does this skip minimization if there were no novelties?

Yes because an input might be interesting due to the assertion feedback but not from a coverage perspective. I need to extend the minimize to take the assertion feedback into account (i.e. minimize with the goal of retaining new coverage as well as the novel assertion states)

Crypt-iQ · 2026-01-28T17:40:42Z

fuzzamoto-nyx-sys/src/nyx-agent.c

@@ -1,3 +1,4 @@
+#include <assert.h>


curious why this is needed?

Crypt-iQ · 2026-01-28T17:53:56Z

fuzzamoto/src/assertions.rs

+pub fn log_assertion(assertion: &AssertionScope) {
+    if let Ok(json) = serde_json::to_string(assertion) {
+        unsafe {
+            nyx_println(json.as_ptr() as *const i8, json.len());


clarifying question: this lets the StdOutObserver pick this up (since under the hood it is using NyxHelper and nyx_stdout) and then is used in AssertionFeedback is_interesting?

Crypt-iQ · 2026-01-28T18:03:50Z

doc/src/design/assertions.md

+
+Compared to traditional aggregate source code coverage reports, sometimes
+assertions provide additional insights into the explored state space. For
+example, a coverage report would tell us that a chain reorganization occured


nit: occurred

Crypt-iQ · 2026-01-28T18:27:34Z

doc/src/design/assertions.md

+Example usage:
+
+```rust
+assert_sometimes!(cond: mempool_size > 0, "Mempool is not empty");


q: where is the macro used? in the scenario?

It can be used in any code that runs inside the vm (scenario, oracles, targets, ...)

dergoegge · 2026-02-13T16:52:27Z

Just rebased, haven't addressed review feedback yet

maflcko reviewed Dec 1, 2025

View reviewed changes

Crypt-iQ reviewed Jan 28, 2026

View reviewed changes

Crypt-iQ mentioned this pull request Feb 12, 2026

add support for incremental snapshots #103

Open

dergoegge force-pushed the assertions branch from 59416e4 to 5ed436f Compare February 13, 2026 16:51

dergoegge force-pushed the assertions branch from 5ed436f to 8a91e66 Compare February 13, 2026 17:01

dergoegge added 2 commits February 13, 2026 17:05

fuzzamoto-libafl: Add sometimes/always assertions

f059e9d

doc: Assertions

7503930

dergoegge force-pushed the assertions branch from 8a91e66 to 7503930 Compare February 13, 2026 17:05

fuzzamoto-libafl: Make minimizer assertion aware

4d2ca9d

Conversation

dergoegge commented Nov 28, 2025

Uh oh!

maflcko left a comment

Choose a reason for hiding this comment

Uh oh!

maflcko Dec 1, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Crypt-iQ left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dergoegge commented Feb 13, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

maflcko Dec 1, 2025 •

edited

Loading