Project Formalization V3

Counterexample Lab / Public case study

Project Formalization

Change one boundary. Watch a machine-checked safety claim become a production violation.

wolfSSL 5.9.0 DTLS 1.3 CVE-2026-6679
Pending ACK records 4,095

The list remains representable through 4,095 entries.

Serialization contract Ready
Actual body 4,095 x 16 = 65,520 B
Reserved body 65,520 B
Capacity reserved65,520 B
Writer traversal65,520 B
out of bounds
  1. Harness ready. Select a boundary and run verification.

Claim boundary: production serialization overflow reproduced from reconstructed post-authentication state. A full encrypted live-peer transcript was not established.

Public evidence / Sealed result

The visual story ends where the evidence begins.

Every claim in the lab maps to preserved output from the pinned wolfSSL production build. Open either plate to inspect it at full resolution.

Source pin
922d04b3
Formal property
ack-write-capacity
Runtime oracle
AddressSanitizer
Evidence plate showing 65,536 bytes narrowing to zero in a 16-bit ACK body length. MechanismArithmetic and traversal contract Production replay plate comparing the clean 4,095 control with the 4,096 AddressSanitizer overflow. Production replayControl, witness, and critic

Five agents / One sealed protocol

Independence is part of the evidence.

The coordinator freezes one target and two framings. Investigators work in isolation; critics attack each result only after it is sealed.

Protocol ready 0 / 5
CO
CoordinatorFreeze target and properties
A1
Investigator 1Find the suspected violation
A2
Investigator 2Verify the safety properties
sealed isolation
C1
Hostile critic 1Challenge witness and replay
C2
Hostile critic 2Search for modeling gaps
Final classification Compare evidence, not confidence.
00:00

The protocol begins with an unset verdict.

Evidence before claims

A counterexample is only the beginning.

  1. 01Pin

    Hash the exact production source and freeze the property.

  2. 02Verify

    Run a real formal backend with explicit bounds and assumptions.

  3. 03Replay

    Reproduce against a fresh build with a useful negative control.

  4. 04Challenge

    Make an independent critic try to break the claim.