Aug 2026· Proceedings of the ACM on Programming Languages· Vol 10, pp. 663 - 691· 0 citations· 36 references
TL;DR
This paper provides a formal account of the syntax and semantics of Hedgehog, a popular PBT framework, and proves that Hedgehog→ possesses a compositional distribution semantics, and introduces Hedgehog→, a restricted version of the language based on the arrow calculus, and proves that Hedgehog→ possesses a compositional distribution semantics.
Abstract
Property-based testing (PBT) is a powerful technique for software verification that relies on random input generators and ”shrinking” processes to find and minimize counterexamples to executable specifications called properties. While optimizing these generators is crucial for testing efficiency, formally justifying such optimizations is currently difficult because existing languages lack a compositional semantics that is coarse-grained enough for high-level reasoning. In this paper, we first provide a formal account of the syntax and semantics of Hedgehog, a popular PBT framework. We demonstrate that Hedgehog’s distribution semantics — which models how users typically reason about generators — is non-compositional. Furthermore, we prove that any sound and complete compositional semantics for Hedgehog must necessarily be equivalent to its sampling semantics, which is too fine-grained to justify common program optimizations. To resolve this dilemma, we introduce Hedgehog→, a restricted version of the language based on the arrow calculus, and prove that Hedgehog→ possesses a compositional distribution semantics. We evaluate Hedgehog→ through a Haskell implementation and show that it remains expressive enough to capture generators of practical interest, while providing the formal foundation needed for compositional generator equivalence proofs.
FLEX is presented, a foundational Constrained Horn Clause (CHC) solver implemented in LEAN, that reduces the trusted base to the kernel alone, and allows using LEAN's entire proof ecosystem to verify low-level systems code, via three contributions.
J. Khan, Petros Markopoulos, Nicolás Lehmann et al.· 0 citations
Term rewriting systems are a common tool in automated reasoning and semantics of programming languages, and many practical applications require these systems to be convergent. While automated tools and theory exist to establish convergence, this paper is concerned with a practical method for testing it to quickly find useful counterexamples. Standard property-based testing approaches struggle here: exhaustively computing all normal forms is fundamentally flawed and too slow, while generating random normal forms makes counterexample minimization (shrinking) fragile due to dependencies on earlier generated test data. To solve this, we introduce a QuickCheck testing method based on generating and shrinking random execution traces. By checking if the first and last terms of a generated trace share the same deterministic normal form, we remove the data dependency between generators. This approach yields a property that efficiently finds counterexamples and enables fast, robust shrinking. We demonstrate the effectiveness of this method on various examples, ranging from group theory equations to distributed process calculus.
Koen Claessen· Proceedings of the ACM on Pr...· 0 citations
Formal verification provides strong guarantees of software correctness, but its adoption is limited by the high cost of writing precise formal specifications. While recent large language models (LLMs) have shown strong capabilities in theorem proving and verified code generation, their true ability to generate program specifications remains unclear. Existing evaluations require either verifying implementation conformance or proving semantic equivalence between specifications, both of which are formidably difficult and may conflate proof difficulty with specification quality. To address this problem, we introduce Coins, a Rocq based evaluation framework that assesses specification quality by instantiating specifications under evaluation on trusted test cases and generating concrete proof obligations. This design aligns with the asymmetric nature of formal reasoning, where successful proofs provide reliable evidence while proof failures are inherently ambiguous. Using Coins, we conduct a large scale study on HumanEval with a curated set of human written Rocq specifications. Our results show that specification generation remains a formidable challenge, and that verification complexity can obscure genuine differences in specification quality. Overall, we find that accurate specification evaluation, rather than model scaling alone, is central to understanding the power of LLMs for specification synthesis, and that test case based formal reasoning offers a more faithful and discriminative measure of progress.
Fan Yang, Xing Li, Shuling Wang et al.· 0 citations
SymCert is presented, a framework implemented in Lean for building verified SMT-based analyses of Cedar policies that provide a verified symbolic compiler and authorizer for reducing policies to SMT formulas, a hierarchy enforcer for ensuring well-formedness of counterexamples, and a counterex-ample extractor for proving analysis completeness.