# Decidable By Construction: Design-Time Verification for Truly Fearless Systems

arXiv: https://arxiv.org/abs/2603.25414 · HTML: https://mlsanity.com/paper/2603.25414/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 28 references that are in the map.
- First posted on arXiv 26 Mar 2026.

## Builds on (most cited first, 13 of 13)

- [Convex optimization](https://mlsanity.com/paper/2106.01946/) (2021)
- [CVXPY: A Python-Embedded Modeling Language for Convex Optimization](https://mlsanity.com/paper/1603.00943/) (2016)
- [OptNet: Differentiable Optimization as a Layer in Neural Networks](https://mlsanity.com/paper/1703.00443/) (2017)
- [Differentiable Convex Optimization Layers](https://mlsanity.com/paper/1910.12430/) (2019)
- [Hierarchical Reasoning Model](https://mlsanity.com/paper/2506.21734/) (2025)
- [Conditional Memory via Scalable Lookup: A New Axis of Sparsity for Large Language Models](https://mlsanity.com/paper/2601.07372/) (2026)
- [Gradients without Backpropagation](https://mlsanity.com/paper/2202.08587/) (2022)
- [Position: Categorical Deep Learning is an Algebraic Theory of All Architectures](https://mlsanity.com/paper/2402.15332/) (2024)
- [Beyond Backpropagation: Optimization with Multi-Tangent Forward Gradients](https://mlsanity.com/paper/2410.17764/) (2024)
- [Closing the Gap Between Float and Posit Hardware Efficiency](https://mlsanity.com/paper/2603.01615/) (2026)
- [Dimensional Type Systems and Deterministic Memory Management: Design-Time Semantic Preservation in Native Compilation](https://mlsanity.com/paper/2603.16437/) (2026)
- [The Program Hypergraph: Multi-Way Relational Structure for Geometric Algebra, Spatial Compute, and Physics-Aware Compilation](https://mlsanity.com/paper/2603.17627/) (2026)
- [Adaptive Domain Models: Bayesian Evolution, Warm Rotation, and Principled Training for Geometric and Neuromorphic AI](https://mlsanity.com/paper/2603.18104/) (2026)

## Built on by (most cited first, 1 of 1)

- [Forethought: Verifiable Reasoning from Neurosymbolic Primitive Programming](https://mlsanity.com/paper/2607.04096/) (2026)

## Abstract (arXiv)

Concurrency, parallelism and distributed execution become truly fearless when the compiler tracks wait-for edges, proves multi-threaded work is sound and preserves distributed boundary contracts. In this design, our Composer compiler preserves proofs while lowering Clef directly to native CPU, GPU, NPU and FPGA code, without translation through C or vendor APIs. Our Program Semantic Graph retains the values, relationships and premises that justify BAREWire's unboxed boundary contracts. And C & C++ interfacing is an explicit marshaling boundary, with proofs tied to actual arguments, conversions and returned values. Four verification tiers connect an account of our design. Tier 1 supplies structural inference, founded on principal dimensional types. Tier 2 generates and checks local arithmetic, representation, and computational integrity at the node level. Tier 3 instantiates reusable domain and system lemmas, including distributed proofs supported by Iris, Actris and Aneris. Tiers 1-3 require no developer annotations, with a quotation based lemma library design to extend coverage as use cases expand. Tier 4 admits computational and probabilistic relational proofs, with project annotations identifying the required relations. We extend the same library direction toward recognizing relational constructions from hypergraph structure. A formal composition rule connects arithmetic, ownership, protocol and realization evidence. Our worked distributed reduction preserves one specified result across concurrent workers, reordered arrivals and boundary mappings. Its probabilistic extension carries worker and conversion error with an explicit failure budget. With recent work by Urschel, we show bounds supply a relevant source of reusable proof terms. These constructions make verification a core engineering discipline for truly fearless programs and systems across a variety of hardware targets.