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

Houston Haynes

cs.PLMar 26, 2026

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

Authors: Houston Haynes

Organizations: SpeakEZ Technologies, Asheville, NC

Abstract

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.

Figures & tables

Concern	Active execution	Replacement preparation and publication
Persistent resources	Published code, configuration and retained state	Candidate version and any state-conversion resources
Temporary storage	Live calls, buffers and queued work	Update computation, transfer and validation buffers
Admission evidence	Premises supporting the current operations	Evidence for the candidate's interfaces, behavior and realization
Version and lifetime	A coherent version remains valid for each use	Atomic publication and justified retirement of superseded resources

Table 1

Tier	Judgment	Compiler and library contribution
1	Structural relationships in admitted type interpretations	Automatic dimensional inference and established structural or parametricity rules
2	Local arithmetic, range and representation conditions	Compiler-generated obligations checked in supported analysis and decision fragments
3	Parameterized domain and system contracts	Automatic selection and instantiation of registered lemmas from program and hypergraph structure
4	Relations between computations, distributions or realizations	Project-specific relational annotations, with reusable rule libraries and structural recognition intended to extend automatic coverage

Table 2

Mechanism	Establishes or supports	Costs that remain
Convex projection	Membership in a specified feasible set, under the implementation's arithmetic contract	Projection evaluation, unless statically proved redundant
Residual or penalty objective	A specified discrepancy and its contribution to an optimization criterion	Residual evaluation and evidence for the required accuracy or feasibility
Lookup and selection	Retrieval under a specified key or selection policy	Lookup, version handling, conversion and required validation
Typed elaboration	The admitted structural and proof obligations	Constraint solving, preservation checks and necessary runtime boundary validation

Table 3

Assessment	Required positive evidence	Discriminating change
Automatic Tier 2/3 coverage	Ordinary reduction and protocol code generates the applicable conditions and lemma instance	A construction outside the registered law produces a specific coverage diagnostic
Argument and boundary binding	The source value, actual call operand, representation conversion and receiver use share a justified correspondence	Changing the actual operand or receiving contract invalidates the affected instance even if an arithmetic answer is unchanged
Concurrent acceptance	Reordering and duplicating arrivals preserves the accepted-set and accumulator invariants	Separating freshness testing from the atomic acceptance transition exposes the duplicate-admission obligation
Relational realization	Each admitted partition and target implementation preserves the selected observation relation	A changed rounding order, width, signedness or emitted operation requires the corresponding new relation or evidence
Error and failure budgets	Worker error, boundary conversion and failure events compose to the application contract	A fresh randomized retry or altered observation policy changes the relevant risk account
Direct composition across tiers	A checked Tier 2 bound becomes a premise in a Tier 4 proof term through its registered interface	Rebinding the bound to another value or removing a receiving-rule premise invalidates the application

Table 4

Explore similar work

May 26, 2026

ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification

Formal verification of large C programs is impeded by state-space explosion: Bounded Model Checking (BMC) tools must encode the entire state space up to the predetermined bound by unrolling all nested constructs. We present ConVer, a top-down compositional verification tool. Given a C program with a top-level assertion, ConVer decomposes verification top-down: it uses a large language model (LLM) to synthesise function contracts from the system property, then alternates system-level and function-level checks in a CEGAR-CEGIS loop, refining contracts whenever a check fails via SMART ICE learning. We evaluate ConVer on four benchmark suites of increasing difficulty and against other state-of-the-art (SOTA) tools. On the Frama-C benchmark of 45 simple C programs, ConVer achieves 82-96% verification success across three LLM backends, with 93-95% of converged programs requiring only a single CEGAR-CEGIS iteration. On the X.509 parser benchmark (6~programs) and LF2C-Simple suite (17 programs), ConVer achieves 33-50% and 82-88% success respectively. On the VerifyThis suite of 11 recursive and loop-intensive programs, the Pre-Abstraction strategy achieves 55-64% success. In addition, we present ESBMC-LF a preprocessor tool that converts LF models to C while preserving the properties of the LF files, enabling ConVer to verify them. We transpile the LF Verifier Benchmarks using ESBMC-LF to C; we denote those LF-Hard. We show that ConVer successfully verifies 67% of LF-Hard benchmarks overall.

