On the Verifiability of Programs Written in the Feature Language Extensions