Exhibit A

Breaker-State Formal Escalation

Localized SAT-backed divergence evidence for the evaluated < versus <= RTL operator shift.

TargetCircuit breaker logic

Conebreaker_state

BackendYosys SAT

Isolated Neighborhood

Triage isolated a semantic mismatch on the breaker_state signal. The logic was represented in a localized miter for formal comparison.

// DESIGN A (Reference)
assign trip = (liquidity < threshold);

// DESIGN B (Candidate - Trojan v4)
assign trip = (liquidity <= threshold);

Functional Divergence Proof

The SAT solver searched for any input state where the reference and candidate logic produced different outputs.

Metric	Result	Analysis
Search space	65,536 states	Exhaustive search of 8-bit input pairs.
Time to proof	< 0.1s	Localized cone verification completed in under 0.1s for the evaluated benchmark.
Proof outcome	DIVERGENCE FOUND	Reference and candidate behavior differ.

Counterexample Trace

liquidity_pool00000000 / decimal 0

threshold00000000 / decimal 0

Assessment: in the reference design, 0 < 0 is false, so the breaker remains closed. In the candidate design, 0 <= 0 is true, so the breaker trips. The operator shift introduces a functional boundary change that could trigger premature circuit-breaker behavior under specific conditions.

Why This Matters

The exhibit demonstrates the practical value of review compression. Instead of attempting broad whole-chip proof first, the workflow starts with the suspicious cone, applies a standard SAT backend to a tractable target, and packages the result for human review.

Boundary

This is a bounded localized divergence exhibit.
It does not prove whole-chip correctness.
It does not claim complete Trojan detection.
It depends on accurate cone extraction and reviewer judgment.