This work presents a deductive verification framework based on a weighted assertion language and an intermediate verification language, whose weight domains are ordered structures with implication and coimplication, which let verification conditions express lower- and upper-bound obligations internally.
Abstract
Weighted programs extend guarded commands with trace weights drawn from a semiring, or more generally a monoid-module. Varying this algebra gives one programmatic syntax for a variety of quantitative and symbolic models. Weakest-preweighting semantics provides a compositional basis for reasoning about those programs. We present a deductive verification framework based on a weighted assertion language and an intermediate verification language. Its weight domains are ordered structures with implication and coimplication, which let verification conditions express lower- and upper-bound obligations internally. We prove sound translations of core commands and reusable encodings for various proof rules applying to procedure calls and loops. To facilitate automation, we prove soundness of a quantifier elimination procedure for our assertion language. A prototype in the Caesar verifier checks case studies for probabilistic queueing costs, recursive database provenance with cyclic dependencies, clearance bounds for networks of arbitrary size, and formal-language reasoning about lock-freedom of a compare-and-swap counter.
FLEX is presented, a foundational Constrained Horn Clause (CHC) solver implemented in LEAN, that reduces the trusted base to the kernel alone, and allows using LEAN's entire proof ecosystem to verify low-level systems code, via three contributions.
J. Khan, Petros Markopoulos, Nicolás Lehmann et al.· 0 citations
The key idea is to implement an entailment checker as a combination of an efficient but unverified prover, suitable for fast-paced interactive proofs, and a proof reconstruction procedure that takes the prover’s trace and produces a certificate of entailment validity that can be checked a posteriori.
V. Mikhal'chuk, V. Gladshtein, I. Sergey· International Conference on...· 0 citations
This paper develops mechanized foundations for writing formal correctness proofs for both HeyVL encodings and PP verification techniques that are grounded in the basics of probability theory and formalizes Markov decision processes (MDPs).
Oliver Bøving, Christoph Matheja· International Conference on...· 0 citations
Relating low-level executable code to a high-level account of its behavior has been a central concern of programming-language research for decades. From formally verified compilers to translation validators, certifying compilers, and proof-carrying code, each approach chooses between laborious but foundational mechanized proofs and automation that costs completeness, generality, and an increased trusted base. Recently, large language models (LLMs) have begun to change the economics of formal verification. Agentic proof development is now capable of producing machine-checked proofs at a scale and speed that were previously out of reach. In this paper, we evaluate the capabilities of LLMs to produce foundational, machine-checked proofs of refinement between executable code and its high-level specification, as post hoc, per-artifact certificates. We study this in the context of the Ethereum Virtual Machine (EVM), a low-level virtual machine that executes smart contracts on the Ethereum blockchain. We build EquiVM, a foundational framework in Lean comprising an executable EVM semantics and a specification language that characterizes the intended behavior of smart contracts, but commits to no source language or compilation toolchain. In EquiVM, refinement is stated for deployed bytecode of arbitrary provenance, interaction with unknown code is part of the semantics, and each proof is a replayable, machine-checked certificate. No previous technique achieves this combination. Using frontier commercial LLMs, twenty-three real-world contracts are proved end to end with minimal human guidance, among them most of the MakerDAO stablecoin system, at up to a hundred million tokens and a hundred hours of proof time per contract. We conclude that foundational mechanized proofs can now be bought at the price of tokens, and that this shift can reshape how verification frameworks are architected.
Verifying effectful higher-order programs, such as probabilistic programs with unbounded recursion, is a central problem in program verification. Predicate transformer semantics, closely related to continuation-passing style and weakest precondition semantics, has been proposed as a compositional method for computing verification objectives. Due to its categorical and denotational formulation, it can uniformly capture quantitative properties such as expected costs. However, its relationship to operational semantics remains largely unexplored with respect to more advanced properties, such as cost moments and conditional expectations of probabilistic programs with unbounded recursion, thereby leaving its connection to concrete program executions unclear. In this paper, we establish a generic framework to prove adequacy for predicate transformer semantics with respect to an appropriately designed operational semantics. Our approach is simple yet expressive enough to cover a wide range of instances, including total expected costs, cost moments, conditional expectations, and expected multiplicative rewards of probabilistic higher-order programs with unbounded recursion.
Kazuki Watanabe, Mirai Ikebuchi, Mayuko Kori· Proceedings of the ACM on Pr...· 0 citations
SymCert is presented, a framework implemented in Lean for building verified SMT-based analyses of Cedar policies that provide a verified symbolic compiler and authorizer for reducing policies to SMT formulas, a hierarchy enforcer for ensuring well-formedness of counterexamples, and a counterex-ample extractor for proving analysis completeness.