Repository navigation

Formal verification for the ECSM affine selector - #925

Open

nicole-graus wants to merge 14 commits into

perf/ecsm-affine-selectorfrom

verify/ecsm-affine-selector

Open

Formal verification for the ECSM affine selector#925
nicole-graus wants to merge 14 commits into
perf/ecsm-affine-selectorfrom
verify/ecsm-affine-selector

Commits on Aug 11, 2026
- Add a z3 soundness gate for the ECSM affine selector
  nicole-graus
  committed
  a311a66
- Add missing negative control
  nicole-graus
  committed
  96a00cc
Commits on Aug 12, 2026
- Check yG canonicality
  nicole-graus
  committed
  10c73d1
- Move the campaign to formal_verification/
  nicole-graus
  committed
  5321a96
- Move the campaign to a flat formal_verification/ecsm-affine
  nicole-graus
  committed
  7c66383
- Trim RESULTS.md and fix the misplaced finding
  nicole-graus
  committed
  168f41a
- Correct the stale attack and SAT counts
  nicole-graus
  committed
  9119838
Commits on Sep 3, 2026
- Walk all 423 indices and instantiate A3g
  jotabulacios
  committed
  09c324a
- Audit the q1 width A3g depends on
  jotabulacios
  committed
  57b32a9
- Fail the gate when its transcript is stale
  jotabulacios
  committed
  42c0e44
- Refresh the gate transcript
  jotabulacios
  committed
  3ded53d
- Update the board for the new checks
  jotabulacios
  committed
  17638ed
Commits on Sep 4, 2026
- Note the yG gap is in the spec too
  jotabulacios
  committed
  f7abe2c
Commits on Sep 8, 2026
- Merge branch 'perf/ecsm-affine-selector' into verify/ecsm-affine-selector
  jotabulacios
  committed
  0547809