Building dependable and reliable software remains a major challenge in today’s world: we sit at the brink of an explosion in the amount and complexity of computer programs. Increasingly intricate and interconnected software systems, the dramatic rise and availability of GPU resources, the prospect of quantum computing at relevant scales of practical utility and the growing role LLMs in program writing make ensuring reliability, security and reproducibility hard. Formal verification becomes foundational to tame that complexity; its effectiveness is modulated by available programming language constructs and their corresponding logic properties. In this manuscript, we present evidence suggesting that APL provides a viable solution to the problem of constructing dependable software through formal verification of programs. As a very high-level language (VHLL) with strong research precedents in formal verification, its abstractions correspond to algorithms readily specifiable in Hoare logic. We provide a general review of formal verification, as well as a literature review of direct and indirect connections to formal verification in APL. Using recent work in APL for quantum computing, we describe a workflow-driven methodology to verify quantum programs from the perspective of correctness, safety and liveness. Finally we discuss opportunities and open questions in formal verification with APL. Our observations suggest that, similar to how machine learning methods became viable once the enabling hardware and software context reached a sufficient state of maturity, formally verified APL software may be ready for prime time: APL and other array languages can –and likely will- play a larger role to shape the landscape of future software.