Muhammad A. A. Pirzada, Weiqi Wang, Yiannis Charalambous +2

The University of Manchester · Manchester, UK

Counterexample-Guided Refinement Formal Verification

Ask PDF

Sep 27, 2026

Zero-Storage Procedural Neural Synthesis via Boundary Dynamics: Formal Verification in Lean 4 and Bare-Metal Gauntlet Validation

Contemporary neural inference architectures rely on dense floating-point weight matrices stored in high-bandwidth memory (VRAM), incurring severe memory-wall bottlenecks and preventing native execution inside deterministic virtual machines like the Ethereum Virtual Machine (EVM). Verifying termination and arithmetic invariants for recursive dynamical systems over continuous domains is generally undecidable in the Blum-Shub-Smale model. Here, we present the formal verification and bare-metal empirical validation of WERR (Waves & Errors) and Phase III Orbital Error Dynamics (OED), a non-tensor decision paradigm that procedurally synthesizes non-linear decision boundaries on demand from a 24-byte coordinate seed

Θ= (c_x, c_y, \text{zoom})

along the boundary of the Mandelbrot set (

\partial\mathcal{M}

). By projecting the recurrence

z_{n+1} = z_n^2 + c

onto the modular residue ring

\mathbb{Z}/9\mathbb{Z}

and the fixed-point domain

\mathbb{Q}_{16.16}

, we establish ten machine-verified theorems in Lean 4 (v4.34.1) with Mathlib4 and zero unproven conjectures (sorry): proving

\mathcal{I}_3 = \{0,3,6\} \subset \mathbb{Z}/9\mathbb{Z}

ideal closure, universal fuel-bounded halting (

\le 9

and

\le 12

steps), absence of

\mathbb{Q}_{16.16}

square overflow below

2^{63}-1

, non-constant boundary escape sensitivity, and a parametric EVM gas bound (

\le 22,557 \le 24,000

gas). Evaluated on a 40-core Dual Intel Xeon server, the vectorized 36-iteration CPU kernel processes 100,000 decisions in 6.49 s (15,397 decisions/s, 0 Bytes VRAM, 15.15x speedup), while a sigmoidal outlier gate suppresses 100.00% of adversarial spikes while preserving 89.60% of clean baseline signals.

Volkan Dağlı, Zerrin Dağlı, Dağhan Dağlı

Anadolu University, Türkiye · ITouch Systems, Türkiye · Mersin University, Türkiye +1

Classification Formal Verification

Ask PDF

May 22, 2026

Agentic Proving for Program Verification

Agentic systems have recently emerged as state-of-the-art approaches for automated theorem proving in formal mathematics. To assess how far these capabilities extend to program verification, we evaluate Claude Code in an agentic proving framework on CLEVER, a Lean 4 benchmark for verifiable code generation. Our results show that Claude generates arguably valid specifications for 98.8% of problems (with 81.3% also accepted by CLEVER's isomorphism-based scoring on the correct portion of the benchmark), certifies implementations against correct ground-truth specifications for 87.5% of problems, and reaches a 98.1% success rate on the end-to-end program generation and verification pipeline over entries with self-consistent premises. Across all stages, Claude further provides high-quality feedback on its own attempts (as confirmed under manual review), identifying underlying causes of failure and lingering bugs in the dataset. These findings highlight a growing mismatch between the difficulty of existing program verification benchmarks and the capabilities of modern agentic provers, and point to the need for more rigorous, bug-resilient evaluation methodologies, and in particular for alternatives to isomorphism-based scoring of generated specifications. More broadly, our results provide empirical evidence that tight compiler-in-the-loop agentic paradigms are currently the most effective approach for foundational program verification.

Alessandro Sosso, Akhil Arora, Bas Spitters

Department of Computer Science Aarhus University Aarhus, Denmark

Automated Theorem Proving Formal Verification Lean Theorem Proving

Ask PDF