Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python

arXiv:2607.03951 · cs.SE, cs.AI, cs.LO, cs.PL · Submitted 2026-07-04 · Read on arXiv

cs.SE, cs.AI, cs.LO, cs.PL

Submitted: 2026-07-04

Updated: 2026-09-21

Comments: Accepted to SEFM 2026 (International Conference on Software Engineering and Formal Methods)

Code: https://github.com/fm4stats/why3-py

License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

Terminology

• Verification — 49× in this paper · explained in 2 episodes
• Formal Verification — 11× in this paper · explained in 2 episodes
• Abstraction — 2× in this paper · explained in 1 episode
• Verifier — 2× in this paper · explained in 2 episodes
• Core — 1× in this paper · explained in 2 episodes
• SMT solver — 1× in this paper · explained in 2 episodes

Sources

• Dafny as Verification-Aware Intermediate Language for Code Generation
• PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C

Related papers

• Falsification-Based Verification of LLM-Generated Optimization Models: Sound Test Batteries and Their Detection Limits
• GitSkills: A Dataset of Agent Skills on GitHub
• SABER: Benchmarking Operational Safety of LLM Coding Agents in Stateful Project Workspaces
• PackMonitor: Enabling Zero Package Hallucinations Through Decoding-Time Monitoring
• IntentCoding: Amplifying User Intent in Code Generation
• Incentives and Outcomes in Bug Bounties