Definition & Overview

A counterexample is a specific input, state, or scenario that disproves a claimed property of a system. In formal logic, a single counterexample is sufficient to disprove a universal claim ("for all X, P(X) holds"). In software testing, counterexamples are automatically generated by property-based testing (PBT) frameworks that explore the input space to find values that violate specified properties, then "shrink" the counterexample to the minimal failing case.

Property-based testing differs fundamentally from example-based testing. Traditional tests verify specific input-output pairs (e.g., "add(2, 3) == 5"). Property-based tests verify universal properties (e.g., "for all integers a and b, add(a, b) == add(b, a)"). When the framework finds an input that violates the property, it produces a counterexample -- a concrete, reproducible witness to the property violation.

In the Prismatic Platform, counterexample generation is part of the comprehensive testing strategy that maintains 100/100 quality. The platform uses StreamData (Elixir's property-based testing library) to generate counterexamples for critical subsystems including the OSINT tool input validation, storage adapter contracts, DD entity schema validation, and NABLA axiom enforcement. The White Team's white-invariant-prover agent uses property-based testing as one of its formal verification tools.

Technical Deep Dive

Counterexample Lifecycle

Phase	Description	Tool	Output
Property Definition	Specify universal claim	StreamData	Property specification
Generation	Random input generation	Generators	Candidate inputs
Evaluation	Test property against inputs	ExUnit	Pass/Fail per input
Counterexample	First failing input found	StreamData	Raw counterexample
Shrinking	Minimize failing input	Shrinking algorithm	Minimal counterexample
Regression	Store for future runs	Seed persistence	Reproducible test

Property-Based Testing with StreamData

defmodule PrismaticOsintCore.PropertyTest do
  @moduledoc """
  Property-based tests for OSINT tool input validation.
  Uses StreamData generators to discover counterexamples
  that reveal hidden assumptions in input processing.
  """

  use ExUnit.Case, async: true
  use ExUnitProperties

  property "tool slug normalization is idempotent" do
    check all slug <- string(:alphanumeric, min_length: 1, max_length: 100) do
      normalized = normalize_slug(slug)
      assert normalize_slug(normalized) == normalized
    end
  end

  property "confidence scores are always in [0, 100]" do
    check all scores <- list_of(float(min: -1000.0, max: 1000.0), min_length: 1) do
      result = PrismaticOsintCore.ConfidenceScorer.aggregate(scores)
      assert result >= 0
      assert result <= 100
    end
  end

  property "entity ID generation produces unique values" do
    check all count <- integer(2..100) do
      ids = Enum.map(1..count, fn _ -> generate_entity_id() end)
      assert length(Enum.uniq(ids)) == count
    end
  end

  property "search query sanitization removes injection attempts" do
    check all query <- string(:printable, min_length: 0, max_length: 500) do
      sanitized = sanitize_query(query)
      refute String.contains?(sanitized, "'")
      refute String.contains?(sanitized, ";")
      refute String.contains?(sanitized, "--")
    end
  end

  defp normalize_slug(s), do: s |> String.downcase() |> String.replace(~r/[^a-z0-9-]/, "-")
  defp generate_entity_id, do: Ecto.UUID.generate()
  defp sanitize_query(q), do: String.replace(q, ~r/[';\\-]{2}/, "")
end

Shrinking Strategy

defmodule PrismaticTest.ShrinkingDemo do
  @moduledoc """
  Demonstrates counterexample shrinking.
  When StreamData finds a failing input, it systematically
  reduces the input to the smallest value that still fails.
  """

  use ExUnit.Case, async: true
  use ExUnitProperties

  property "demonstrates shrinking to minimal counterexample" do
    # If this property fails, StreamData will shrink the list
    # from potentially [42, 99, 7, 81, ...] to something like [1, 1]
    # The minimal counterexample reveals the true boundary condition
    check all list <- list_of(positive_integer(), min_length: 1) do
      assert Enum.sum(list) < 100
    end
  end
end

White Team Property Verification

defmodule PrismaticDark.WhiteTeam.InvariantProver do
  @moduledoc """
  White Team invariant verification using property-based testing.
  Systematically searches for counterexamples to claimed invariants.
  A failed search (no counterexample found) provides probabilistic
  evidence that the invariant holds.
  """

  @type invariant :: %{
    name: String.t(),
    property: (term() -> boolean()),
    generator: StreamData.t(term()),
    iterations: non_neg_integer()
  }

  @type proof_result :: %{
    invariant: String.t(),
    status: :holds | :violated,
    iterations_tested: non_neg_integer(),
    counterexample: term() | nil,
    shrunk_counterexample: term() | nil
  }

  @default_iterations 1000

  @spec prove(invariant()) :: {:ok, proof_result()} | {:violated, proof_result()}
  def prove(invariant) do
    iterations = Map.get(invariant, :iterations, @default_iterations)

    result = try do
      Enum.reduce_while(1..iterations, nil, fn i, _acc ->
        value = StreamData.resize(invariant.generator, min(i, 100))
        |> Enum.take(1)
        |> List.first()

        if invariant.property.(value) do
          {:cont, nil}
        else
          {:halt, {:counterexample, value, i}}
        end
      end)
    rescue
      _ -> nil
    end

    case result do
      {:counterexample, value, iteration} ->
        proof = %{
          invariant: invariant.name,
          status: :violated,
          iterations_tested: iteration,
          counterexample: value,
          shrunk_counterexample: shrink(value, invariant.property)
        }
        {:violated, proof}

      _ ->
        proof = %{
          invariant: invariant.name,
          status: :holds,
          iterations_tested: iterations,
          counterexample: nil,
          shrunk_counterexample: nil
        }
        {:ok, proof}
    end
  end

  defp shrink(value, property) when is_list(value) do
    value
    |> Enum.reduce(value, fn _, acc ->
      shorter = Enum.drop(acc, -1)
      if shorter != [] and not property.(shorter), do: shorter, else: acc
    end)
  end
  defp shrink(value, _property), do: value
end

Architecture & Implementation

The Prismatic Platform integrates property-based testing at three levels. At the unit level, StreamData generators create random inputs for individual function testing. At the integration level, contract tests use property generation to verify that storage adapters satisfy their behavioral contracts across a wide input space. At the verification level, the White Team's invariant prover systematically searches for counterexamples to claimed system properties.

Counterexample persistence is critical for regression prevention. When StreamData finds a counterexample, the test seed is recorded, enabling exact reproduction of the failing case in subsequent test runs. This turns a discovered counterexample into a permanent regression test -- satisfying the Mandatory Regression Test Protocol.

The shrinking algorithm is what transforms property-based testing from "finding a bug" to "understanding a bug." A raw counterexample might be a 50-element list with complex values, but the shrunk counterexample might be [0, -1], immediately revealing the boundary condition. StreamData's shrinking is type-aware: it shrinks integers toward 0, strings toward empty, lists toward shorter, and composites recursively.

Usage in Prismatic Platform

The OSINT tool input validation uses property testing to ensure that no user input can cause unexpected behavior. Generators produce random queries, including edge cases (empty strings, Unicode, very long inputs, special characters), and verify that the input processing pipeline handles all cases gracefully without crashes or injection vulnerabilities.

The DD pipeline's schema validation uses property testing to verify that entity normalization is idempotent (normalizing a normalized entity produces the same result) and that relationship integrity is maintained across load cycles. Counterexamples from these tests have revealed edge cases in Unicode handling, date parsing, and JSONB attribute merging.

The Quality gates include property-based test execution as part of the CI pipeline. All property tests run with a minimum of 100 iterations (configurable to 1000 for critical paths), providing probabilistic assurance that no counterexamples exist within the tested input space.

Cross-References

Contract - behavioral specifications tested by property-based testing
Assertion - verification primitive within property tests
Code Coverage - property tests improve edge case coverage
Code Quality - counterexample discovery improves quality
Livebooks: livebooks/domains/quality_testing/ - property-based testing labs
Academy: Advanced testing methodology and property-based testing

Created by Tomas Korcak (korczis) | GitHub

Counterexample