Search results

Migration ergonomics: check-deadline, sliver prove_equiv, eval-constant helper

Status: Open.

#71 In pulseengine/ordeal;

· avrabe opened on Jul 15, 2026

v0.15.0 (FEAT-012): Lean-verified bit-blaster — encoder into the trusted core

enhancementNew feature or requestNew feature or request

Status: Open.

#68 In pulseengine/ordeal;

· avrabe opened on Jul 11, 2026

v0.14.0 (FEAT-011): the certificate as evidence — rules_ordeal + rivet artifact type + SAT front-end

enhancementNew feature or requestNew feature or request

Status: Open.

#67 In pulseengine/ordeal;

· avrabe opened on Jul 11, 2026

v0.13.0 (FEAT-010): equivalence & soundness toolkit — prove_valid API + consumer recipes

enhancementNew feature or requestNew feature or request

Status: Open.

#66 In pulseengine/ordeal;

· avrabe opened on Jul 11, 2026

perf: deferred FEAT-005 items — LRAT trimming, incremental term-graph caching, criterion benchmark harness

enhancementNew feature or requestNew feature or request

Status: Open.

#57 In pulseengine/ordeal;

· avrabe opened on Jul 11, 2026

approach: single-source the checker + lean/Kernel.lean (generation), so drift is unrepresentable — beyond the regen.sh freshness gate

Status: Open.

#48 In pulseengine/ordeal;

· avrabe opened on Jul 8, 2026

·  

v0.15.0

approach: run the bv_decide-style checker adversarially vs the Aeneas path (dual-mechanisation bug-finder)

Status: Open.

#47 In pulseengine/ordeal;

· avrabe opened on Jul 8, 2026

·  

v0.15.0

rivet aspice-schema friction resolved — re-verify traceability closes clean (rivet #648/#650/#652)

Status: Open.

#40 In pulseengine/ordeal;

· avrabe opened on Jul 3, 2026

Integration question: bit-exact verification of spar's generated data-type layouts (small QF_BV equivalence)?

Status: Open.

#38 In pulseengine/ordeal;

· avrabe opened on Jul 3, 2026