Function lec_next_state_matches_vm 

pub fn lec_next_state_matches_vm(
    rtl: &str,
    reg: &str,
    spec: BoundedExpr,
) -> Option<bool>

LOGICAL EQUIVALENCE CHECK (corner 5, phase 3) — discharged by OUR OWN certified SAT, not yosys’s SAT or Z3. Parse the soft-core RTL, extract register reg’s next-state, and prove it equals spec (the VM op’s datapath function) for EVERY input by refuting the miter rtl_next ≠ spec with logicaffeine_proof::sat::prove_unsat — a bit-blasted CDCL refutation, the LEC “back-check”. This is the equivalence a tool like yosys equiv runs on its internal SAT, done here on ours. Returns Some(true) iff the RTL datapath is equivalent to the VM spec, Some(false) if a differing input exists, None if the RTL / next-state / miter can’t be lowered to the bit-blaster.