Issues

rv32: a retained function relocating against a declined INTERNAL emits a dangling `synth_func_N` and exits 0 — the #851 guard #1013 gave aarch64 is not on the RISC-V path

#1102

· avrabe opened

on Aug 28, 2026

MC/DC gate: the report-side absolute floors are layout-coupled — a 14-line guard anywhere moves unrelated functions' proved counts both directions (witness#208)

bug

#1100

· avrabe opened

on Aug 27, 2026

The silent-miscompile evidence behind the #1093 decline is not a CI oracle — the guard survives, its justification does not

#1097

· avrabe opened

on Aug 27, 2026

README:122 and FEATURE_MATRIX advertise a 'CI-tracked compile rate' over the spec suite that no job produces — and submodules are never checked out, so the directory is empty in CI

#1095

· avrabe opened

on Aug 27, 2026

The traceability completeness gate has never fired: 60/60 release artifacts across v0.56-v0.60 have no linked sys-verification, and 'rivet coverage' prints instead of asserting

#1091

· avrabe opened

on Aug 27, 2026

An artifact can be 'implemented' in vX.Y on evidence that shipped in vX.Y-1 — every gate passes and the release notes are wrong

#1085

· avrabe opened

on Aug 27, 2026

coq/*.ml extraction snapshots are checked in, stale, and referenced by no gate or build — the stale-artifact-nobody-checks class in a corner #977 did not reach

#1080

· avrabe opened

on Aug 27, 2026

debug_assert-guarded immediate ranges are compiled out in release — an out-of-range imm12 mis-encodes silently; 6 sites remain after #1071 fixed the one the census reached

#1072

· avrabe opened

on Aug 26, 2026

synth-wcet-v1 names functions from the export section only, so the --wcet-hints seam has no key for internal functions — 7 of our 13 loop declines are unaddressable

#1063

· avrabe opened

on Aug 26, 2026

CI capacity: 56 of 63 job definitions target ubuntu-latest while 12 self-hosted runners idle — 401 jobs queued, 0 in progress during the v0.59 merge wave

#1062

· avrabe opened

on Aug 26, 2026

RULE-VERIFY has no obligation for control flow or byte-level memory — 48% of a real object is covered by neither half

#1057

· avrabe opened

on Aug 25, 2026

The i64 param-clobber fuzz harness checks 'before FIRST read' — a write between two reads is exempt by construction (missed #1048 and the Clz/Ctz/Popcnt clobber it had itself named)

#1055

· avrabe opened

on Aug 25, 2026

Navigation Menu

Uh oh!

All issues

rv32: a retained function relocating against a declined INTERNAL emits a dangling `synth_func_N` and exits 0 — the #851 guard #1013 gave aarch64 is not on the RISC-V path

MC/DC gate: the report-side absolute floors are layout-coupled — a 14-line guard anywhere moves unrelated functions' proved counts both directions (witness#208)

The silent-miscompile evidence behind the #1093 decline is not a CI oracle — the guard survives, its justification does not

README:122 and FEATURE_MATRIX advertise a 'CI-tracked compile rate' over the spec suite that no job produces — and submodules are never checked out, so the directory is empty in CI

The traceability completeness gate has never fired: 60/60 release artifacts across v0.56-v0.60 have no linked sys-verification, and 'rivet coverage' prints instead of asserting

An artifact can be 'implemented' in vX.Y on evidence that shipped in vX.Y-1 — every gate passes and the release notes are wrong

coq/*.ml extraction snapshots are checked in, stale, and referenced by no gate or build — the stale-artifact-nobody-checks class in a corner #977 did not reach

debug_assert-guarded immediate ranges are compiled out in release — an out-of-range imm12 mis-encodes silently; 6 sites remain after #1071 fixed the one the census reached

synth-wcet-v1 names functions from the export section only, so the --wcet-hints seam has no key for internal functions — 7 of our 13 loop declines are unaddressable

CI capacity: 56 of 63 job definitions target ubuntu-latest while 12 self-hosted runners idle — 401 jobs queued, 0 in progress during the v0.59 merge wave

RULE-VERIFY has no obligation for control flow or byte-level memory — 48% of a real object is covered by neither half

The i64 param-clobber fuzz harness checks 'before FIRST read' — a write between two reads is exempt by construction (missed #1048 and the Clz/Ctz/Popcnt clobber it had itself named)

Uh oh!

Search results