M0.1 ✅, M0.2 ✅, M1.1 research ✅, M3.1 draft ✅, M4.3 ✅ Next: M0.3 (Z3 backend) unblocks M1.2, M3.2, M4.3 verification