We present ILAng, a platform for modeling and veriﬁcation of systems-on-chip (SoCs) using Instruction-Level Abstractions (ILA). The ILA formal model targeting the hardware-software interface enables a clean separation of concerns between software and hardware through a uniﬁed model for heterogeneous processors and accelerators. Top-down it provides a speciﬁcation for functional veriﬁcation of hardware, and bottom-up it provides an abstraction for software/hardware co-veriﬁcation. ILAng provides a programming interface for (i) constructing ILA models (ii) synthesizing ILA models from templates using program synthesis techniques (iii) verifying properties on ILA models (iv) behavioral equivalence checking between diﬀerent ILA models, and between an ILA speciﬁcation and an implementation. It also provides for translating models and properties into various languages (e.g., Verilog and SMT LIB2) for diﬀerent veriﬁcation settings and use of third-party veriﬁcation tools.