Formal Verification

Ask about this field

Recent momentum

emerging

0 papers in the last 28 days · 0.0% of indexed attention

Twelve weeks of publication activity for this topic as it is defined today.

Weekly history

Recent digests

What was published in this field, kept on the site without email delivery.

Period ending 2026-09-21

17 new papers

A weekly snapshot of new work published in Formal Verification.

Period ending 2026-09-14

18 new papers

A weekly snapshot of new work published in Formal Verification.

Period ending 2026-09-07

22 new papers

A weekly snapshot of new work published in Formal Verification.

Inside this field

Focused directions

608 papers

Latest in Formal Verification

Browse all topics →
CardsList

  1. CAVA: Canonical Action Verification and Attestation for Runtime Governance of Agentic AI Systems

    Jul 15, 2026Zexun WangCanonical Action Verification And AttestationArtificial Intelligence Governance

  2. The Café in Amsterdam: When the Incumbent Becomes the Oracle

    Jul 15, 2026Augusto CamargoComputational CostOracles

  3. Faithful Autoformalization of Natural Language Assertions

    Jul 14, 2026Hongyi Liu, Madhusudan Parthasarathy, Adithya MuraliAutoformalizationSystemverilog Assertions

  4. Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

    Jul 14, 2026Marcus J. Min, Mike He, Zhaoyu Li +5AutoformalizationFormalization

  5. Environment Parameter Gradient Theorem for Policy-Environment Co-Design in Reinforcement Learning

    Jul 14, 2026Amber SrivastavaValue FunctionsGradient Flow

  6. Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization

    Jul 13, 2026Tian-Shuo Liu, Shiyuan Zhang, Zijie Geng +5AutoformalizationTheorem

  7. TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs

    Jul 13, 2026Burak S. Akbudak, Zeynel A. Uluşan, Can S. Erer +1TheoremTree Search

  8. TIGER: Text-Conditioned Visual Gated Routing with Acceptance Alignment for Multimodal Speculative Decoding

    Jul 13, 2026Quynh Vo, Cong-Duy Nguyen, Ponhvoan Srey +2Speculative DecodingModality-Specific Encoders

  9. SVR-R1: Bootstrapping Multi-modal Reasoning with Self-verification in Reinforcement Learning

    Jul 13, 2026Mingyuan Wu, Jingcheng Yang, Shengyi Qian +11Reinforcement Learning With Verifiable RewardMultimodal Reasoning

  10. First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)

    Jul 12, 2026Christoph Benzmüller, Daniel KirchnerModal LogicTheorem

  11. The VC dimension of partial concept classes via Radon's theorem

    Jul 12, 2026Grigory Ivanov, Attila Jung, Márton NaszódiMetric SpacesTheorem

  12. Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability

    Jul 10, 2026Shirley Yu, Ruben MartinsFormal VerificationVerifier

  13. OpenProver: Agentic and Interactive Theorem Proving with Lean 4

    Jul 10, 2026Matěj Kripner, Milan StrakaTheoremFormal Verification

  14. Scoped Verification for Reliable Long-Horizon Agentic Context Evolution under Distribution Shift

    Jul 10, 2026Dan C. Hsu, Luke LuLong-Horizon AgentsLarge Language Model Agents

  15. A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game

    Jul 9, 2026Joseph K. MillerTheoremFormalization

  16. The Patchwork Problem in LLM-Generated Code

    Jul 9, 2026Viraaji Mothukuri, Reza M. PariziCode GenerationVerifier

  17. Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis

    Jul 9, 2026Pierre Dantas, Lucas Cordeiro, Waldir JuniorFormal VerificationLadder

  18. Reverse Engineering Compliance: A Dual-Graph Verification Framework for Auditing Legacy IT Security Concepts

    Jul 9, 2026Lea Roxanne Muth, Marian MargrafReverse EngineeringCompliance

  19. Multi-agent Autoformalization of Tensor Network Theory

    Jul 8, 2026Sirui Lu, Erickson Tjoa, J. Ignacio CiracAutoformalizationTensor Networks

  20. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

    Jul 8, 2026Eric Jiang, Xiao Liang, Yikai Zhang +16MathematicsArtificial Intelligence Research

  21. RLVP: Penalize the Path, Reward the Outcome

    Jul 8, 2026Bojie Li, Noah ShiOutcome-Based RewardsPenalties

  22. Harnessing Code Agents for Automatic Software Verification

    Jul 7, 2026Shuangxiang Kan, Shuanglong Kan, Sebastian ErtelFormal VerificationTheorem

  23. When Certificates Fail: A Unified Safety Framework for Embedded Neural Interface Models

    Jul 7, 2026Jasmeet Singh BindraNeural Network VerificationBrain-Computer Interface

  24. AgentLens: Production-Assessed Trajectory Reviews for Coding Agent Evaluation

    Jul 7, 2026Andrey Podivilov, Vadim Lomshakov, Sergey Savin +4Coding AgentsEvaluation Harnesses

  25. Plainbook: Data Science, in Plain Language

    Jul 7, 2026Luca de Alfaro, Mathis Aubert, Ranjit Jhala +2ReproducibilityVisual Analytics

  26. aiAuthZ: Off-Host, Identity-Bound Authorization for AI Agents

    Jul 6, 2026Sai Varun KodathalaAuthorizationArtificial Intelligence Safety

  27. Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information

    Jul 6, 2026Kazumi Kasaura, Kei Tsukamoto, Kento Mori +6FormalizationKernel Hilbert Spaces

  28. LLM-as-a-Verifier: A General-Purpose Verification Framework

    Jul 6, 2026Jacky Kwok, Shulu Li, Pranav Atreya +6VerifierReinforcement Learning With Verifiable Reward

  29. How Far is Too Far? Defining the Distance Threshold for Verification Siamese Networks

    Jul 6, 2026Heloísa Dias Viotto, Cauê Samonek, Lucas Garcia Pedroso +3DistanceVerifier

  30. InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs

    Jul 6, 2026Guangyuan Wu, Weining Cao, Zehui Tan +4LoopWeave

  31. DSpark: Confidence-Scheduled Speculative Decoding with Semi-Autoregressive Generation

    Jul 6, 2026Xin Cheng, Xingkai Yu, Chenze Shao +30Speculative DecodingSelf-Speculative

  32. FormalRx: Rectify and eXamine Semantic Failures in Autoformalization

    Jul 6, 2026Haocheng Wang, Baiyu Huang, Yingjia Wan +4AutoformalizationGeo-Contextual Alignment

  33. Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs

    Jul 6, 2026Gabriel Poesia, Simon Henniger, Tzu-Han Hsu +2Mock-Interface SynthesisFormal Verification

  34. Mechanism-level routing failure in LLMs over Lean-verified algebraic structures

    Jul 5, 2026Manuel Israel Cázares, Wenlin Zhang, Haobo MaTheoremAlgebraic Structures

  35. Flash-BoN: Instant Drafts for Inference-Time Scaling in Diffusion Models

    Jul 5, 2026Ruchit Rawal, Reza Shirkavand, Sayak Paul +5Text-To-Image Diffusion ModelsText-To-Image

  36. MechMath Agent Team: LLM Driven Agents for Mathematical Research

    Jul 5, 2026Yichuan Cao, Ruichen Qiu, Junqi Liu +5MathematicsMulti-Agent Reasoning

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

    Jul 4, 2026Akira Tanaka, Yusuke KawamotoTwo-Sample TestingReproducibility

  38. AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis

    Jul 4, 2026Adarsh Vatsa, Sachi Shome, Yingming Zhou +1AuthorizationVerifier

  39. FOI-O: An NZ-first ontology and verification methods package for Freedom of Information process modelling

    Jul 3, 2026Dylan A MordauntOntologyBusiness Processes

  40. A Workflow-Aware Serving Layer for Agentic Applications

    Jul 3, 2026Jiayi Qian, Zishen Wan, Hanchen Yang +3Agentic WorkflowsWorkflow Automation and Optimization

  41. Online Safety Monitoring for LLMs

    Jul 2, 2026Mona Schirmer, Metod Jazbec, Alexander Timans +3Large Language Model SafetySafety

  42. PairCoder++: Pair Programming as a Universal Paradigm for Verified Code-Driven Multimodal and Structured-Artifact Generation

    Jul 2, 2026Junhao Chen, Xiang Li, Mingjin Chen +9Code GenerationPair Programming

  43. Reformalization of the Jordan Curve Theorem

    Jul 2, 2026Simon Guilloud, Sankalp Gambhir, Samuel ChassotAutoformalizationTheorem

  44. Safe and Adaptive Cloud Healing: Verifying LLM-Generated Recovery Plans with a Neural-Symbolic World Model

    Jul 2, 2026Junyan Tan, Haoran Lin, Siyuan Guo +4Fault Injection ExperimentsLlm-Driven

  45. Theoria: Rewrite-Acceptability Verification over Informal Reasoning States

    Jul 1, 2026Michael Saldivar, Ben SlivinskiTheoremVerifier

  46. Self-Evolving Agents with Anytime-Valid Certificates

    Jul 1, 2026Biswa SenguptaSelf-Evolving AgentsModifications

  47. Dynamic Bidirectional Pattern Memory: A Production-Scale Empirical Characterisation of Inference-Time Gating in Clinical NLP

    Jul 1, 2026Ali H. Lazem, William TeahanNatural Language InferenceLarge Language Model Pipelines

  48. LRAT-Catcher: Importing SAT Solver Certificates into Lean4 by Reflection

    Jul 1, 2026Stefan SzeiderSatisfiabilityTheorem

  49. AxDafny: Agentic Verified Code Generation in Dafny

    Jun 30, 2026Benjamin Breen, Austin Letson, Borja Requena Pozo +1Formal VerificationCode Generation

  50. Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts

    Jun 30, 2026Rajeev Goré, Cormac KikkertSatisfiabilityTheorem

  51. Calibration, Not Compilation: Detecting and Repairing Misspecified Probabilistic Programs Written by Language Models

    Jun 30, 2026Jian Xu, Delu Zeng, John Paisley +1CorrectnessLarge Language Model Reliability

  52. Verification-Gated Agentic Mission-State Governance for Intelligent Industrial Multi-Robot Systems

    Jun 30, 2026Guoqin Tang, Qingxuan Jia, Yichen Tan +3Multi-Robot SystemsVerifier

  53. Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

    Jun 30, 2026Arshia Soltani Moakhar, Iman Gholami, Max Springer +2AutoformalizationTheorem

  54. Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

    Jun 30, 2026Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy +3TheoremExplanation Faithfulness

  55. Knowledge-Driven Dimension Estimation from a Single Image -3D Asset Generation Technology for Digital Twin Construction

    Jun 29, 2026Hidenori Sakaniwa, Akihito Akai, Akihiko Hyodo3D Object DetectionMonocular Videos

  56. Transformer Architectures as Complete Bayes Processes: A Formal Proof in the Measure-Theoretic Kernel Framework

    Jun 29, 2026Haobo YangTransformer ArchitecturesBayesian

  57. Proofs of Ownership for Machine Learning Models

    Jun 29, 2026Ran Canetti, Shafi Goldwasser, Or ZamirZero-Knowledge ProofsProof

  58. SEVA: Self-Evolving Verification Agent with Process Reward for Fact Attribution

    Jun 29, 2026Aojie Yuan, Yi Nian, Haiyue Zhang +2VerifierFacts

  59. Toward Secure and Reliable PDDL Formalization of Large Language Models with Planner-in-the-Loop Feedback

    Jun 29, 2026Jiamei Jiang, Jiajing Zhang, Feifei Mo +2Large Language Model PlanningFormalization

  60. A Machine-Verified Proof of a Quantum-Optimization Conjecture

    Jun 29, 2026Uri Kol, Maor Ben-Shahar, Kfir Sulimany +1Quantum Approximate Optimization AlgorithmProof