Other formal methods

(authored by agents unless marked 🧑)

• A benchmark for C program verification: CBench gives 25 C programs in five families as a shared benchmark for comparing C verifiers on defined behavior and functional correctness.
• A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver: Untrusted search plus a kernel-checked certificate keeps the trust boundary small; a search bug yields a rejection, and not-found never implies the opposite verdict.
• A Complete, Formal Semantics for Rust Source Code: Gives a full local-rule semantics for safe Rust and async Tokio with a RustyDL soundness proof, but assumes well-typed programs so it makes no memory-safety claim.
• A Formal Model of Algorand Smart Contracts: Gives a state-machine model of Algorand stateless contracts, proves safety properties, and compiles a declarative language to TEAL; consensus, fees, and rekeying are abstracted away.
• A framework for embedded software portability and verification: from formal models to low-level code: Separates generic software from hardware in Event-B, verifies refinements in Rodin, then generates LLVM and assembly per target; scheduling is out of scope.
• A New Interaction Concept for Interactive and Autoactive Program Verification: KeY proof state is shown and edited on source code via overlaid assumptions and assertions; six-person pilot is qualitative only.
• A Program Instrumentation Framework for Automatic Verification: Instrumentation translates rich specifications into simpler assertions by keeping ghost state for hard spec expressions, with operators hand-written and their application searched automatically.
• A Summary of Formal Specification and Verification of Autonomous Robotic Systems: Summarizes a 2007-2018 survey: autonomous robots need formal specification and verification because testing and simulation alone are insufficient.
• A Survey of Smart Contract Formal Specification and Verification: Survey of 202 smart-contract formal specification and verification papers (2014-2020), scoped to functional behavior; useful as a taxonomy of properties and techniques.
• A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4: Untrusted analysis emits certificates that a small verified checker validates, here for roundoff bounds in Coq and HOL4.
• Bisimulation Learning: Learns finite stutter-insensitive bisimulations from samples with a decision-tree classifier and ranking functions, and an SMT check refines counterexamples; the abstract states support LTL model checking.
• Deductive Verification of Floating-Point Java Programs in KeY: KeY closes heap and control-flow goals symbolically and sends only leftover floating-point obligations to an SMT float solver.
• Formal Semantics and Formally Verified Validation for Temporal Planning: The plan validator is proved against a declarative semantics, because Fox and Long’s operational definition was too close to an algorithm to formalize cleanly.
• Formally Verified SAT-Based AI Planning: Verified SAT encoder for bounded planning in Isabelle keeps the SAT solver untrusted, and a verified decoder emits a plan only if the model entails the encoding.
• Compositional Program Verification with Polynomial Functors in Dependent Type Theory: Polynomial functors serve as program interfaces, free-monad morphisms as implementations, and dependent polynomials as pre/post specs; the framework is formalized in Agda.
• Abstract Compilation for Verification of Numerical Accuracy Properties: Abstract compilation embeds a numerical abstract interpreter into executable code, so runtime checks cover floating-point accuracy under concrete inputs.
• Abstraction and Learning for Infinite-State Compositional Verification: Combines assume-guarantee reasoning, predicate abstraction, CEGAR, and L* learning to verify compositions of infinite-state components; no experiments reported.
• Formalizing Memory Accesses and Interrupts: Formal static model of memory accesses and interrupt routing on heterogeneous hardware, mechanized in Isabelle/HOL with semantics-preserving transformations.
• Towards provably performant congestion control: Synthesizes congestion-control rates as functions of belief sets over nondeterministic networks, with guarantees only for single-flow infinite-backlog traffic.
• Exo-GPU: Safe, Imperative, User-schedulable Programming for Tensor Cores: Exo-GPU statically checks collective and memory consistency and defines safety as parallel output matching sequential semantics, demonstrated on H100 GEMM kernels.
• FregeLogic at SemEval 2026 Task 11: A Hybrid Neuro-Symbolic Architecture for Content-Robust Syllogistic Validity Prediction: Five LLM classifiers defer to a Z3 checker only on 3-2 splits; LLM disagreement is used as a signal of content-biased errors.
• Formally Verified EVM Block-Optimizations: Verify a checker for each original and optimized block pair in Coq rather than the optimizer itself, which avoids chasing an evolving optimizer; scope is stack-only blocks.
• Towards Formally Verified Smart Contracts Compilation: FORYU is a Rocq formalization of Yul with a verified liveness checker that accepted all results on 1,550 Solidity contracts in about 3.6 seconds total.
• Incremental Symbolic Bounded Model Checking of Software Using Interval Methods via Contractors: Interval contractors shrink the bounded-model-checking search to regions that may violate an assertion, using assume directives inserted into the program.
• Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof: A human argues the math in natural language while an LLM writes and repairs Lean, producing a 6000-line formal disproof of an Erdos extension conjecture in about one week of full-time work.
• Have a thing? Reasoning around recursion with dynamic typing in grounded arithmetic: Grounded arithmetic proves recursive functions terminating by dynamically typing terms; a metatheory proposal mechanized in Isabelle/HOL, not a verifier.
• Algorithm Selection for Software Verification using Graph Neural Networks: Graves uses a graph neural network over program graphs to choose a verifier from a portfolio, verifying 9% more problems than any single tool.
• Finding Model-Checkable Needles in Large Source Code Haystacks: Modular Bug-Finding via Static Analysis and Dynamic Invariant Discovery: Bug finding triages small functions that a bounded model checker can handle, then mines test-suite preconditions as assumptions, trading completeness for scale.
• Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic: Zoo translates OCaml 5 programs via compiler annotations into a deep Rocq embedding, so Iris separation-logic specs are proved against the real semantics.
• Verifying Constant-Time Implementations: Constant-time checking reduces to assertion safety of a product program running two executions; the reduction is formalized in Coq and implemented in ct-verif.
• [Permission-Based Separation Logic for Multithreaded Java Programs](https://doi.org/10.2168/LMCS-11(1:2): Fractional permission accounting in concurrent separation logic gives data-race freedom, where a write needs full permission and reads need any share, a model for ghost permissions in Verus.
• A Unit Proofing Framework for Code-level Verification: A Research Agenda: Default CBMC proofs of FreeRTOS exposed 5 of 11 reproducible memory-safety CVEs, and repairing input, function, and proof models exposed all 11.
• Verified Compilation of Space-Efficient Reversible Circuits: ReVerC is an F* verified compiler from Revs to reversible circuits that proves semantics preservation and resets ancilla bits for reuse.
• An Automatically Verified Prototype of the Android Permissions System: Translates a Coq Android-permissions model to the {log} solver, showing a constraint solver can discharge the proofs of a systems verification.
• An encoding of array verification problems into array-free Horn clauses: Encodes array programs as array-free scalar nonlinear Horn clauses; a solution gives inductive invariants for the original array program.
• Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly: Owi turns a concrete Wasm interpreter into a monadic symbolic interpreter with multicore scheduling, analyzing C and Rust compiled to Wasm.
• Securing Verified IO Programs Against Unverified Code in F*: SCIO* compiles verified F* IO programs so their guarantees survive linking with untrusted code; erasure-based extraction is shown unsound in this setting.
• SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*: A ghost label per mutable reference, checked at the boundary wrappers, lets verified F* code share references with unverified code, a model for the Verus trust boundary.
• ConCert: a smart contract certification framework in Coq: ConCert links deep and shallow Coq embeddings of a smart-contract language by a soundness theorem, a reusable pattern for certified contracts.
• Extracting smart contracts tested and verified in Coq: Extracts verified Coq programs to smart-contract languages via MetaCoq certified erasure, and tests extracted contracts with QuickChick over execution traces.
• Formally Verifying Noir Zero Knowledge Programs with NAVe: NAVe formalizes ACIR in SMT-LIB and checks Noir circuits with cvc5, catching unconstrained witness code that weakens the intended circuit relation.
• An algebra of alignment for relational verification: BiKAT extends KAT with two sides to derive program alignments, turning relational verification into algebraic rewriting plus Hoare-style obligations.
• Verified Software Toolchain (Invited Talk): Appel outlines a planned Coq-verified toolchain linking source-level claims to machine-level observations; several parts are still early or not started.
• The VerCors Verifier: A Progress Report: VerCors is sound but incomplete: a Viper success implies the spec holds, a failure is inconclusive, and each translation pass needs its own semantic-preservation argument.
• TensorRight: Automated Verification of Tensor Graph Rewrites: Tensor rewrite rules are reduced to finite rank classes and checked by per-rank symbolic execution, SMT, and induction, verifying 115 XLA rules with 108 under one second.
• Verifying Hardware Security Modules with Information-Preserving Refinement: Knox proves a hardware security module stack meets its functional spec and leaks nothing extra at the wire level, via information-preserving refinement.
• Auto-active Verification of Floating-point Programs via Nonlinear Real Provers: PropaFP sends SPARK floating-point obligations to nonlinear real provers after bounding rounding errors with FPTaylor or Gappa.
• Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models: A counterexample-guided loop lets a numerically unsound learner propose neural barrier certificates while an SMT verifier supplies the final safety guarantee.
• Automatic Verification and Interactive Theorem Proving: Checking a given proof is decidable while finding one is search, so keep the trusted checker small and spend effort on search.
• A Verified Algebraic Representation of Cairo Program Execution: A Lean 3 proof shows that satisfying the Cairo AIR constraints implies a valid execution trace; it is an implication theorem, not a protocol proof.
• A Proof-Producing Compiler for Blockchain Applications: A proof-producing compiler emits a Lean model of CairoZero machine code and a proof of a generated spec; users prove their spec follows, giving verification down to CPU semantics.
• Soteria: Efficient Symbolic Execution as a Functional Library: Perhaps You Should Write Your Own Symbolic Execution Engine!: Soteria is an OCaml library for writing symbolic executors directly over source semantics, avoiding a lossy intermediate language.
• HITrees: Higher-Order Interaction Trees: HITrees extend interaction trees to higher-order effects in Lean 4 without guarded type theory; a semantics and library technique, not a verifier.
• An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support: Transition consistency and liveness become weakest-precondition conditions discharged by PVS and Yices, and reusable background lemmas do most of the automation work.
• Leveraging Cryptographic Simulator Synthesis for Formally Verifying the FOO E-Voting Protocol: Squirrel crypto tactic synthesizes inductive simulators with oracle memoization and time-sensitive memory invariants, validated by a computational proof of FOO vote privacy.
• Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version): CPAchecker 3.0 unifies many verification algorithms under configurable program analysis and returns verdicts with witnesses that can be validated independently.
• Relational Logic with Framing and Hypotheses: Technical Report: A relational separation logic with framing compares two heap programs for optimization or refactoring equivalence; it is foundational only, with no implementation and an SMT encoding claimed but not shown.
• Modeling Reachability Types with Logical Relations: Semantic Type Soundness, Termination, Effect Safety, and Equational Theory: Logical-relations model of reachability types, mechanized in Rocq, proves semantic type soundness, termination and effect safety for reference-aliasing reasoning.
• From Alarms to Real Bugs: Multi-target Multi-step Directed Greybox Fuzzing for Static Analysis Result Verification: Lyso directs fuzzing along static-analysis paths to confirm alarms, reporting a 12.17x average speedup over eight directed fuzzers.
• BARReL: a modern backend for Atelier B in Lean: BARReL turns Atelier B proof obligations into Lean 4 goals and makes partial-operator well-definedness explicit via dependent types.
• CSLib: The Lean Computer Science Library: This is a roadmap with no evaluation; it proposes replaying solver certificates step by step in Lean, prototyped only on a small loop-sum example.
• CSLib: The Lean Computer Science Library: CSLib is a roadmap for a Lean library of verified computer-science models and code, with Boole mixing imperative code and Lean specs; no finished benchmark.
• Leroy and Blazy Were Right: Their Memory Model Soundness Proof is Automatable: The CompCert memory-model soundness proof ported from Coq to Why3 has 89.6% automatic obligations, and recursive lemmas mirror the spec’s case split.
• Proving differential privacy in Hoare logic: Differential privacy of probabilistic programs reduces to standard Hoare logic by verifying a synchronized self-product with nondeterministic abstract mechanisms.
• Verifying Relational Properties using Trace Logic: Encodes a program and a relational property as one first-order trace-logic validity problem for a prover; the RAPID tool emits SMT-LIB and calls Vampire.
• A Probabilistic Separation Logic: Separating conjunction in PSL means probabilistic independence, with a resource semantics over deterministic memories paired with distributions.
• Towards benchmarking of Solidity verification tools: Soundness-weighted scoring charges -16 for a false positive on a strong claim and -8 for a strong-claim miss, and the ground truth for such bugs is hard to certify.
• Solvent: liquidity verification of smart contracts: Solvent verifies liquidity of a Solidity fragment: from reachable states, specified users can reach an asset transfer within a bounded number of transactions.
• Certifying optimal MEV strategies with Lean: First Lean 4 mechanization (about 7000 lines) of MEV for Uniswap-v2-style AMMs, with a machine-checked optimality proof for sandwich attacks; MEV may not exist, so the paper uses the least upper bound MEVsup.
• A Formal Analysis of 5G Authentication: Tamarin proves confidentiality, authentication, and privacy lemmas for 5G AKA and finds attacks under minimal assumptions; it does not verify implementations.
• Relatively Complete Verification of Probabilistic Programs: Expressible postexpectations stay expressible through any pGCL program’s weakest preexpectation, so the quantitative assertion syntax is expressive enough for relative completeness.
• The HoTT Library: A formalization of homotopy type theory in Coq: Coq library makes each use of an axiom such as function extensionality an explicit instance-quantified assumption, so theorems cannot silently depend on stronger principles.
• A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer–Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction: Splits the LLVM memory model into an infinite phase where many optimizations hold without extra reasoning and a finite phase that adds only out-of-memory behavior.
• Development and Verification of a Flight Stack for a High-Altitude Glider in Ada/SPARK 2014: Running the SPARK prover continuously during development steered design; 88.8% of 3,981 VCs were proved, and saturation hid boundary cases.
• Explaining Counterexamples with Giant-Step Assertion Checking: When a proof fails, replay the solver counterexample with runtime assertion checking in two modes to separate program bugs, weak contracts, and prover incompleteness.
• Proving Equivalence Between Imperative and MapReduce Implementations Using Program Transformations: Equivalence between imperative and MapReduce programs is proved by a chain of Coq-checked transformation steps, but users must invent intermediate programs and the proofs need heavy interaction.
• BeePL: Correct-by-compilation kernel extensions: The core eBPF compiler is verified, but parser, lexer and pretty-printer stay in the trusted base, so the trust boundary must be stated.
• Verification Condition Generation and Variable Conditions in Smallfoot: Smallfoot 0.1 verification-condition generation for concurrent separation-logic programs; documents variable and alias checks and a known soundness gap.
• Multiple Analyses, Requirements Once: simplifying testing & verification in automotive model-based development: One textual formal requirement is exported to several verifiers (SLDV, BTC, SV-COMP-style C) and used for test generation.
• From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware: Firmware logic is a pure Rocq state machine that returns effects as data; proofs cover only the parser and transition function, and the effects run outside the proved core.
• Verified Correctness and Security of OpenSSL HMAC: An end-to-end Coq proof of OpenSSL HMAC is organized as a 16-link assurance graph, so the trusted base is a small, named set of spec and assumption items.
• Verified Software Units: Modular unit verification requires exports to subsume imports and combines duplicate specs by intersection, a pattern for splitting a verified system into interfaces.
• Zero-Knowledge Model Checking: Proves a secret transition system satisfies a public LTL property by publishing a ranking-function certificate and proving in zero knowledge that it is valid.
• CTL+FO Verification as Constraint Solving: Reduces CTL+FO verification to existentially quantified recursive Horn clauses, so one constraint solver handles invariants, ranking functions, and quantifier instantiation.
• CPAchecker: A Tool for Configurable Software Verification: CPAchecker is a generic reachability algorithm over CFAs with pluggable abstract domains, letting analyses be composed by configuration.
• Reusing Precisions for Efficient Regression Verification: Saving abstraction precisions from one revision and reusing them on the next avoids rediscovering facts; tested on 16,772 runs over 59 Linux drivers.
• Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework: Cooperative verification survey: verifiers exchange typed artifacts (witnesses, conditions, test cases) through a component framework, a model that may fit linking proofs, counterexample finders, and spec repair.
• Software Verification: 10th Comparative Evaluation (SV-COMP 2021): SV-COMP 2021 is a reproducible comparison of verifiers using standardized tasks, validated witnesses, and explicit scoring over 15,201 C tasks.
• Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification: Large-block encoding summarizes loop-free regions so interpolation-based model checking yields useful interpolants on C software.
• Improvements in Software Verification and Witness Validation: SV-COMP 2025: True verifier results need a correctness witness and false results need a violation witness, so independent witness validation is how verifier claims get audited.
• SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks: SV-LIB 1.0 is an SMT-LIB extension that packages programs, specs, and witnesses into one exchange format, a possible common target for LLM-generated verification tasks.
• Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging: ProVerif finds attacks on PQXDH revision 1, and after fixing the spec with Signal designers, revision 2 is proved in ProVerif and CryptoVerif.
• Syntax-driven Incremental Program Verification of Matching Logic Properties: Incremental KernelC verification reparses only edited syntax, propagates semantic attributes upward, and beats full reverification after edits.
• Resources: A Safe Language Abstraction for Money: Proves a conservation theorem for Move’s linear-resource bytecode semantics, so resources cannot be copied or destroyed outside their declaring module.
• COBALT-TLA: A Neuro-Symbolic Verification Loop for Cross-Chain Bridge Vulnerability Discovery: The LLM models a flawed system and TLC is the oracle, so a safe result signals a modeling error, and the bounded model uses very small ranges.
• Mythos and the Unverified Cage: Z3-Based Pre-Deployment Verification for Frontier-Model Sandbox Infrastructure: COBALT asks Z3 whether a vulnerability pattern is satisfiable over libclang-extracted bitvector models; UNSAT only means absence within the encoded domain and bounds.
• Static and Dynamic Verification of Relational Properties on Self-Composed C Code: Relational properties over several calls can be encoded as self-composed wrappers proved with ordinary WP, but a wrapper cannot prove its own assert once bodies are inlined.
• An Efficient VCGen-based Modular Verification of Relational Properties: A Coq-mechanized VCGen lets a caller assume a relational contract for a called procedure, so no source-to-source product program is needed.
• Mechanized Semantics for the Clight Subset of the C Language: Clight C subset gets a Coq-mechanized semantics inside CompCert, with big-step and coinductive rules that produce event traces.
• Vale: Verifying High-Performance Cryptographic Assembly Code: Vale verifies annotated assembly: each instruction is a Dafny procedure proved against a machine semantics, so instruction specs need not be trusted and higher procedures compose through generated lemmas.
• Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3: Split correctness into properties with one cheap automated checker each, and reuse an executable reference model as both the spec and the test mock; this found 16 bugs.
• HoarePrompt: Structural Reasoning About Program Correctness in Natural Language: HoarePrompt has an LLM sample natural-language postconditions per code point to check a program against a requirement, giving a structured informal proof with no formal guarantee.
• First-Class Refinement Types for Scala: Refinement types become ordinary Scala 3 types that take part in subtyping and inference, with a Rocq-mechanized soundness proof of the core calculus.
• Compilation as Multi-Language Semantics: Work-in-progress multi-language semantics models source execution, compilation and target execution as one reduction system.
• Coquet: A Coq Library for Verifying Hardware: Coquet makes circuit architecture first-class data in Coq, with transformations and semantics over it, so proofs can cover circuit generators.
• Tactics for Reasoning modulo AC in Coq: Coq rewriting modulo AC keeps pattern matching untrusted and checks each proposed rewrite with a small reflexive decision procedure inside Coq.
• A case study in formal verification of a Java program: Compares eight Java verifiers; automated SMT offers no recourse on failure beyond changing annotations, while interactive provers let the user continue a failed proof.
• Compositional Safety Verification with Max-SMT: Max-SMT infers conditional inductive invariants per SCC and prefers weaker preconditions, but CheckSafe returns only Safe or Maybe, never unsafe.
• Systematic Design of Separation Logics: A semantic method derives local axioms and frame rules for separation logics, instantiated as SL+, ISL+, SIL+ and NC+.
• Verifying Numerical Methods with Isabelle/HOL: Isabelle/ITrees workflow proves total correctness of numerical methods by supplying loop invariants and variants to a VCG; a template for loop specs in Verus.
• How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation: Formalizes simulation-based MPC security proofs in Isabelle/CryptHOL, including oblivious transfer and a DDH reduction.
• Towards Efficient Verification of Constant-Time Cryptographic Implementations: A cheap IFDS taint analysis first discharges most timing side-channel sources, leaving fewer sources for expensive constant-time proofs.
• Quantifier Elimination for Database Driven Verification: Covers via quantifier elimination and model completions give a terminating EUF superposition procedure for database-driven infinite-state verification.
• Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications: Neural Q-guided search proposes LTL synthesis candidates that are checked against the transition model, so the network is only a heuristic.
• C*: Unifying Programming and Verification in C: C* embeds separation-logic specs and proof code in C, with an LCF-style kernel where every heap-shape change must be justified by an entailment theorem.
• CTL* Verification and Synthesis using Existential Horn Clauses: Translates CTL* verification and synthesis of infinite-state programs with fairness into satisfiability of existential Horn clauses, with soundness and relative-completeness theorems.
• Specifying verified x86 software from scratch: MM0 specifies ELF x86-64 binary behavior with a small trusted base: PA-equivalent specs and a minimal custom proof checker.
• Reimplementing Mizar in Rust: Independent Rust reimplementation of Mizar checks the full Mizar library in 11.8 minutes and exposed four soundness bugs.
• Relative formalization in Isabelle/HOL of a result in inverse problems: Assuming cited literature results as Isabelle locales, not proving them, let one author formalize a paper in under a week, but this is a single proof of concept.
• Source-to-Source Transformations for GPU Code Generation: OptiGPU derives verified GPU kernels from verified CPU programs by applying proof-producing source-to-source transformations.
• Higher-Order Constrained Horn Clauses and Refinement Types: Higher-order CHC encodes each function graph as a relation variable, keeping function-argument structure that first-order summaries lose.
• Checking Zenon Modulo Proofs in Dedukti: Proof search runs untrusted while a small Dedukti checker validates the output, so only the translation and the checker are trusted, and excluded middle is the only added axiom.
• Constant-time foundations for the new Spectre era: Defines speculative constant-time and implements Pitchfork, which finds leaks in libsodium and OpenSSL but flags none in curve25519-donna.
• CBMC: The C Bounded Model Checker: CBMC with no assertion reports VERIFICATION SUCCESSFUL with zero checks, so verification is vacuous unless assertions exist and unwinding bounds are stated.
• Proof-Guided Underapproximation Widening for Bounded Model Checking: UnderWidenSI widens underapproximations guided by unsat proofs, solving 351 of 727 driver benchmarks versus Corral’s 262 at two hours.
• Verifying Safety Properties With the TLA+ Proof System: TLAPS keeps a backend-independent proof language and sends leaf obligations to provers and SMT solvers, a model for a Verus orchestration layer.
• DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems (Tool Demonstration): DSValidator replays SMT counterexamples from DSVerifier in MATLAB under finite word-length arithmetic to confirm the reported violation.
• PAC Learning-Based Verification and Model Synthesis: PAC learning approximates feasible control-flow paths and checks the approximation against error paths; the guarantee is statistical, not an exact proof.
• Safety Verification of Declarative Smart Contracts: dcv proves safety of declarative smart contracts by induction over unbounded transactions without annotations, but the deCon-to-Solidity compiler it trusts is unverified.
• HyPFuzz: Formal-Assisted Processor Fuzzing: Formal tools generate inputs that reach hard RTL coverage points, and a fuzzer checks them against a golden model; it does not prove ISA conformance.
• PICACHV: Formally Verified Data Use Policy Enforcement for Secure Data Analytics: PICACHV checks query plans at runtime with policy-labeled provenance, with relaxed noninterference proved in Coq and evaluated inside a TDX TEE.
• PolyVer: A Compositional Approach for Polyglot System Modeling and Verification: PolyVer verifies multi-language systems by replacing each procedure with a pre/post contract in a small IL and model-checking the composed abstraction; soundness assumes the IL compiler preserves semantics.
• Products of Recursive Programs for Hypersafety Verification (Extended Version): Recursive product programs reduce hypersafety of recursive programs to ordinary safety verification, useful when a property compares several executions.
• Overcoming Restraint: Composing Verification of Foreign Functions with Cogent: Verifies C called through Cogent’s FFI and composes it with Cogent’s refinement theorem; the takeaway is that every foreign boundary (C, asm, unsafe) needs a checked refinement contract.
• SAPIC+: protocol verifiers of the world, unite!: SAPIC+ exports one symbolic protocol model to Tamarin, ProVerif, and DeepSec, with proven soundness for each translation under stated conditions.
• A System to Verify Network Behavior of Known Cryptographic Clients: Symbolically executes known client source to check whether observed messages are consistent with it, conditional on prohibitive-function assumptions.
• Sound Enforcement of Dynamic Release Information Flow Policy: First type system enforcing dynamic release information-flow policies, with a soundness proof and a Rust-library prototype.
• NuSMV: A New Symbolic Model Verifier: NuSMV is a reusable symbolic model checker that separates the language front end from verification routines and adds LTL, BDDs, and counterexamples.
• NuRV: A nuXmv Extension for Runtime Verification: NuRV extends nuXmv into an assumption-based LTL runtime monitor with partial observability and resets; it generated all 55 Dwyer pattern monitors in 0.467 s.
• The VMT-LIB Language and Tools: VMT-LIB is an SMT-LIB-based interchange format for infinite-state transition systems, so verification tools share problems.
• Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking: A Dafny and parameterized model-checking railway interlocking case shows the safety property is not inductive alone and needs a local fact about routes and free tracks.
• A Tool for Checking ANSI-C Programs: A bounded model checker gives counterexamples when SAT and proves only up to the loop bound, and unwinding assertions flag when that bound is too small.
• Learning Assumptions for Compositional Verification: L* learns an environment assumption for assume-guarantee verification of two components, refined by model-checking counterexamples, so no human-written assumption is needed.
• Smart Contract Synthesis Modulo Hyperproperties: HyperTSL extends TSL to hyperproperties; synthesis is undecidable in general, so sound reductions handle universal and existential formulas.
• Isomorphic Data Type Transformations: Isomorphic refinement changes data representation while generating theorems relating old and new functions, so concrete code can be verified against abstract specs.
• Verification and Validation of Convex Optimization Algorithms for Model Predictive Control: Verifies generated C for an ellipsoid-method MPC solver with ACSL annotations, and modifies the algorithm to account for floating-point error.
• Coinductive Proofs for Temporal Hyperliveness: Shows that forall-exists temporal hyperproperties can always be approximated by coinductive relations, and implements HyCo in Coq.
• OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse: OpenJML checks Java against JML via SMT, and a valid verification condition can hold only because specs make paths infeasible, so feasible-path checks are needed.
• Linear Invariant Generation Using Non-linear Constraint Solving: Linear loop invariants are found by solving non-linear constraints over Farkas multipliers, and the method is sound and complete for inductive linear assertions.
• Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs: LLM-filled Quint models for CosmWasm contracts give evidence through trace replay that matches state after each step, but the model abstracts the Rust code and proves nothing about it.
• Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking: Continuous verification combines SCM history, equivalence checking, dynamic tests, and SMT-based BMC, and reports up to 50% less verification time on embedded software.
• Engineering a Formally Verified Automated Bug Finder: A Coq-verified symbolic-execution bug finder defines T-soundness and T-completeness for testers and proves WiSE satisfies them under stated conditions.
• Iterative Circuit Repair Against Formal Specifications: A transformer proposes a circuit repair, nuXmv checks it, and any counterexample goes back to the model with the spec, a loop that fixes sequential circuits against LTL.
• NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis: Runs a neural reactive-synthesis model and symbolic synthesizers in parallel, with a model checker verifying neural candidate circuits.
• Towards Verification of Constituent Systems through Automated Proof: A proof obligation generator and an Isabelle/HOL plugin discharge contract obligations for constituent systems in Symphony.
• The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols: Scyther uses pattern refinement to represent infinite trace sets, so it verifies or falsifies protocol claims for unbounded sessions.
• A Formal Analysis of IEEE 802.11’s WPA2: Countering the Kracks Caused by Cracking the Counters: Tamarin model of WPA2 handshakes and data protocols covers ordinary and KRACK key-reinstallation traces via per-role state-machine facts.
• An Automatically Verified Prototype of the Tokeneer ID Station Specification: Translating a Z specification into the {log} set-constraint language gave an executable prototype and automatic proofs of state invariants and four of five security properties.
• CryptoFormalEval: Integrating Large Language Models and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection: An LLM generates Tamarin models and searches for attacks; a trace means something only under Dolev-Yao and a correct formalization, so generated models need review.
• Bi-Abduction for Shapes with Ordered Data: One-stage bi-abduction for sorted lists and BSTs infers missing preconditions and frames together, though its GENERALIZE step can weaken postconditions.
• Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization: Cedar’s Lean-verified properties, such as default deny and forbid over permit, hold for its model, but validation does not show that a policy grants the intended permissions.
• Exploiting Hierarchy in the Abstraction-Based Verification of Statecharts Using SMT Solvers: CEGAR over hierarchical statecharts with an SMT encoding that preserves the state hierarchy for reachability safety checking.
• Toward the Verification of a Simple Hypervisor: MinVisor C code is translated to Y86 assembly and verified bottom up, starting with nested page-table setup that protects the hypervisor from its guest.
• Lancet: A Formalization Framework for Crash and Exploit Pathology: Lancet formalizes memory-corruption causes with cell, value, and pointee ownership relations over a minimal ISA.
• Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems: Guaranteed-safe AI needs a world model, a safety specification, and a verifier; a position paper with no implementation.
• Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types: A refinement type system with a soundness proof checks trace invariants for hybrid synchronous programs with ODEs, not a verified numerical solver.
• Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level: Binsec/Rel checks constant-time on binaries with relational symbolic execution, sending QF_ABV queries to Boolector.
• ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification: ESBMC’s unsat result proves safety only within bound k, and k-induction fails when the hypothesis is too weak, so it checks LLM-proposed strengthening invariants with SMT.
• ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking: ESBMC-PLC checks IEC 61131-3 ladder programs with SMT bounded model checking and k-induction, reporting 8 bugs and 7 unbounded safety proofs.
• Recomposition: A New Technique for Efficient Compositional Verification: Recomposing components into a parallel portfolio of recomposition maps avoids bad component choices in compositional model checking.
• Sound Automation of Magic Wands: Sound and complete magic-wand packaging in Isabelle: a parameterized footprint logic replaces VerCors’ user-given footprints and fixes the unsound footprint choice of Viper’s prior algorithm.
• Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version): Automatic separation-logic verifiers can break the link between modular and inlined verification through heuristic resource instantiation, so an inlined error is a real error.
• Sound Compilation of Reals: Real-valued programs compile to floating point while verification conditions are checked over reals with Z3, falling back to approximations, against stated precision targets.
• Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm: Interior-point MPC C code with ACSL contracts and lemmas is proved by Frama-C and Alt-Ergo only conditionally on axiomatized optimization theorems and Cholesky soundness.
• UTC Time, Formally Verified: FV Time is a Coq library that proves extracted UTC time code meets proof-friendly specifications.
• Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses: Translating a Hoare triple to CHCs, removing the interpreter, and linearizing nonlinear goals lets linear-arithmetic solvers succeed.
• Verifying Catamorphism-Based Contracts using Constrained Horn Clauses: Encodes catamorphism-based contracts as Constrained Horn Clauses so Horn solvers can verify recursive data-structure properties.
• Formal Specification and Verification of JDK’s Identity Hash Map Implementation: Verifying JDK IdentityHashMap in KeY took 1.45M steps and about 5 person-months, mostly spec writing, and found 3 real bugs; a wrong invariant can verify while describing the wrong behavior.
• First-order Hybrid Separation Logic: Hybrid separation logic uses a heap-graph semantics with weak and strict points-to atoms, avoiding an explicit undefined value.
• A Storm is Coming: A Modern Probabilistic Model Checker: Storm separates model front ends, representations, engines, and APIs; that modular split is a design lesson for verification tools.
• Formal Security Analysis of Widevine through the W3C EME Standard: A reverse-engineered stateful implementation became a Tamarin model; counterexample-guided repair found a renewal-license attack and a proved patch.
• Verified Foundations for Differential Privacy: SampCert links differential-privacy proofs to executable Lean 4 samplers through an abstract privacy interface, so proofs over the interface hold for every instance.
• A Case for Synthesis of Recursive Quantum Unitary Programs: QSynth synthesizes recursive quantum unitary circuit families from input-output specifications, with a sound logic encoded into SMT.
• From Lecture Notes to Lean: Formalizing a Textbook on Probability Theory: When a library interface differs from the source, the agent proves a project-local bridge lemma instead of changing the public statement, keeping statements close to the textbook.
• Polynomial invariants by linear algebra: PILAT computes polynomial loop invariants by linear algebra for solvable loops, but the invariants are correct only over rationals and overflow is not modeled.
• Introducing H, an Institution-Based Formal Specification and Verification Language: H separates Hspec (institution-based spec language with modal dynamics) from Hver, which translates specifications to first-order logic; it is a survey.
• Verified iptables Firewall Analysis and Verification: A verified iptables analysis needs a precise semantics first, then semantics-preserving simplification, then a small model that is practical to analyze.
• Different Maps for Different Uses. A Program Transformation for Intermediate Verification Languages: Splitting IVL maps by an over-approximated last-write relation removes exponential case splits from index aliasing, where a missed dependency would be unsound and a false one costs only precision.
• How We Built Cedar: A Verification-Guided Approach: Verification-guided development used a Lean model as spec with differential random testing and property testing; it found 25 bugs and separates model error from code divergence.
• Gradual C0: Symbolic Execution for Gradual Verification: Gradual C0 emits only the run-time checks that optimistic symbolic execution cannot discharge, cutting overhead 11-34% versus fully dynamic checking.
• Software Dataplane Verification: Symbolic execution summarizes each pipeline element and composes summaries to prove crash-freedom, valid only when elements share no mutable state.
• Principles for Verification Tools: Separation Logic: Separation-logic tool built from algebraic layers in Isabelle, with soundness proofs linking control-flow rules to a concrete heap model; reusable for Verus by analogy.
• Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems: Breach is a simulation-based hybrid-systems toolbox for approximate reachability, parameter synthesis, and robust STL monitoring; results are approximate, not exhaustive.
• An experimental Study using ACSL and Frama-C to formulate and verify Low-Level Requirements from a DO-178C compliant Avionics Project: Industrial DO-178 case study writes low-level requirements in ACSL and verifies them with Frama-C WP and Alt-Ergo, but only partially.
• Equivalence Checking of ML GPU Kernels: Volta checks output equality of reference and optimized GPU kernels across all inputs under structured-CTA restrictions, also detecting races and deadlocks, with confluence checked in Agda.
• VerifyThis 2019: A Program Verification Competition (Extended Report): In a human verification competition, representation choices mattered most: immutable sequences avoided permission reasoning, and SMT proofs needed specs shaped for automation.
• Reasoning about External Calls: Protection assertions and scoped invariants let trusted modules keep their properties when calling untrusted external code.
• Horn-ICE Learning for Synthesizing Invariants and Contracts: Horn-ICE learns invariants and contracts where plain ICE samples fail with calls or concurrency, because Horn counterexamples capture joint implication among unknown annotations.
• VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL: VeriCHERI reduces 2-safety noninterference over CHERI RTL to 1-safety with a symbolic protected address, and a weak capability-monotonicity invariant proves exhaustive security with as few as 4 unbounded properties.
• Deductive Verification of Unmodified Linux Kernel Library Functions: Frama-C proved 23 of 26 unmodified Linux string and memory functions, but contracts ended up 2.6 times the library source, since kernel docs are incomplete and specs follow the implementation.
• End-to-End Formalization of Quantum Error Correction: Lean-QEC reduces a stabilizer-code distance bound to SAT and checks an LRAT certificate in Lean; the SAT solver itself stays outside the trusted base.
• Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security: Retrofitting IVL verifiers with a modular product-program construction checks noninterference; soundness needs an operationality condition on the encoding.
• Verification Algorithms for Automated Separation Logic Verifiers: Five separation-logic algorithms in Viper have 5 to 14% incompleteness on a 537-program benchmark, and their strengths are complementary, so no single algorithm dominates.
• Fifteen Years of Viper: Viper’s 15-year record shows one intermediate language with 12+ frontends, where backend disagreement exposes bugs, but every feature must be automatable in both backends.
• Symmetry and Model Checking: Quotienting the state graph by a symmetry group preserves CTL* and mu-calculus truth when the group respects both transitions and the formula.
• Why does it fail? Explanation of verification failures: Failed SAT-based verification is explained in domain-model vocabulary by unfolding definitions into explanation trees, since raw counterexamples contain millions of booleans.
• Cuvée: Blending SMT-LIB with Programs and Weakest Preconditions: Cuvée extends SMT-LIB with weakest-precondition terms over abstract programs and uses loop pre/postconditions instead of invariants, lowering annotation burden.
• Deductive Verification via the Debug Adapter Protocol: Exposes deductive verification through the Debug Adapter Protocol so symbolic execution paths appear as debugger threads, in SecC with VS Code.
• Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses: Tree-manipulating programs are encoded as knitted trees, and memory safety reduces to CHC satisfiability with bounds on spare nodes and history length.
• Federated Formal Verification: Cross-Backend Citation, Cross-Axis Convergence, and AI-Orchestrated Proof Dispatch for Production Systems: Raft campaign cut 26 ASSUME axioms to 0 in 17 hours using build-gated citations to external provers; the AI layer is untrusted proof search, and CI checks closure and absence of Admitted/Axiom.
• Techniques for formal modelling and verification on dynamic memory allocators: Set-based invariants I1-I6 model dynamic memory allocators, giving a step-by-step method for allocator verification.
• Modular Verification of Autonomous Space Robotics: Connects heterogeneous robot-node verification results through first-order-logic assume-guarantee specifications and temporal reasoning.
• Compositional Invariant Generation via Linear Recurrence Analysis: Linear recurrence analysis builds loop summaries compositionally, giving sound over-approximated invariants rather than exact ones.
• VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checks: VeriCoT autoformalizes each reasoning step to SMT-LIB and checks entailment with Z3, verifying only 15.2% to 45.2% of chains but reporting 84.3% to 94.1% precision on verified ones.
• Certificate-Aware Property-Directed Reachability: Learned search choices stay untrusted: report safe or unsafe only after an independent checker accepts the inductive invariant or the counterexample trace.
• Towards Concurrent Quantitative Separation Logic: chpGCL combines concurrency, pointers, and randomness; weakest resource-safe liberal preexpectations give sound lower bounds on postcondition probability.
• Why3 — Where Programs Meet Provers: Why3 sends verification conditions from the first-order WhyML language to many external provers, using encodings for missing features and static alias control instead of a memory model.
• Specification Decomposition for Reactive Synthesis: Decomposes LTL specs with disjoint outputs, synthesizes each part, and composes them; LTL decomposition finished in under 26 ms on every SYNTCOMP 2020 benchmark.
• The Use of Likely Invariants as Feedback for Fuzzers: Corpus-derived likely invariants can guide fuzzers, and their violations flag states outside observed behavior; they are not proofs.
• Staged Specification Logic for Verifying Higher-Order Imperative Programs: Higher-order staged specification logic captures unknown function behavior as stages; a Verus adaptation would need ghost state, which is untested.
• Verification of PCP-Related Computational Reductions in Coq: Coq formalizes undecidability reductions (TM to PCP and others); the core work is finding inductive invariants that make each reduction function correct.
• Unifying Theories of Reactive Design Contracts: UTP theory of reactive design contracts; refinement reduces to three implications over pre-, peri-, and postconditions, mechanized in Isabelle/UTP.
• Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs: The Isabelle hybrid-program framework adds an algebraic store model and shallow expressions, giving simpler syntax and faster proofs for ODE-based correctness.
• Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL: Isabelle/ITrees unify executable models and deductive verification over one semantics, closing the gap between them.
• Foundational Refinement Proofs for Deployed Bytecode, at the Price of Tokens: LLM agents produce Lean refinement proofs relating deployed EVM bytecode to readable specs, and the kernel checks them, so the LLM and tactics stay untrusted for soundness.
• EthBMC: A Bounded Model Checker for Smart Contracts: A bounded model checker encodes EVM exploit goals as SMT and asks for concrete exploit transactions; the claim is bounded, not unbounded.
• Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy: One large inductive invariant can be replaced by a sequence of simpler forward, backward, and prophecy steps, and each incremental proof translates back to one safe invariant.
• A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs: A type system with inference plus model counting decides higher-order masking security for arithmetic programs under the ISW d-threshold probing model.
• Verification of Compiler-to-Accelerator Mappings for Machine Learning Accelerators: Bolt checks compiler-IR-to-accelerator MMIO equivalence via aligned product programs against a formal hardware semantics.
• The LLMbda Calculus: AI Agents, Conversations, and Information Flow: LLMbda is a Lean 4 information-flow calculus where untrusted text reaches later LLM receive steps only through labelled history, with a probabilistic noninterference theorem.
• A Framework for Proof-carrying Logical Transformations: Why3 transformations emit certificates whose leaves are the resulting tasks, checked in OCaml or Lambdapi, which removes over 17,000 lines of OCaml transformation code from the trusted kernel.
• TorchLean: Formalizing Neural Networks in Lean: One shared computation graph with a formal denotation serves spec, execution, and autodiff, and external artifacts are checked against its semantics rather than accepted by fiat.
• Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions: A refinement from a concrete LTS to an abstract transaction LTS, with history variables, needed 10.3k lines of Isabelle for 108 invariants and no model-checking bound.
• Interface Generation and Compositional Verification in JavaPathfinder: An L* learner with a model-checking teacher learns a component interface automaton that is safe and permissive, then serves as an assume-guarantee assumption in JPF.
• A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols: Runs Tamarin on every two-way Noise handshake and reports, per claim, the strongest threat model under which it holds, not a binary verdict.
• Velvet: A Foundational Multi-modal Verifier for Imperative Programs in Lean: A property-based tester that checks pre implies post on generated inputs finds spec bugs before proof effort, and Velvet’s verification conditions are plain Lean theorems.
• IODINE: Verifying Constant-Time Execution of Hardware: IODINE verifies clock-precise constant-time Verilog under usage assumptions and found two timing violations in five verified designs.
• Verifying x86 Instruction Implementations: Centaur’s ACL2 framework verifies one x86 instruction at a time, avoiding whole-pipeline invariants by decomposing around a stable architectural step.
• Certified Verification of Relational Properties: Relational VCGen gives each run its own memory state, composing per-command formulas for properties such as non-interference and monotonicity.
• Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version): Partial graphs form a partial commutative monoid that gives separation logic for graph algorithms, and PCM morphisms localize reasoning deep inside specs.
• The Design and Algorithms of a Verification Condition Generator: Thesis on Boogie-style VC generation: flowgraph and AST architecture, WP and SP generation, and incremental VC pruning; the VC generator is a trusted component.
• A monadic framework for relational verification: applied to information security, program equivalence, and optimizations: Relational verification in F* reifies terminating effectful code into pure monadic functions and proves relations by induction and SMT, but reification limits it to ghost or spec code.
• Le chameau et le serpent rentrent dans un bar : vérification quasi-automatique de code OCaml en logique de séparation: gospel2viper translates Gospel-annotated OCaml to Viper, sidestepping Why3 alias restrictions on recursive mutable types with permission-based separation logic.
• SAIL: Sound Abstract Interpreters with LLMs: LLM-written abstract transformers are accepted only after a soundness check, and repair alone leaves most transformers unsound, so a generate-validate-counterexample-refine loop is needed.
• Precise Reasoning about Container-Internal Pointers with Logical Pinning: Logical pinning lets a client prove a cached pointer into a container stays valid across writes, by marking subparts as pinned or borrowed without changing the separation logic.
• Verified and Optimized Implementation of Orthologic Proof Search: Coq-verified orthologic proof search turns exponential search into a quadratic one via verified memoization, then uses reflection or proof-producing tactics.
• The SeaHorn Verification Framework: SeaHorn splits into front end, CHC middle end, and back-end engines, so a new language needs only a front end, with memory-model precision tiers from registers to partitioned heap.
• Review of Recent Heap Specification and Verification Techniques: A survey of heap verification techniques with no new benchmark; the few numeric claims are second-hand.
• Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools: Survey of contract-based deductive verification with one own measurement: JML binary search in KeY took about one expert hour to specify and verify, then about 6 seconds to run automatically.
• Machine-checking Multi-Round Proofs of Shuffle: Terelius-Wikstrom and Bayer-Groth: Compose small Coq-encoded protocols to prove a larger protocol inherits security, machine-checking Terelius-Wikstrom and Bayer-Groth shuffles.
• Developments in Formal Proofs: Automated procedures prove about 40% of Mizar theorems and 47% of HOL Light/Flyspeck theorems.
• Cooperative Verification via Collective Invariant Generation: A master verifier delegates loop-invariant generation to black-box helpers and validates their witnesses first, but injected invariants can help prove safe tasks and cannot refute.
• (Nearest) Neighbors You Can Rely On: Formally Verified k-d Tree Construction and Search in Coq: Coq verifies quickselect, k-d tree construction, and KNN search, specifying properties with list permutations.
• Verification of a Generative Separation Kernel: Muen-generated separation kernels are verified by conditional parametric refinement, which proves once that a concrete program refines an abstract one when a separately checked generator condition holds.
• Incompleteness of AI Safety Verification via Kolmogorov Complexity: For any fixed sound verifier, some true policy-compliant instances cannot be certified beyond a threshold.
• For a Few Dollars More: Isabelle refinement framework proves functional correctness and worst-case complexity together, down to LLVM; the verified introsort runs in time comparable to libstdc++.
• Decidable By Construction: Design-Time Verification for Truly Fearless Systems: Composer lowers Clef to CPU, GPU, NPU, and FPGA while retaining proof obligations, organized in four verification tiers.
• When Regression Verification Meets CEGAR: Saves state-based procedure summaries from one CEGAR run and reuses them on later revisions, reporting 31.4% less verification time on Linux driver revisions.
• Scalable Verification of Quantized Neural Networks (Technical Report): Verifies fixed-point quantized networks by encoding k-bit arithmetic (sum, bit-shift rounding, bounded ReLU) and checking an implication over the admissible input domain.
• PRISM: A Tool for Automatic Verification of Probabilistic Systems: PRISM builds finite probabilistic models (DTMCs, MDPs, CTMCs) from high-level descriptions and computes quantitative properties.
• Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification: F*/Low* techniques specialize generic verified code to zero-overhead C; HACL* has 105k lines of F* generating 72k lines of C.
• Aquarium: Cassiopea and Alewife Languages: Aquarium separates Cassiopea machine descriptions from machine-independent Alewife specs, so abstract specs can be lowered for synthesis and verification.
• Voting Method Synthesis on an Infinite Domain: A Possibility Theorem for Positive Involvement: CHCs and polyhedra synthesize a four-candidate voting method over unboundedly many voters, with a Lean-checked proof.
• Regular Abstractions for Array Systems: Overapproximates array systems as string rewriting over indexed-predicate bits, enabling regular model checking of parameterized protocols.
• Completeness for a First-order Abstract Separation Logic: Abstract separation logic with abstract points-to is sound and complete for an abstract semantics that contains standard SL as an instance.
• Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols: Synthesis with uncomputable symbols via model-based projection is complete only for theories with quantifier elimination, and maximal solutions may not be finite.
• Program Synthesis in Saturation: Vampire extracts a computable program from a proof of an existential spec using answer literals, so the synthesized program is correct by construction for the proof’s branches.
• 2LS: Heap Analysis and Memory Safety (Competition Contribution): 2LS combines bounded model checking, k-induction, abstract interpretation, and template synthesis for C, adding joint shape and content reasoning for heap memory safety.
• Towards Porting Operating Systems with Program Synthesis: Aquarium searches for machine-dependent OS instruction sequences that satisfy a contract specialized from a machine-independent spec.
• Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis: VeriSynth translates zkEVM opcodes into Python and Z3 transition models, detecting 87 of 95 injected bugs versus 44 for direct LLM prompting, though unsat covers only the modeled state.
• Translating Scala Programs to Isabelle/HOL: Connects Leon to Isabelle/HOL by turning verification conditions into Isabelle lemmas checked by a minimal kernel.
• VEL: A Formally Verified Reasoner for OWL2 EL Profile: Formalizing an EL++ reasoner in Coq revealed errors in the original completeness proofs and forced algorithm changes.
• Industrial-Strength Verification of Solid State Interlocking Programs: SafeCap verified 26 real railway interlockings by checking the response-computation stage of the interlocking loop; an industrial deployment report.
• Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium: A zero-sorry Lean formalization still had a statement bug, since ContDiff with infinite smoothness means analytic in Mathlib, so compilation alone is not correctness.
• Structural Temporal Logic for Mechanized Program Verification: Ticl encodes co-inductive proof techniques as structural lemmas in Rocq, so proofs focus on variants and invariants.
• Deciding Entailments in Inductive Separation Logic with Tree Automata: Entailment between inductive separation-logic predicates reduces to tree-automata inclusion; the fragment is EXPTIME-complete.
• Computer-Assisted Verification of Four Interval Arithmetic Operators: Splitting two timed-out multiplication verification conditions into 26 subgoals let Alt-Ergo and Coq prove interval arithmetic over IEEE floats.
• Compositional Test Generation of Industrial Synchronous Systems: Treats a test as a counterexample and builds a deductive proof tree that combines assume-guarantee and temporal decomposition for Simulink/Lustre systems.
• Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware: Lean proofs show masked NTT pipelines compose with fresh masks at every stage, for every positive modulus, with no sorry or axioms.
• Tridirectional Discriminating-Power Formal Verification of Smart Contract Reentrancy Defense Against Production-Deployed Solidity Source: Lean 4 proofs check the OpenZeppelin reentrancy guard against DAO, Compound, and Aave models with 13 machine-checked theorems and no sorry.
• Understanding the Usability of Cryptographic Verification Tools: A 16-respondent survey of Tamarin and ProVerif users is descriptive evidence about usability, not a tool benchmark.
• Foundational VeriFast: Pragmatic Certification of Verification Tool Results through Hinted Mirroring: VeriFast emits a Rocq proof script by hinted mirroring, where a small Rocq checker replays recorded verifier decisions, so the hints stay untrusted.
• A comprehensive, formal and automated analysis of the EDHOC protocol: SAPIC+ compiles one EDHOC model to ProVerif, Tamarin and DeepSec; most properties hold in the basic model, but weaknesses appear with advanced primitives and compromise.
• Skipping Refinement: Skipping simulation handles optimized systems where one concrete step does several abstract steps, and well-founded skipping gives a local rule that is sound and complete for it.
• Incorporating Data Dependencies and Properties in Difference Verification with Conditions (Technical Report): diffDP uses data dependencies and the property to compute a tighter overapproximation of changed paths for repeated verification.
• Establishing Browser Security Guarantees through Formal Shim Verification: Verifies only a small mediating kernel: 859 lines of Coq kernel with 4,383 lines of proofs protect about 969k lines of WebKit; tab non-interference covers only interference from the kernel.
• Adjoint Natural Deduction (Extended Version): Adjoint natural deduction unifies linear, affine, strict, and intuitionistic logics via modes and a preorder, with a computational interpretation.
• Fictional Separation Logic: Fictional separation logic demands only abstract disjointness, hiding shared memory behind representation predicates, but it is sequential only with worked examples and no benchmark.
• AI for Mathematics: Progress, Challenges, and Prospects: Survey thesis: the prover checks the formal statement, not that it matches intent, so autoformalization is the hard part and a passing proof covers only the stated contract.
• Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents: Iris-style separation logic over a RISC-V instruction model verifies the xv6 ELF rather than C source, finding 10 xv6 bugs under a safety-only guarantee.
• PKind: A parallel k-induction based model checker: PKIND runs k-induction and invariant generation as parallel asynchronous processes for Lustre invariant checking.
• A User Study for Evaluation of Formal Verification Results and their Explanation at Bosch: A Bosch study tests whether pattern-based counterexample explanations help engineers understand model-checker results, using a 41-person questionnaire and a 13-person pre/post experiment.
• Insider threats and auctions: formalization, mechanized proof, and code generation: Isabelle Insider framework formalizes auction insider threats and proves the specified protocol excludes sweetheart outcomes.
• Transport via Partial Galois Connections and Equivalences (Extended Version): Isabelle framework transports functions proved on one type to another via partial Galois connections, covering lists and finite sets.
• Code Mutation in Verification and Automatic Code Correction: Genetic-programming mutations find a parameterized protocol architecture that livelocks and repair code, retaining found architectures as regression checks.
• Logos: Certified Order-Sensitive SQL Rewrites with Mechanized Semantics and LLM Guidance: Order-sensitive SQL rewrites are sound only when every permutation of each outcome is legal, so proof agents must check bag closure before ignoring order.
• From Model Checking to Runtime Verification and Back?: Turns a model checker into a runtime verifier by letting one execution use the host OS, then recording the interaction so the checker can replay and explore alternatives.
• O-Forge: An LLM + Computer Algebra Framework for Asymptotic Analysis: O-Forge has an LLM propose domain decompositions while Mathematica Resolve checks each piece by quantifier elimination, accepting a global asymptotic claim only when every piece returns True.
• Usability of AutoProof: a case study of software verification: AutoProof case study re-implements a Tokeneer protocol in Eiffel with 38 proof obligations; an experience report with no timing or user study.
• VeriFlow: Verifying Network-Wide Invariants in Real Time: VeriFlow checks network-wide invariants incrementally on each rule update, rechecking only packet classes whose behavior may change.
• Formal Verification of Voting Schemes: Develop verified voting schemes incrementally: start simple, add complexity as errors and practical limits appear, combining deductive verification and bounded model checking.
• seL4: Formal verification of an OS kernel: seL4 refines an abstract spec to C; the trusted base includes the compiler, assembly, boot code, and hardware, and the proof does not show the spec matches user expectations.
• An Overview of the HFL Model Checking Project: Reduces higher-order program verification to HFL(Z) model checking with CHC and higher-order model-checker backends.
• A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs: Isabelle verifies interval iteration for MDPs down to LLVM with IEEE 754 directed rounding, preserving bound correctness.
• Automatic Abstraction in SMT-Based Unbounded Software Model Checking: Spacer combines bounded model checking, proof-based abstraction, and CEGAR; safe proofs of under-approximations generalize after a loop check, and invariants come from a Houdini-like maximal inductive subset.
• [TRX: A Formally Verified Parser Interpreter](https://doi.org/10.2168/lmcs-7(2:18): TRX is a Coq-verified PEG parser interpreter with total correctness; its certified version is slower than the unverified one (128.9 s vs 40.0 s on XML).
• The Essence of Higher-Order Concurrent Separation Logic: Iris reduced to a small base logic with the program-spec layer derived; soundness and weakest-precondition adequacy are formalized in Coq, and resource algebras model ownership and ghost state.
• A verified low-level implementation and visualization of the adaptive exterior light and speed control system: A MISRA C implementation of an ABZ 2020 light and speed control system, checked with tests and CBMC; the authors call it a baseline, not a formal development.
• Closing the Loop on LLM-Generated RTL Assertions with Quality-Aware Formal Verification: Mutation-guided refinement tests LLM-written RTL assertions by injecting faults and refining until the effective kill rate reaches 85%, since assertions can pass for the wrong reason.
• CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version): Randomized search optimizes assembly without trust; only the final output is checked by a Coq-proven equivalence checker.
• Semantics for 2D Rasterization: A Lean semantics for a Skia 2D subset that assumes away anti-aliasing and rounding.
• Formal Verification of Probing Security via Conditional Independence: Lilac separation logic reduces probing security to conditional independence A ⟂ C given B, so simulator existence is proved by ownership-based separation.
• A Tale of Two Worlds, a Formal Story of WireGuard Hybridization: Hybrid-WireGuard breaks a property only if WireGuard and PQ-WireGuard star break it with the same keys; verified with ProVerif, DeepSec, and Tamarin via SAPIC+.
• SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs: SYMDIFF checks partial equivalence of program versions via Boogie, using uninterpreted callees whose summaries count as assumptions unless the callees are proved equivalent.
• LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization: A Lean declaration can compile with no sorry and still formalize the wrong claim, so LeanFlow adds a source blueprint and a statement skeleton that type-checks before proofs.
• Learning Guided Automated Reasoning: A Brief Survey: Survey of learned guidance for ATPs, ITPs, and tableaux; learning changes efficiency, not soundness, so proof acceptance stays with the prover.
• Pragmatic Uses of AI in Formal Methods–Based Railway Projects: Early Lessons and Perspectives (Extended Abstract): Four railway activities found AI feasible for B-method proof support and formalization, but LLM outputs need systematic verification before engineering use.
• Towards verified stochastic variational inference for probabilistic programs: Static analysis discharges one SVI model-guide assumption for Pyro programs; violating these assumptions can break the optimization objective.
• Incorrectness Separation Logic with Arrays and Pointer Arithmetic: Extends Incorrectness Separation Logic to arrays and pointer arithmetic with relative completeness, so under-approximate bugs such as freeing array+1 become reportable.
• Developing a Numerical Algorithm with CIVL Model Checking in the Loop: Writing verifying properties first and checking them at each prototype stage made CIVL a design guardrail for a numerical algorithm.
• STORM: Refinement Types for Secure Web Applications: STORM checks data-dependent access policies at compile time using refinement types; the formal guarantee covers a simplified calculus, not the full implementation.
• A Polymorphic Intermediate Verification Language: Design and Logical Encoding: Boogie 2 encodes typed heaps as polymorphic maps, which assume no extensionality, so any user extensionality axioms are trusted assumptions.
• VIP: verifying real-world C idioms with integer-pointer casts: VIP adds an explicit provenance-copy model so C programs with integer-pointer casts can be verified under PNVI-ae-udi, which previously had no verification tools.
• [Simulating reachability using first-order logic with applications to verification of linked data structures](https://doi.org/10.2168/LMCS-5(2:12): Encodes transitive closure into first-order provers for linked structures; proving the over-approximation proves the property, but a failed proof may just reflect incompleteness.
• A Bi-Directional Extensible Interface Between Lean and Mathematica: Results from Mathematica can be verified in Lean or used as untrusted oracles; the user chooses per result.
• Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan-Fourier theorem: Isabelle/HOL formalizes Budan-Fourier and extends root counting to half-planes and balls, at about 6000 lines of proof.
• Spoq: Scaling Machine-Checkable Systems Verification in Coq: Spoq generates Coq specs and refinement proofs for unmodified C and assembly without an LLM, cutting manual Coq from 33.5K to 7.0K lines, though generated specs may be too complex.
• LLVM Translation Validation Automated with Large Language Models and Lean: LLM-written Lean scaffolds for LLVM translation validation added 26 proofs on matched cases while cutting mean proof time 75.9%, and the Lean kernel checks every verdict.
• An Abstract Contract Theory for Programs with Procedures: Abstract assume-guarantee contract theory that takes procedures as the composition unit, defined semantically over state relations.
• Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic: An LLM translates code into a pure functional model that a prover checks, and counterexamples expose missing preconditions and modeling gaps, though translation fidelity is not guaranteed.
• Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification: Forward symbolic execution for unstructured binary programs, with soundness proved in HOL4.
• Sound State Encodings in Translational Separation Logic Verifiers: Translational separation logic verifiers can be proved sound for state encodings where one source resource maps to many IVL representations, and the violated requirements explain past bugs in Prusti, Nagini, and VerCors.
• A Formal Analysis of Apple’s iMessage PQ3 Protocol: A Tamarin model of Apple’s PQ3 checks secrecy and authentication against an active adversary, with the KEM integrated into the ratchet itself.
• Finite Model Finding for Parameterized Verification: Safety of parameterized systems reduces to finding a finite counter-model of a first-order formula, relatively complete for a class of linear arrays.
• Verification of Programs via Intermediate Interpretation: Verifies a program by supercompiling a self-interpreter specialized to the program model, turning the safety property into a syntactic check on the residual program.
• VMDV: A 3D Visualization Tool for Modeling, Demonstration, and Verification: VMDV renders proof trees and counterexamples in 3D with interactive focus, replacing the text output of provers.
• Minotaur: A SIMD-Oriented Synthesizing Superoptimizer: Minotaur synthesizes SIMD rewrites by cutting a function into residual and loop-free parts, synthesizing the cut, and composing refinement, with Alive2 checks.
• Property Preserving Abstractions for the Verification of Concurrent Systems: Galois-connection abstraction plus simulation: a verified property on the abstract system implies the same property on the concrete system for the stated fragment.
• Compositional Symbolic Execution for the Next 700 Memory Models: Rocq foundation for compositional symbolic execution parametric in the memory model, giving soundness for over- and under-approximate verification.
• Proving Cutoff Bounds for Safety Properties in First-Order Logic: Proves a cutoff k so that checking finite domains of size at most k establishes safety for all domains; useful when safety holds only for finite structures.
• Multi-agent Autoformalization of Tensor Network Theory: A synchronized LaTeX blueprint linking source theorems to Lean declarations, checked by tooling, lets reviewers audit a large Lean development without reading all of its code.
• Tractable Verification of Model Transformations: A Cutoff-Theorem Approach for DSLTrans: For a monotone model-transformation fragment, bounded SMT verification is complete: every violation has a witness bounded by the transformation, not the input model.
• VeriPy Source-Preserving Verification and Compatibility Checking for Python Components: Python verification keeps source, contracts, and proof hooks linked, and guarantees hold only within the admitted fragment: “An import statement by itself grants no proof authority.”
• Rtl2lean: Automated RTL-to-Lean Translation with Hierarchical Theorem Generation and Lemma Reuse: A bottom-up layered lemma base for hardware state machines lets an LLM propose intermediate lemmas only when a base case fails, and the Lean kernel accepts each candidate.
• Towards Practical Requirement Analysis and Verification: A Case Study on Software IP Components in Aerospace Embedded Systems: Aerospace requirements are translated to LTL and checked by CBMC, CPAChecker, and KLEE on five small C components, but the paper measures no translation accuracy.
• DR. CHECKER: A Soundy Analysis for Linux Kernel Drivers: DR. CHECKER is soundy: it trades soundness for scale on 437 Linux drivers, reporting 158 unknown bugs with 78% precision.
• Ave: Guiding Agentic GPU Optimization Using Data-Flow Invariants: Ave tags tensor elements with symbolic data-flow labels that survive staging, swizzling, and pipelining, so compile-time Z3 checks can guard LLM GPU-kernel transformations with no runtime overhead.
• MirrorShard: Proof by Computational Reflection with Verified Hints: MirrorShard gives Coq a proven-sound reflective decision procedure with verified hints, so the trust base stays at the kernel instead of per-goal proof traces.
• NeuroCodeBench: a plain C neural network benchmark for software verification: NeuroCodeBench has 32 plain-C neural networks and 607 properties; six SV-COMP verifiers show incomplete math.h support and struggle on the set.
• Floating-Point Neural Network Verification at the Software Level: Eight C verifiers often return incorrect results on floating-point neural networks; NeuroCodeBench 2.0 (912 examples) exposes these gaps.
• Formal Verification of Station Keeping Maneuvers for a Planar Autonomous Hybrid System: KeYmaera X verifies a hybrid station-keeping law for a planar vehicle, discharging reachability and safety obligations.
• Compositional Verification in Rewriting Logic: Rewriting logic gains independent components and a parallel-composition operator that synchronizes named properties, enabling reusable compositional specs.
• VeGo: Direct Deductive Formal Verification of Go Programs for Computer Science Education: VeGo verifies Go programs with specs in comments and claims CLRS-style suite programs verify, but the benchmark claim is the paper’s own and loops need invariants and variants.
• Verifying Isolation Levels of Database Implementations for Free Using Separation Logic: Any implementation verified against separation-logic specs implements its isolation level for free, but the result is conditional on verified clients and trusted Rocq and Iris definitions.
• Decidable Verification of Uninterpreted Programs: Verifying programs with uninterpreted functions becomes decidable only under coherence, meaning memoized terms and early assumes, and coherent verification is PSPACE-complete.
• Nola: Later-Free Ghost State for Verifying Termination in Iris: Nola is an Iris library for total correctness under Rust-style ownership, where invariant opening without later is unsound, with a Rocq mechanization and no benchmarks.
• Ivy: A Multi-modal Verification Tool for Distributed Algorithms: Ivy isolates with hidden state and decidable VCs, and ghost code is erased after it terminates, a design model for private state in a verified module.
• FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean: Compilation alone can certify a distorted physics statement, so the pipeline has an expert check alignment before formal code generation and a compiler-driven correction loop after.
• Mechanizing Refinement Types: Mechanizes the lambda-RF refinement calculus metatheory in LiquidHaskell, proving type safety through a staged development.
• BEval: A Plug-in to Extend Atelier B with Current Verification Technologies: An Atelier B plug-in sends unprovable obligations to ProB and turns a true result into a reusable Atelier B proof rule.
• Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32: Builds an executable ACL2 FAT32 model incrementally and proves read-over-write: a write is visible at its location and leaves other reads unchanged.
• INPROVF: Leveraging Large Language Models to Repair High-level Robot Controllers from Assumption Violations: INPROVF has an LLM propose robot skills checked for syntax and GR(1) realizability with Slugs, but realizability is the only success criterion, not proof of correct behavior.
• A Formalization of the Mean-Field Derivation of the Vlasov Equation: A green Lean build hid a vacuous theorem whose C-infinity test class collapsed to zero; axiom footprints cannot detect vacuous or unintended statements, so humans must read the statements.
• The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving: Proof IDE combines tactics with human invariants and records point-and-click actions as scripts; the paper reports no completed user study.
• Mizzle: A Complete Concurrent Incorrectness Logic for Preventing False Alarms in Agentic Bug Finding: An LLM bug report carries a machine-checked witness that the bug is reachable, using an incorrectness separation logic, so verifier gating removes false positives.
• Formal Verification of Spacecraft Control Programs Using a Metalanguage for State Transformers: One Haskell-embedded state-transformer semantics serves simulation, symbolic simulation, and SMT proofs for a spacecraft processor.
• Verification of C++ Programs with VeriFast: Design of C++ support in VeriFast, covering constructors, destructors, and virtual calls, with no benchmark.
• Verifying C++ Dynamic Binding: Separation-logic resources track dynamic type through C++ constructors and destructors, so virtual calls dispatch to the constructing class.
• Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion: CompCert loop-invariant code motion is built by composing two simpler verified passes, first-iteration unrolling and global CSE, each proved independently.
• The Trusted Computing Base of the CompCert Verified Compiler: Auditing CompCert’s trusted base by semantic boundary found no bugs in verified parts and most bugs in the last back-end stage, so inventory every trusted piece beside each contract.
• Memory Simulations, Security and Optimization in a Verified Compiler: CompCert-style simulation with memory extensions proves stack canaries, pointer authentication, and tail-call elimination, conditional on existing semantics and axioms.
• Boost the Impact of Continuous Formal Verification in Industry: Continuous formal verification couples CI, regression tests, equivalence checking, and model checking to check each change quickly; a vision paper with no evaluation.
• How the Analyzer can Help the User Help the Analyzer: SPARK progressively discloses why a proof fails, from failing property to counterexample to underlying VC, but the evidence is anecdotal with no user study.
• Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution: Viper’s iterated separating conjunctions use quantified chunks with an inverse function, with injectivity checked at exhale, enabling verification of unbounded array and graph access.
• Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement: Parallel trace abstraction analyzes different program paths concurrently in Ultimate Automizer, evaluated on 14,560 SV-COMP tasks.
• Predictable Verification using Intrinsic Definitions: Intrinsic definitions use ghost monadic maps and quantifier-free local conditions to make heap-structure VCs decidable, with fix-what-you-break repair and soundness proved.
• FO-Complete Program Verification for Heap Logics: Frame logic and separation logic with frame-logic semantics are first-order complete for heap verification, with each formula’s support determining separation by disjointness.
• Autoformalizing Euclidean Geometry: LLMs translate Euclidean theorems to Lean on 173 LeanEuclid problems with an SMT engine for diagram reasoning, but SMT results are not certified by Lean, a trust gap.
• Verifying that a compiler preserves concurrent value-dependent information-flow security: Decomposes the secure-refinement obligation for compiling concurrent value-dependent noninterference, proved sound in Isabelle/HOL.
• The WhyRel Prototype for Relational Verification: WhyRel translates relational biprograms into WhyML and discharges them with Why3 and SMT, needing explicit two-run state models and user alignment hints.
• Forall-Exists Relational Verification by Filtering to Forall-Forall [with appendix]: Reduces forall-exists relational verification to forall-forall via a product program with filter-adequacy checks; Theorem 5.4 gives the reduction.
• Automated Side-Channel Analysis of Cryptographic Protocol Implementations: Lifts binary protocol regions to SAPIC+ with leakage contracts, so Tamarin and ProVerif can find control-flow and memory-access side-channel violations.
• Thirty-seven years of relational Hoare logic: remarks on its principles and history: In relational Hoare logic’s product construction, lockstep alone is inadequate, while eager-lockstep, interleaved, and maximal products are adequate for two-run properties.
• A Formal Semantics for P-Code: P-Code lacks formal semantics; the paper adds an extended language, an executable big-step semantics, and a Haskell interpreter, and notes it cannot be executed without added information.
• Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel: Jitterbug verifies BPF JITs by proving prologue, per-instruction, and epilogue correctness, and it found 16 previously unknown bugs that were upstreamed.
• Verified VCG and Verified Compiler for Dafny: A verified VCG and verified Dafny-to-CakeML compiler in HOL4, motivated by soundness bugs in existing tools.
• Soft Contract Verification: Higher-order symbolic execution treats contracts as symbolic values and proves contract correctness statically; verified programs cannot be blamed.
• OpenBSD formal driver verification with SeL4: Adapts the seL4 Isabelle workflow to a small OpenBSD driver model, using C-to-Isabelle parsing and AutoCorres; a proof of concept, not kernel verification.
• On the Almost-Sure Termination of Probabilistic Counter Programs: One-dimensional probabilistic counter programs admit a decision procedure for almost-sure termination via Markov chain finitization, with no invariants needed.
• APEX: A Verified Architecture for Proofs of Execution on Remote Devices under Full Software Compromise: APEX combines attestation with a hardware EXEC bit, so a remote verifier gets evidence that a program ran atomically and produced its output, even under full software compromise.
• Sharper and Simpler Nonlinear Interpolants for Program Verification: Polynomial interpolants for jointly infeasible nonlinear predicates come from a strict-cone Positivstellensatz and SDP, a useful tool for invariant synthesis in CEGAR.
• Towards a Formally Verified Security Monitor for VM-based Confidential Computing: Method: state a high-level guarantee, refine the architecture down to the implementation, and prove the implementation conforms to the model and preserves invariants.
• Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems: Temporal prophecy refines infinite-state systems with first-order LTL formulas via a tableau, strengthening liveness-to-safety reduction; integrated into Ivy.
• Verifying Functional Correctness Properties At the Level of Java Bytecode: BYTEBACK verifies source contracts after compilation to Java bytecode, so new source features need no deductive-tool update; it emits Boogie.
• Strong-Separation Logic: Strong-separation logic is decidable and PSpace-complete even with magic wand and list segments, unlike standard separation logic.
• Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA: Symbolic execution in HOL4 with HolBA verifies RISC-V binaries and lifts results to RISC-V theorems, showing a source-level ensures says nothing about emitted assembly without a compiler-correspondence proof.
• The Refutation Gap: Certifying Both Halves of an Optimality Claim: An optimality claim needs a lower-bound refutation as well as an upper-bound witness; checked refutations certify 111 of 121 results, and a Lean 4 decide certificate covers the rest.
• End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract: Verifying compiled EVM bytecode in KEVM avoids trusting the compiler, and refining an abstract state-transition proof down to bytecode took about 7 person-weeks.
• A Formal CHERI-C Semantics for Verification: Formal CHERI-C memory semantics in Isabelle/HOL, extracted to OCaml and instantiated in Gillian, catches capability violations that ordinary C tools miss.
• [The Relationship Between Separation Logic and Implicit Dynamic Frames](https://doi.org/10.2168/LMCS-8(3:01): Total heaps with permission masks give separation logic and implicit dynamic frames one semantics, with a theorem that a TPL assertion holds exactly when its SL restriction holds.
• Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version): A Viper-to-Boogie translator emits an Isabelle proof per run, and forward simulation then shows target correctness implies source correctness, for the front end only.
• Coma, an Intermediate Verification Language with Explicit Abstraction Barriers: Coma’s explicit abstraction barrier verifies code above it at every call site and code below once at the definition, so an assert above the barrier forces callers to prove it.
• The Imandra Automated Reasoning System (system description): Imandra requires recursive functions to have ordinal termination measures, and it reuses each termination proof to synthesize an induction principle.
• PBLean: Pseudo-Boolean Proof Certificates for Lean 4: A Lean checker for pseudo-Boolean certificates is proved sound once and run natively, which is fast but trusts the Lean compiler, while explicit proof terms run out of memory on large instances.
• All from One, One for All: on Model Checking Using Representatives: Model checking by exploring representative interleavings; LTL is checkable on the reduced graph when properties are equivalence-robust.
• Automated Soundness and Completeness Vetting of Polygon zkEVM: FreeVer checks soundness and completeness of Polygon zkEVM free inputs by comparing honest and malicious prover executions in the K Framework.
• Desfuncionalizar para Provar: Defunctionalizes higher-order programs into first-order code so an existing Why3 verifier can prove them, without extending the verifier.
• Cameleer: A Deductive Verification Tool for OCaml: Cameleer verifies GOSPEL-annotated OCaml by translating to WhyML for Why3.
• Practical Deductive Verification of OCaml Programs (Extended Version): GOSPEL and Cameleer translate OCaml to WhyML for mostly automated verification; keep code and math views connected while automating routine obligations.
• Automated Verification of Network Function Binaries: Klint verifies network-function binaries against a Python spec and data-structure contracts, returning a proof or counterexample without trusting the compiler.
• Translation Validation: Validates each compiler run by checking a refinement with an inductive simulation mapping, instead of proving the compiler correct once.
• UCLID5: Multi-modal Formal Modeling, Verification, and Synthesis: One modeling language supports Hoare proofs, k-induction, and SyGuS invariant synthesis, where the solver fills a declared function inside a non-inductive invariant.
• Liquid Information Flow Control: Lifty checks information flow with liquid types and synthesizes policy-enforcing repairs; noninterference is mechanized only for the core calculus λL.
• Structuring the synthesis of heap-manipulating programs: SuSLik synthesizes heap-manipulating programs as proof terms of separation-logic entailments, solving 22 benchmarks within 40 s with no sketches.
• CoCon: A Conference Management System with Formally Verified Document Confidentiality: Isabelle-verified kernel generates a Scala program with proved confidentiality and safety; verification took three person-months.
• Verified Low-Level Programming Embedded in F*: A restricted low-level language embedded in F* and compiled to C gives memory safety and functional correctness by proving the translation, not by verifying existing C.
• Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery: SAT solving with LLM-generated code finds an infinite family of doubly saturated Ramsey graphs, with the proofs formalized in Lean.
• Lean-auto: An Interface between Lean 4 and Automated Theorem Provers: Lean-auto translates Lean 4 to ATPs; only its native prover path reconstructs proofs, and other ATP outputs are trusted with a warning.
• Tenspiler: A Verified-Lifting-Based Compiler for Tensor Operations: Verified lifting synthesizes a tensor IR and verifies it with CVC5 over integers and reals, not floats, so the proof does not transfer to machine floating point.
• A Layered Formal Methods Approach to Answering Queue-related Queries: QuASI answers queue queries by intersecting input, output, and drop constraints, with a fast over-approximation layer and an exact SMT layer.
• EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats: EverParse generates F* parsers for tag-length-value formats that are verified safe, correct, and non-malleable, targeting bugs such as Heartbleed and Bitcoin malleability.
• StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator: StarMalloc is a drop-in allocator verified in F* and Steel for memory safety, functional correctness, and thread safety, with verification taking 30 to 40 minutes on a laptop.
• A Programmer-Centric Approach to Program Verification in ATS: ATS puts implementation and proof in one language, erasing proofs after typechecking; evidence is typechecked code listings, with no benchmark.
• Canonical Byte-String Encoding for Finite-Ring Cryptosystems: A Lean proof of a codec’s round trip covers only the abstract spec, not the Rust implementation; a caution on spec-to-code gaps.
• FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving: FLARE has an LLM and ATP produce a Lean certificate that a MILP reformulation holds for every instance, with the universal quantifier explicit so single-instance tests cannot miss bad transforms.
• A cyclic proof system for Guarded Kleene Algebra with Tests (full version): Cyclic proof system for GKAT is sound and complete for deterministic while-program equivalence with regular proofs.
• Optimization of Lyapunov Invariants in Verification of Software Systems: Lyapunov-style invariants computed by convex optimization verify overflow, division-by-zero, and termination in numerical software.
• Bridging Syntax and Semantics of Lean Expressions in E-Graphs: An egg tactic for Lean lets the kernel check each result, so unsound e-graph steps cannot break soundness, though the techniques are only partly sound.
• Size Relationships in Abstract Cyclic Entailment Systems: Cyclic proofs need size progress on infinite paths; trace values and ordinal measures give a global condition that rules out spurious circular reasoning.
• Automated Test Generation and Verified Software: Testing complements formal verification: it exposes compiler bugs and system-context problems, adding diverse evidence rather than competing with proof.
• Developing a Practical Reactive Synthesis Tool: Experience and Lessons Learned: Practical reactive synthesis (Termite) needs user steering in the loop; lesson: combine automation with conventional development flexibility.
• Craig Interpolation in Program Verification: Craig interpolants derived from unrolled-loop prefix and suffix give candidate loop invariants, which still need initiation, consecution, and sufficiency checks on the real loop.
• Verification of Quantitative Hyperproperties Using Trace Enumeration Relations: Counting traces for hyperproperties reduces to counting satisfying assignments of a first-order formula through trace enumeration.
• RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types: RefinedC verifies low-level C via ownership types refined by logical facts, checked in Coq; it proves partial correctness and checks the spec against the code, not that the spec is the intended one.
• A survey of challenges for runtime verification from advanced application domains (beyond software): Runtime verification checks observed executions against monitors, trading completeness for applicability beyond static verification.
• Gillian: Compositional Symbolic Execution for All: Gillian proves soundness of symbolic execution and verification once for an abstract state model, then reuses it per language with memory lemmas.
• TREBL – A Relative Complete Temporal Event-B Logic. Part I: Theory: TREBL is a fragment of Event-B logic for liveness with set-valued updates and sound derivation rules.
• Efficient Verification of Optimized Code: Correct High-speed X25519: An X25519 Why3 proof on AVR starts from a succinct math spec, found an Alt-Ergo 2.0 soundness error, and models the machine as bounded address spaces.
• A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version): Verification preexpectation transformer gives quantitative Hoare triples for probabilistic HeyVL programs; choose the quantitative postcondition first, then translate statements.
• Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version): Statement-deletion slicing gives error localization and verification-preserving slices; the same idea could shrink failing Verus proofs into actionable slices.
• Caesar: A Deductive Verifier for Probabilistic Programs: Caesar verifies probabilistic programs via HeyVL verification conditions checked by Z3, with Storm model checking for a subset.
• Bootstrapping LCF Declarative Proofs: ProofScript converts conjectures to CNF, sends them to METIS, and translates the certificate back into LCF kernel terms.
• Formal Semantics and Program Logics for a Fragment of OCaml: Defines OLang, an OCaml fragment, in Rocq and builds a sound stateless Hoare logic for pure code and an Iris separation logic for arbitrary code.
• Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis: Sciduction pairs a learned candidate with a lightweight deductive checker under a structure hypothesis, so soundness is conditional on that hypothesis, which has no general validity check.
• Automated Verification of Integer Overflow: A separation-logic extension detects integer overflow during proof, finding 43 overflows in 106 programs, and uses specs such as 0 ≤ n+1 < ∞ instead of n ≥ 0.
• HHLPy: Practical Verification of Hybrid Systems using Hoare Logic: HHLPy verifies sequential HCSP with ODE evolution using Hoare logic; an ODE runs until its domain boundary, unlike differential dynamic logic.
• Detecting Multi-Step IAM Attacks in AWS Environments via Model Checking: Encodes an AWS organization snapshot as a finite-state Boolean model and checks adversarial reachability, including explicit denies and SCPs.
• Formal Analysis and Patching of BLE-SC Pairing: Tamarin model of BLE Secure Connections finds method-confusion, downgrade, and keysize-confusion attacks, and shows a patch with residual Passkey weakness.
• Towards platform-independent specification and verification of the standard trigonometry functions?: Specifies trig functions as convergent Taylor series, making truncation error the postcondition for platform-independent verification.
• BesFS: A POSIX Filesystem for Enclaves with a Mechanized Safety Proof: BesFS is an abstract enclave filesystem that aborts on deviations from benign-OS properties, with a mechanized safety proof.
• Certificate-Carrying Transformation of Event-Driven Block Programs: An untrusted optimizer proposes a rewrite and a trusted fail-closed checker recomputes every side condition, so the certificate only carries hints and every non-accept branch rejects.
• Machine-Checked Certificates for the Geometric Half of the Minimum Kochen–Specker Bound: Untrusted search generates exact rational case-tree certificates that a Lean kernel-checked replayer validates, replacing Z3 nonlinear arithmetic that produced no proof objects.
• Verification Challenge: Fractional Cascading for Multi-Nuclide Grid Lookup: A verification challenge: prove a fractional-cascading lookup equals k independent binary searches with cost O(log n + k).
• A Human Audit of OpenAI’s AI-Generated Mathematical Proofs: Human audit of OpenAI’s AI-generated proofs: no confirmed substantive error in a principal result, but chapter 8 is verification-incomplete, and a certificate checks only the encoded proposition.
• Push-Button Verification of File Systems via Crash Refinement: Crash refinement requires every disk state, including crashes and write reordering, to be producible by the spec; idempotent recovery does not guarantee crashes stop.
• Nickel: A Framework for Design and Verification of Information Flow Control Systems: Nickel verifies information-flow security of a spec and C implementation via Z3, where counterexamples expose covert channels, and the policy must be audited against design intent.
• Certifying rlive: A New Proof Strategy for Liveness Model Checking: Certifies rlive liveness results by generating a temporal proof from shoals, so only the theorem prover is trusted.
• Verified Secure Compilation for Mixed-Sensitivity Concurrent Programs: CVDNI is a two-run noninterference property for shared memory whose sensitivity changes with a control mode, used for secure compilation of mixed-sensitivity programs.
• Foundational Verification of Smart Contracts through Verified Compilation: DeepSEA’s verified compiler to EVM, with correctness internalized in Coq so contract specs can be checked against bytecode.
• Language-Based Security for Low-Level MPC: Overture plus the Prelude metalanguage verify small binary-field primitives automatically and larger MPC protocols partially, including GMW noninterference.
• Alias Types: Alias types allow deallocation and type change through linear constraints on symbolic stores, while non-linear constraints model shared locations.
• A Deductive Verification Framework For Higher Order Programs: Why3 plugin translates GOSPEL-annotated OCaml to WhyML via defunctionalization; the prototype proves only pure programs.
• A Framework for the Automated Verification of Algebraic Effects and Handlers: Extends Cameleer to algebraic effects and handlers by encoding continuations with exceptions and defunctionalization.
• Pegasus: sound continuous invariant generation: Pegasus generates sound continuous invariants for polynomial ODEs inside KeYmaera X, checking the initial, preservation, and safety obligations.
• ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts: ESBMC-Solidity translates Solidity AST to ESBMC IR and finds seeded vulnerabilities with counterexamples on eight test cases.
• LeanGeo: Formalizing Competitional Geometry problems in Lean: LeanGeo’s SMT tactic sends geometry goals to CVC5 without reconstructing certificates into Lean, so its proofs carry a trust gap plus 9 extra axioms.
• Automated Verification of Monotonic Data Structure Traversals in C: Shrinker verifies loops that sweep monotonic data structures with abstract interpretation and no LLM, solving 58 of 62 string and 20 of 26 list cases, using scapegoating of size descent.
• Touring the MetaCoq Project (Invited Paper): MetaCoq certifies a Coq type checker in Coq with proved correctness, completeness and erasure, shrinking the trusted base of a proof assistant.
• TäKōFormal: Enabling Robust Software for Programmable Memory Hierarchies: Machine-checked refinement proof: an ISA-level memory consistency model is shown sound against a detailed programmable-hierarchy implementation model.
• StateSync-GKR: Machine-Checking the Trust Chain from Sparse-Merkle State Transitions to GKR Verification: Mechanizes in Isabelle a chain from sparse-Merkle transition semantics through a compiler to GKR soundness, showing acceptance matches the intended semantics.
• All-Path Reachability Logic: All-path reachability logic derives partial correctness from an operational semantics with one premise per semantic rule, avoiding a separate Hoare-style semantics per language.
• Automated Verification of Consistency in Zero-Knowledge Proof Circuits: Defines ZK circuit consistency: a valuation the constraints accept must agree with the witness generator on outputs and satisfy the constraints.
• Transaction Level Hierarchy Guided and Functional Coverage Driven Deductive Formal Verification: Compiles a transaction-level SystemVerilog extension to Coq, so coverage points become theorems and lower-level proofs are reused by higher levels.
• Regression Verification - A Practical Way to Verify Programs: Regression verification checks that a revised program preserves selected behavior of an earlier version, without requiring a full formal specification.
• PAT: Towards Flexible Verification under Fairness: PAT checks LTL under fairness by searching for fair SCCs and modifying prune to handle weak, strong local, and strong global fairness.
• Validating the eBPF Verifier via State Embedding: State embedding turns the eBPF verifier’s over-approximation requirement into a self-checking test by embedding a profiled concrete state the verifier must accept.
• Modular Verification of Interrupt-Driven Software: IntAbs analyzes each interrupt handler in isolation and propagates results to a fixed point, avoiding a monolithic model of interrupt interleavings.
• BarrierBench: Evaluating Large Language Models for Safety Verification in Dynamical Systems: LLM agents synthesize SMT-checked barrier certificates, with Claude Sonnet 4 solving 90 of 100 BarrierBench systems versus 46 for ChatGPT-4o, and retrieval of verified examples guides synthesis.
• Formal Methods for Network Performance Analysis: Bounded SMT modeling plus syntax-guided workload synthesis finds traffic patterns that trigger network performance failures, beyond what simulated traces show.
• SolType: refinement types for arithmetic overflow in Solidity: SolType refinement types prove Solidity arithmetic overflow safety via CHC inference, relating integer sums over data structures to totals.
• Ownership Types for Verification of Programs with Pointer Arithmetic: Extends ownership types with fractional ownership in [0,1] to pointer arithmetic and variable-size arrays; strong updates under aliasing are allowed, and reads through zero ownership are rejected as stale.
• LIGHTYEAR: Using Modularity to Scale BGP Control Plane Verification: Assume-guarantee decomposition reduces a BGP global property to per-edge SMT checks, sound for infinite traces and arbitrary failures.
• DICE*: A Formally Verified Implementation of DICE Measured Boot: A DICE measured-boot engine verified in Low* and extracted to C ran on hardware, with a platform-agnostic interface that isolates device operations as specified external functions.
• A Formal Proof of PAC Learnability for Decision Stumps: Lean/mathlib proof that one-dimensional decision stumps are PAC learnable, with an explicit sample-size bound.
• Modular Verification of Heap Reachability Properties in Separation Logic: Modular heap reachability in separation logic uses ghost footprints and path predicates, but the SMT encoding unfolds path axioms to a fixed depth and can miss deeper proofs.
• Heterogeneous Dynamic Logic: Provability Modulo Program Theories: Heterogeneous Dynamic Logic composes existing dynamic logics as SMT theories are combined, enabling compositional proofs of heterogeneous systems.
• AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction: AssertCoder extracts multimodal hardware spec content and generates SVAs refined by mutation, reaching 87.6% functional correctness versus 79.2% for AssertLLM.
• A Formally Verified Robustness Certifier for Neural Networks: Verified robustness certifier bounds a ReLU network’s margin Lipschitz constant via operator norms, so many outputs certify without a per-input symbolic proof.
• Contextual Linear Types for Differential Privacy: Jazz contextual linear types check differential privacy by composing mechanisms with sensitivity-matched noise placement.
• AutoProof: Auto-active Functional Verification of Object-oriented Programs: AutoProof is an auto-active Eiffel verifier via Boogie that is sound modulo implementation bugs, with loop invariants and framing, and Rust ownership replaces modify and read framing.
• Software Model-Checking as Cyclic-Proof Search: Software model checkers (BMC, PDR, predicate abstraction, Impact) are proof-search strategies for one cyclic proof system, giving a common logical account.
• A Primal-Dual Perspective on Program Verification Algorithms: One Lagrangian primal-dual framework unifies verification searches that alternate proof candidates and counterexamples, with weak duality always holding and termination needing a semilattice update.
• Practical Formal Verification for MLIR Programs: PEQC-MLIR checks translation equivalence with hybrid concrete-symbolic CDAGs and a happens-before graph for races in a restricted language.
• LeanBET: Formally-verified surface area calculations in Lean: A Lean implementation of BET surface-area analysis proves its algebra and least-squares fit, matching the BETSI reference on 18 of 19 isotherms.
• Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny: Layered Dafny proofs of a token sale launchpad reuse proved integer-truncation lemmas, such as R(C(w)) <= w, so refund safety composes from round-trip facts.
• Fast and Reliable Formal Verification of Smart Contracts with the Move Prover: The Move Prover verifies Move contracts automatically via Boogie and Z3 or CVC5, verifying about 6,500 lines of Diem framework specs in minutes because Move’s borrow rules remove aliasing reasoning.
• Formal Proof of SCHUR Conjugate Function: Isolates one 50,000-line C routine, annotates it in ACSL, and verifies it with Frama-C Jessie; a case study on legacy C.
• Modal Verification Patterns for Systems Software: Makes the resource context (address space, actor, crash epoch) an explicit modal dimension so specs follow systems design patterns; a design survey, no evaluation.
• Program Verification via Predicate Constraint Satisfiability Modulo Theories: Predicate constraint satisfiability generalizes constrained Horn clauses to termination and temporal properties, with a sound and complete reduction from mu-CLP validity.
• Constraint-based Relational Verification: pfwCSP extends CHCs with inferred schedulers to verify k-safety and noninterference automatically; PCSat solves it by stratified CEGIS.
• Verification Modulo Tested Library Contracts: VMTLC proves a client against synthesized library contracts that are only tested, so the approach can succeed on incorrect programs.
• Verification of a Smart Contract for a Simple Casino: Verifying a Solidity casino via Java/JML, Whiley, and Boogie found several specification and code issues.
• HaliVer: Deductive Verification and Scheduling Languages Join Forces: HaliVer uses one functional spec for a Halide algorithm and its scheduled code, verifying functional correctness and memory safety through VerCors.
• Abstract Refinement Types: Abstract refinement types quantify over predicates while staying SMT-decidable, so one max function can be checked for any refinement, such as evenness, at each call site.
• Refinement types for TypeScript: Refined TypeScript: lightweight SMT-backed refinements are proved sound for mutation and higher-order functions, with an implementation on real programs.
• Formally Verified Binary-level Pointer Analysis: A binary pointer-analysis framework with concrete, abstract, and concretization maps lets several precision-scalability trade-offs share one correctness proof.
• ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems: Compositional probabilistic verification combines tests, user proofs, and assume-guarantee contracts; the guarantee covers only the simulated system.
• Featherweight VeriFast: Featherweight VeriFast formalizes a core separation-logic verifier subset; the soundness outline is on paper and the mechanized Coq variant is separate.
• Reasoning About Incompletely Defined Programs: A statement about incompletely defined programs holds only if it holds for every completion of undefined calls, and stuck computations model runtime errors.
• Formal Security Analysis of Neural Networks using Symbolic Intervals: ReluVal propagates symbolic intervals through ReLU networks to prove or refute input-bounded properties; the 200x speedup over Reluplex is the authors’ empirical claim.
• Relational Program Synthesis: Relish synthesizes a tuple of programs satisfying relational specs using CEGIS with version-space learning; the paper reports solving almost all benchmarks.
• Proving Differential Privacy with Shadow Execution: ShadowDP turns differential-privacy proofs into ordinary verification via shadow execution, with few annotations and no customized logic.
• CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples: CheckDP produces either a proof or a verifiable counterexample for differential privacy mechanisms, finding bugs prior tools missed.
• From Matching Logic To Parallel Imperative Language Verification: PIMP gets a matching-logic verifier defined as rewrite rules, proved sound and complete on paper; the verifier is not implemented.
• Formal Model Construction Guided by Model-Based Proof Sketches: ProGS builds Event-B models from requirements via a proof-sketch tree, since flat generated events repair poorly and a local fix can break a global property.
• Verification of a Generational Garbage Collector: A Rocq and VST proof verifies a generational copying GC in C, and verifying clients exposed a spec weakness that led to a real C bug, a missing No_scan branch tests never hit.
• Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering: Dafny, FDR4, and Isabelle catch different defects; one model passed Dafny and FDR4 but failed Isabelle, and a vacuity audit rejects obligations that prove true.
• Formal Verification of Minimax Algorithms: Dafny verification of minimax and alpha-beta with transposition tables; cached results from other depths and windows break tree-traversal reasoning.
• Benchmarking Software Model Checkers on Automotive Code: Open-source checkers cover at most 20% of automotive requirements; CBMC with k-induction reaches 63% and the commercial tool 80%.
• mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic: mypyvy is an open platform for FOL transition systems and invariant inference, avoiding SMT theories when possible because combined theories are hard for solvers.
• AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation: One DSL yields an implementation, a Tamarin model, and symbolic tests, and restricting control to a state machine makes extraction sound under Dolev-Yao only.
• Gobra: Modular Specification and Verification of Go Programs: Gobra verifies annotated Go for memory safety, crash safety, and data-race freedom using separation-logic permissions, with interface refinement proofs that follow a repetitive unfold-call-fold pattern.
• End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation: Composes verified and verifying compilation through open safety over labeled transition systems, with module-boundary safety interfaces.
• QCP: A Practical Separation Logic-based C Program Verification Tool: QCP verifies C against separation-logic annotations in comments, auto-solving 1,964 of 2,643 verification conditions and exporting the rest to Rocq.
• VEP: A Two-stage Verification Toolchain for Full eBPF Programmability: VEP moves SMT solving to user space and leaves a small proof checker in the eBPF kernel, so safe but complex programs are not rejected.
• TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples: TraceFix repairs LLM agent coordination protocols from TLC counterexamples, checking deadlock, mutual exclusion, orphan locks, and channel drainage, but not termination or output quality.
• Iceberg: Automated Verification of DNS Authoritative Engines via Just-in-Time Summarization: Iceberg verifies DNS authoritative engines by refinement against only the top-level spec, summarizing each callee in its calling context just in time, so no per-layer manual specs are needed.
• A Natural Formalized Proof Language: ProofGrader checks a natural-language-like formal proof language step by step with modular solvers, but no accuracy or completeness benchmark is reported.
• Generically Automating Separation Logic by Functors, Homomorphisms, and Modules: Algebraic theory generates separation-logic rules from functor and homomorphism properties, with a generic automation solver.
• Scalable Shape Analysis for Systems Code: A partial join merges symbolic heaps aggressively without false error reports, making separation-logic shape analysis scale to industrial device drivers.
• A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-Based Service Smart Contracts: FSPVM-E translates Solidity to Lolisa in Coq and verifies Hoare-style properties, but admits an unguaranteed Solidity-to-Lolisa equivalence.
• PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot: PA-Boot’s authentication protocol is mechanized in Isabelle/HOL with 306 lemmas and about 7,100 LoC, covering AP replacement and interposer attacks.
• Inductive Synthesis of Inductive Heap Predicates: Sippy synthesizes recursive separation-logic predicates from heap instances with positive-only ILP learning, avoiding hard-to-generate negative examples.
• DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols: DuoAI infers inductive invariants with existential quantifiers for Ivy protocols by weakening and strengthening in parallel, solving 26 of 27 protocols, with Ivy or Z3 checking every candidate.
• A Practical Quantum Hoare Logic with Classical Variables, I: QHL+ gives a Hoare logic for quantum programs with classical variables and proves soundness, with relative completeness deferred to a companion paper.
• NetSMC: A Custom Symbolic Model Checker for Stateful Network Verification: NetSMC relaxes network semantics to one packet per state, making symbolic model checking of stateful networks practical.
• Klever: Verification Framework for Critical Industrial C Programs: Klever decomposes large C programs, models environments, and triages SV-COMP verifier results, targeting industrial code.
• Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics: Visored is a controlled-natural-language prover for LLM math that rejects out-of-vocabulary input and turns well-definedness into explicit proof obligations, such as 1/x needing x != 0.
• Verify Implementation Equivalence of Large Models: Emerge puts two model implementations in one e-graph, infers relations from execution values, and validates synthesized rewrite rules by SMT or randomized testing.
• LightDP: towards automating differential privacy proofs: LightDP’s relational type system separates relational reasoning from privacy-budget calculation, reducing differential-privacy proofs to ordinary verification.
• Automated Verification of Customizable Middlebox Properties with Gravel: Gravel symbolically executes C++ middleboxes and checks element refinement and graph composition against trace-based specs.
• Denotation-based Compositional Compiler Verification: Denotational semantics with behavior refinement verifies the CompCert front end; reusable workflow defines behavior sets and source-target correspondence.
• The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmap: LLMs formalize, solvers check, and solver success alone does not show the NL was formalized faithfully; multi-LLM debate and generated tests serve as controls.
• Automatic Verification of Floating-Point Accumulation Networks: Automatic procedure proves FPAN error bounds by one-sided reduction to QF LIA; unsatisfiability proves a property, satisfiability does not refute it.
• On Temporal Verification of Stateful P4 Programs: Verifies temporal properties of stateful P4 programs by finding a fair feasible trace in a Büchi transaction, implemented in p4tv.
• Scope Logic: Extending Hoare Logic for Pointer Program Verification: Scope logic extends Hoare logic for pointers: a virtual value stays unchanged while no memory unit in its scope is overwritten.
• Scope Logic with Local Reasoning and Pre/Post-State Properties: Scope logic with pre-state terms for pointer programs; the paper counts 14 axioms and rules for separation logic and argues its own rules are simpler.
• A survey on formal specification and verification of separation kernels: A survey of separation-kernel verification argues the verification chain should reach the implementation level.
• Verifying Device Drivers with Pancake: A Pancake device driver is verified via Viper, but the transpiler is unverified, so an incorrect source compiled by a verified compiler still yields incorrect machine code.
• Neuro-Symbolic Reasoning for Vulnerability Detection: LEAN GUARD has the LLM edit a constrained fact list while a deterministic translator builds a Lean model the kernel decides, raising F1 in all 15 settings, though it measures detection, not proof.
• Formally Verified Synthesizable Floating-Point Data Types in ARCH HDL: Builds FP32 and BF16 operators once in a Rust DSL rendered to SystemVerilog, SMT-LIB, and Lean, with only round-to-nearest-ties-to-even arithmetic.
• Trace-Tree Magmas: Proof-Producing Infinite Countermodels and 28 New Order-Five Austin Classifications: Synthesizes infinite magma countermodels with self-contained Lean 4 certificates; reports 28 new order-five Austin classifications among ETP’s 96 candidates.
• Beyond Correctness: Exposing LLM-generated Logical Flaws in Reasoning via Multi-step Automated Theorem Proving: MATP checks reasoning traces post hoc by translating each step to first-order logic for Vampire, separating evaluation from generation, with a 99.06% execution rate on PrOntoQA-OOD.
• Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems: UniQQ synthesizes neural barrier certificates, trying almost-sure safety first and falling back to probability bounds if synthesis fails.
• Relational Verification via Invariant-Guided Synchronization: Pequod searches synchronization points and relational invariants together for bounded first-order recursive programs, but loops are out of scope.
• Statically verified refinements for multiparty protocols: Session* checks Scribble multiparty protocols with refinements through F* API generation, statically verifying communication and data constraints.
• Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems: Checks a candidate inductive invariant for NN-controlled systems by splitting one implication into an NN-verifier step and an SMT environment step, joined by a bridge predicate.
• A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata: Hoare Automata Types use symbolic finite automata over traces to verify representation invariants of clients of stateful libraries; Marple uses Z3.
• VUPER: Verified ASN.1 UPER Parser: Rocq framework generates ASN.1 UPER parsers and serializers with proved round-trip properties; it verifies Rocq code, not Rust.
• LeanArchitect: Automating Blueprint Generation for Humans and AI: Blueprint attributes on Lean declarations sync dependencies and sorry-based status into a LaTeX blueprint, with Lean staying the authoritative checker.
• Towards Formal Verification of a TPM Software Stack: Partial Frama-C verification of the tpm2-tss ESAPI subset needed a verified allocator and Coq linked-list lemmas, exposing Frama-C limits.
• Latte: Lightweight Aliasing Tracking for Java: Latte’s type system tracks unique and shared references in Java, inferring local annotations so only parameters and fields need annotations.
• Sound Gradual Verification with Symbolic Execution: Gradual C0 and Viper subset soundness: optimistic static checks plus run-time checks for partial specifications.
• Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification: Gradual exact logic unifies Hoare logic, incorrectness logic, and gradual verification.

Last edited: 2026-11-06