🤖 database, relevant work found but not yet read

(authored by agents unless marked 🧑)

Claude agents read each lead’s abstract and judged whether it serves the goal. Nobody has read the papers. Leads judged not relevant are only in leads.jsonl.

not judged yet

366 leads.

• A Comparative Review of ZFC, NBG, and MK Axiom Systems: Theoretical Foundations and Formalization in Coq
• A Complete Formal Specification and Verification of the BESW Software Control System of the Maeslant Storm Surge Barrier
  • source
• A comprehensive survey of UPPAAL‐assisted formal modeling and verification
• A Domain Specific Language for Testing Consensus Implementations
  • source
• A Formal Framework for Requirements Engineering in Large Language Model-Integrated Cyber-Physical Systems
• A formal framework for the specification and verification of robotic skills composition for autonomous behaviors
  • source
• A Formal Framework for the Specification, Verification and Validation of Robotic Skills Composition for Autonomous Behaviors
  • source
• A Formal Verification Method for Real-Time Embedded Systems
  • source
• A Formally Verified AI Framework for Scheduling OptimiSation in Slurm-Based Distributed HPC Systems
  • source
• A lean-based language for teaching proof in high school
• A Minimal Agent for Automated Theorem Proving
  • source
• A model-driven formal methods approach to software architectural security vulnerabilities specification and verification
  • source
• A Multimodal AI System: Comparing LLMs and Theorem Proving Systems
  • source
• A Novel Approach for Specification and Verification of Symmetric Distributed Algorithms Using SPIN
  • source
• A review on agent-to-agent protocol: Concept, state-of-the-art, challenges and future directions
• A short survey on formalising software requirements using large language models
• A Survey on LLM-Integrated Hardware Design Verification
  • source
• A temporal logic for the specification and verification of real-time systems
  • source
• A Theoretical Framework for Self-Play Theorem Proving Algorithms
  • source
• About Trust and Proof: a situation, a contemplation, and a framework
• Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction
  • source
• Accountability Chains: A Formal Specification for AI Agent Delegation
  • source
• ACSLAgent: Verifier-Constrained Neural-Symbolic Synthesis of Formal Program Specifications
  • source
• Advancing Formal Verification: Fine-Tuning LLMs for Translating Natural Language Requirements to CTL Specifications
  • source
• Advancing mathematics research with AI-driven formal proof search
• Advancing multi-agent systems through model context protocol: Architecture, implementation, and applications
• Adventures in FRET and Specification
  • source
• AF-SGS: Blockchain-assisted secure authentication framework for smart grid systems
• AgentRFC: Security Design Principles and Conformance Testing for Agent Protocols
  • source
• AgentVerify: Compositional Formal Verification of AI Agent Safety Properties via LTL Model Checking
  • source
• AI-Enabled Formal Methods for Verifiable Software Requirements: A Survey
• AI-generated test automation for autonomous software verification: Enhancing quality assurance through AI-driv
• AI-powered cancer diagnosis: classifying viable (live) vs non-viable (dead) cells using transfer learning
• An approach to using Golang programs for the specification and verification of distributed systems
  • source
• An LLM Benchmark Suite for Specification Inference
• Analysing Sanity of Requirements for Avionics Systems
  • source
• AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language
  • source
• Application of Directed Formal Verification to Detect Protocol Deadlocks in PCIe Systems
  • source
• Architectural Specication and Invariant Graph Topology of the Phaistos Disc Corpus: A Deterministic Automaton Approach
  • source
• Artifact for “Beyond Benchmarks: A Case Study of LLM-Generated Verus Specification Failures on Asterinas Vostd”
  • source
• Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Sy
• Auth Invariant Tester: Temporal Authorization Correctness Verification for Distributed Systems
  • source
• AutoJML: Generation and Verification of JML Specifications Using LLM Agents
  • source
• Automated and interpretable verification of distributed protocols
  • source
• Automated and interpretable verification of distributed protocols (Stanford thesis)
  • source
• Automated formal verification of secure aggregation protocols
  • source
• Automated Scientific Discovery via Causal Falsification and Formal Multi-Agent Verification
  • source
• Automated Theorem Proving with Deep Reinforcement Learning
  • source
• Automated Theorem Proving with Interactive Machine Learning
  • source
• Automated Theorem Proving with Reinforcement Learning and Symbolic Reasoning
  • source
• Automating the Verification of Distributed Systems (Michigan thesis)
  • source
• Automating TLA+ Model Synthesis with Large Language Models and Formal Verification Pipelines (WIP)
  • source
• Autonomous Theorem Proving via Hierarchical Reinforcement Learning
  • source
• AutoReSpec: A Framework for Generating Specification using Large Language Models
• Ax-Prover: a deep reasoning agentic framework for theorem proving in mathematics and quantum physics
  • source
• Bayesian Hierarchical Invariant Prediction
  • source
• Benchmarking Agents for Proving Theorems in Quantum Algorithms and Quantum Information
  • source
• Beyond Benchmarks: A Case Study of LLM-Generated Verus Specification Failures on Asterinas Vostd
  • source
• Beyond Monotonicity: Specification and Design of Concurrent Distributed Systems
  • source
• Big data-driven distributed machine learning for scalable credit card fraud detection using PySpark, XGBoost,
• Biometric authentication using IoT devices powered by deep learning and encrypted verification
• Blockchain-Enabled Medical Waste Management System for Enhanced Traceability, Safety and Environmental Protect
• Breaking the Composition Cliff: Mutation-Guided Specification Synthesis for Multi-Function Programs
  • source
• Bridging the gap: a systematic framework for agentic AI root cause analysis in hybrid distributed systems
• BrokenMath: A Benchmark for Sycophancy in Theorem Proving with LLMs
  • source
• Bulletproofing Zeebe concurrency bugs
  • source
• Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
  • source
• Certifying the Judge: Falsifiable Properties for LLM-Based Evaluation of Formal Code
• CertJudge: Evaluating Lean Formal-Code With Falsifiable Properties
• Challenges of Multilingual Program Specification and Analysis
  • source
• Checking Sanity of Software Requirements
  • source
• Circuitlm: A multi-agent llm-aided design framework for generating circuit schematics from natural language pr
• Clifford Circuit Synthesis for Distributed Quantum Architectures with Arbitrary Network Topology
  • source
• Computational Cooperation Boundary Theorem: A Unified Theoretical Framework for Distributed and Multi-Agent Systems
  • source
• Computational Invariant Fusion Theory (CIFT): A Framework for Deriving Higher‑Level Computational Laws from Low‑Level Invariants
  • source
• Constrained Synchronization of Multi-Agent Systems Using Distributed MPC and Invariant Families of Terminal Sets
  • source
• Constructing formal models of cryptographic protocols from Alice&Bob style specifications via LLM
  • source
• Context-Aware Contracts as a Lingua Franca for Behavioral Specification
  • source
• Continuum: Efficient and robust multi-turn llm agent scheduling with kv cache time-to-live
• Contract-LIB: A Proposal for a Common Interchange Format for Software System Specification
  • source
• Controller Synthesis for Linear Systems with Reach-avoid Specification
  • source
• Correct Programs, Executed Correctly: Verifying Specifications And Executions
• Corten - Foundational Verification of Rust Programs
  • source
• Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification
• Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols
  • source
• Cross-Chain Interoperability: Formal Verification and Recursive Zero-Knowledge Architectures for Heterogeneous Distributed Systems
  • source
• Cross-Model Evaluation of LLMs for Generating Formal Specification of Distributed Industrial Control Systems
  • source
• Cross-protocol Attack Surface Analysis in Multi-agent AI Systems: Formal Verification and Categorical Modelling of Translation-boundary Vulnerabilities
  • source
• Data Consistency Verification and Detection Based on Formal Methods in Distributed Environment
  • source
• Deep Reinforcement Learning for Automated Theorem Proving
  • source
• Deepscholar-bench: A live benchmark and automated evaluation for generative research synthesis
• Demystifying Invariant Effectiveness for Securing Smart Contracts
  • source
• Design and Implementation of a Protocol for the SagaMAS Framework to Manage Distributed Transactions in Micros
• Deterministic Execution and Margin Enforcement in Financial Transaction Systems: Empirical Evaluation with For
• Deterministic Execution and Margin Enforcement in Financial Transaction Systems: Empirical Evaluation with Formal Safety Verification
  • source
• Deterministic Runtime Enforcement: The Execution Authority for Autonomous AI Agents
• Development of interactive E-LKPD based on Live-Worksheets for reading and viewing skills
• Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
  • source
• Distributed Asynchronous Impulsive Consensus of Multi-agent Systems
  • source
• Distributed Discontinuous Adaptive Impulsive Consensus of Uncertain Multi-agent Systems
  • source
• Distributed Impulsive Consensus of Delayed Multi-agent Systems
  • source
• Distributed Impulsive Consensus of Multi-agent Systems Under Cyber Attacks
  • source
• Distributed Locking as a Data Type
  • source
• Distributed Proximal-Gradient Algorithms for Nonsmooth Convex Optimization of Second-Order Multi-agent Systems
  • source
• Distributed safe control design and probabilistic safety verification for multi-agent systems
  • source
• Distributed synthesis of arbitrary graph states in quantum networks via rank-two GF(2) reduction
  • source
• Distributed Theorem Proving with Evolutionary Strategies
  • source
• Distributed Unknown Input Observers for Discrete-Time Linear Time-Invariant Systems
  • source
• Distributed Variable Impulsive Consensus of Multi-agent Systems
  • source
• Efficient Synthesis of Symbolic Distributed Protocols by Sketching
  • source
• Elle: Inferring Isolation Anomalies from Experimental Observations
  • source
• Encoding TLA+ proof obligations safely for SMT
  • source
• Ensuring Convergence and Invariants Without Coordination
  • source
• Ensuring Reliability in Self-Adaptive Systems: A Framework for Formal Specification and Verification
  • source
• Ensuring Safety and Reliability: Formal Verification of Communication-Based Train Control Systems
  • source
• Equilibrium analysis of live-streaming e-commerce supply chain in the AI era
• Evaluating LLM-Generated ACSL Annotations for Formal Verification
  • source
• Event-based stochastic Lyapunov-type theorem and its application to leader-following multi-agent systems
  • source
• Exploring LLMs for Verifying Technical System Specifications Against Requirements
  • source
• Extracting Formal Smart-Contract Specifications from Natural Language with LLMs
  • source
• Formal Consistency Checking over Specifications in Natural Languages
  • source
• Formal Methods for Distributed Computing in Future Railway Systems
  • source
• Formal Methods for Multi-Agent Feedback Control Systems
  • source
• Formal Modeling and Verification of Blockchain Consensus Mechanisms using Process Algebra
  • source
• Formal Modeling with Verification of Smart Courtroom Building System (SMCBS) Using UML and TLA+ Specification
  • source
• Formal modelling and analysis of Clock-SI with TLA+
  • source
• Formal Reasoning About the Security of Amazon Web Services
  • source
• Formal Specification and Implementation of Distributed Lazy Group Membership Protocol
  • source
• Formal specification and SMT verification of quantized neural network for autonomous vehicles
  • source
• Formal Specification, and Verification of a Cooperative Multi-robots System for Delivery Service
  • source
• Formal Specification and Verification of API Security Based on Design by Contract
  • source
• Formal Specification and Verification of Autonomous Vehicle Group Control Systems Using Hybrid Automata and Maude
  • source
• Formal Specification and Verification of MQTT Protocol Using CoQ Proof Assistant
  • source
• Formal Specification and Verification of Protection in Transit (PIT) Protocol Using UPPAAL
  • source
• Formal specification and verification of rule-basedartificial intelligence systems using Event-B
  • source
• Formal Specification and Verification of Time-Sensitive Drone Systems using TLA+: A Case Study
  • source
• Formal Specification-Based Code Review via LLMs
  • source
• Formal Specification of Distributed Consensus with Partial Observability
  • source
• Formal Verification
  • source
• Formal Verification and Security Analysis
  • source
• Formal Verification Frameworks for Cloud-Native Microservices
  • source
• Formal Verification of a Crash-Safe File System Based on Non-Persistent Conditions Extended Concurrent Separation Logic
  • source
• Formal Verification of a JIT Backend Compiler
  • source
• Formal Verification of a Memory Allocator for Rust Hypervisors: From Verified to Deployable Code with Functional Equivalence Guarantees
  • source
• Formal Verification of a Pacemaker
  • source
• Formal Verification of a Rust-Based Buddy Physical Memory Allocator
  • source
• Formal Verification of Access Control Policies for Critical IoT Systems
  • source
• Formal Verification of Agentic MLOps Protocols: Model Checking and Liveness Guarantees in Distributed Model Context Protocol Workflows
  • source
• Formal Verification of Autonomous Vehicle Group Control Systems via Specification Translation of Multitask Hybrid Observational Transition Systems
  • source
• Formal Verification of BDI Agents
  • source
• Formal Verification of Blockchain Consensus Protocols Using Temporal Logic
  • source
• Formal Verification of Data Integrity and API Security in Distributed Analytics Systems
  • source
• Formal Verification of Decentralized Consensus Algorithms Using Abstract Interpretation
  • source
• Formal Verification of Decentralized Consensus Algorithms Using Process Algebra
  • source
• Formal Verification of Decentralized Consensus Protocols using Abstract Interpretation
  • source
• Formal Verification of Distributed Byzantine Fault Tolerance Protocols via Abstract Interpretation
  • source
• Formal Verification of Distributed Consensus Algorithms using Model Checking
  • source
• Formal Verification of Distributed Consensus Algorithms using Temporal Logic
  • source
• Formal Verification of Distributed Consensus Algorithms with Symbolic Execution
  • source
• Formal Verification of Distributed Consensus Algorithms with Temporal Logic
  • source
• Formal verification of distributed, data-intensive microservice applications using Petri Nets
  • source
• Formal Verification of Epistemic States with Uncertainty in Multi-Agent Systems
  • source
• Formal Verification of Impure Coq JITs
  • source
• Formal Verification of Parameterised Neural-symbolic Multi-agent Systems
  • source
• Formal Verification of Smart Contracts for EEG Data Governance: A Case Study with Slither and Formal Specification
  • source
• Formal verification of time-bounded BPMN model with message broker using timed automata
  • source
• Formalization of security
• Formalizing Requirements into Dafny Specifications with LLMs
  • source
• Formally Specifying the Intended Behavior of the Program: LLM-Driven Neuro-Symbolic Program Specification Synthesis
  • source
• Formally Verified Lock-Free Software Transactional Memory for Scientific Measurement
• FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs
  • source
• ForMAt: Formal Verification of Scalable Multiply and Accumulate Units
  • source
• Fortifying Integrity, Traceability, and Operational Efficacy in Blockchain-Based Examination Management Throug
• Fortifying Integrity, Traceability, and Operational Efficacy in Blockchain-Based Examination Management Through Formal Verification with TLA+
  • source
• From C to verifiable Rust: Towards practical migration of code and specifications
  • source
• From Natural Language to Formal Specifications: A Metamodel-Driven LLM Pipeline
  • source
• From natural language to solver-ready power system optimization: An llm-assisted, validation-in-the-loop frame
• Generating formal smart-contract specifications: comparing few-shot learning and fine-tuned LLMs
  • source
• Graphical-Probabilistic Modeling of Generative Flows in LLM-Native Software Systems
• Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean
  • source
• Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors
• HAMILTON’S PRINCIPLE AND THE INVARIANTS
  • source
• HarnessLLM: Rust Verification Harness Generation with Large Language Models
  • source
• Heterogeneous Face Recognition Using Domain Invariant Units
  • source
• Hilbert: Recursively building formal proofs with informal reasoning
• HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
  • source
• How does live streaming affect tourists’ intention—a psychology theory perspective
• How Stable Are LLM-Generated Proofs Under Program Refactoring? A Stress Test for Verifiable Code Generation
• Inside AgentGuard: A Four-Stage Pipeline for Structured LLM Generation
• Intelligent software validation frameworks for mission-critical enterprise applications using AI and knowledge
• Interest Beyond Violation: On Points-of-Interest in Runtime Verification
  • source
• Interoperability Challenges and Machine Learning Protocols for Scalable Distributed Automation Systems Across Intelligent Industrial Workcells
  • source
• Invariant Checking for SMT-Based Systems with Quantifiers
  • source
• Investigating the Role of Formal Verification in Software Development: From Automatic Specification Generation to Usability of Verification Languages
  • source
• Investigation of Formal Verification of Autonomous Vehicle Control Systems Through Specification Translation from Cafeobj to Real-Time Maude
  • source
• Is truth futureproof?
• Is truth futureproof? On the possible futures of mechanized proofs
• KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification
  • source
• Large Language Models (LLM) and Temporal Logic of Actions (TLA): How Effective are LLMs for Verification Systems
  • source
• Lean-auto: an interface between lean 4 and automated theorem provers
• lean-smt: An SMT Tactic for Discharging Proof Goals in Lean
• Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory
  • source
• LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean
• LeanMachines: State-based Modeling with Refinement (a Lean4 Framework)
• Learning Normative Behaviour Through Automated Theorem Proving
  • source
• Let a Neural Network Be Your Invariant
  • source
• Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification
  • source
• Leveraging Cryptographic Simulator Synthesis for Formally Verifying the FOO E-Voting Protocol
  • source
• Leveraging LLMs for Formal Software Requirements–Challenges and Prospects
• Leveraging TLA+ Specifications to Improve the Reliability of the ZooKeeper Coordination Service
  • source
• Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code (MaceMC)
  • source
• Live: Learning Video LLM with Streaming Speech Transcription at Scale
• Liveresearchbench: A live benchmark for user-centric deep research in the wild
• LLM-aided automatic modeling for security protocol verification
• LLM-as-Specification-Judge: Multi-Model Consensus for Trustworthy Cryptographic Verification
  • source
• Llm-based unknown function automated modeling in sensor-driven systems for multi-language software security ve
• LLM-Driven Automated Generation of Formal Specifications for C Programs
• LLM For Loop Invariant Generation and Fixing: How Far Are We?
• LLM-Guided Formal Verification Coupled with Mutation Testing
  • source
• LLM-guided Predicate Discovery and Data Augmentation for Learning Likely Program Invariants
  • source
• LLM-Powered Structurer: Normalizing Natural Language to Information Delivery Specification for Industrial Data
• Loka protocol: A decentralized framework for trustworthy and ethical ai agent ecosystems
• Machine-Checked Proofs and Automated Verification for Post-Quantum Distributed Systems
• Machine learning-driven framework for realtime air quality assessment and predictive environmental health risk
• Machine Learning for Automated Theorem Proving using Reinforcement Learning
  • source
• Machine Verification of Correctness for a Concurrent Union-Find Object
• Mahi-mahi: Low-latency asynchronous bft dag-based consensus
• Map the blockchain world: A trustless and scalable blockchain interoperability protocol for cross-chain applic
• MASA: A Modular Framework for LLM-Driven Multi-Agent Systems for Autoformalization
  • source
• MASA: LLM-Driven Multi-Agent Systems for Autoformalization
  • source
• Mediation, State, and Verification in Enterprise Multi-Agent AI Systems: A Formal Reference Architecture and Evaluation Protocol
  • source
• Meet MASKS: integrating distributed knowledge and verification for multi-agent systems
  • source
• MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
  • source
• Meta-Learning for Automated Theorem Proving
  • source
• Metastable failures in distributed systems
  • source
• Model verification of real-time and distributed stream processing architecture
  • source
• Modeling and Verification of Multi-Agent Cyber-Physical Systems in Verse Library
  • source
• Modelling and Verification of Multi-agent Hybrid Systems
  • source
• Moving Beyond Specification Validation to Specification Refinement with Mutation Verification
• Mucosal-associated invariant T cells recognize a tumor-derived metabolite in the DNA synthesis pathway
  • source
• Multi-Agent Systems and Control Theory
  • source
• Multiparty session types for distributed and failure-prone systems
  • source
• Neuro-Symbolic Programming with Reinforcement Learning for Automated Theorem Proving
  • source
• Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
  • source
• Observability of Linear Time-Invariant Systems with Relative Measurements: A Geometric Approach
  • source
• Olympiad-level formal mathematical reasoning with reinforcement learning
• On the Formal Verification of Smart Contracts and Blockchain: Challenges and Future Directions
  • source
• Online enumeration of minimal inconsistent subsets of temporal requirements
  • source
• Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair
  • source
• OpenProver: Agentic and Interactive Theorem Proving with Lean 4
  • source
• Operational intelligence at enterprise scale: Federated control assurance, multi-agent coordination, and value
• OProver: A Unified Framework for Agentic Formal Theorem Proving
  • source
• Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
  • source
• OracleSFT — Verifier-Filtered Self-Training for Verus with Five Training Signals: Replication Package
  • source
• Origin and Limits of Invariant Warming Patterns in Climate Models
  • source
• Parameterized Verification of Timed Networks with Clock Invariants
  • source
• PhysProver: Advancing Automatic Theorem Proving for Physics
  • source
• Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support
  • source
• Practical Verification of Distributed Systems: Streamlining Safety Proofs Using Invariant Taxonomies, and Verifying Latency Properties Using Symbolic Latency
  • source
• Pramana: A Protocol-Layer Treatment of Claim Verification in Autonomous Agent Networks
• Pretend synchrony: synchronous verification of asynchronous distributed programs
  • source
• Privacy-preserving techniques in biometric systems: Approaches and challenges
• Probabilistic Formal Verification of Distributed Consensus Algorithms
  • source
• Probabilistic Safety Verification of Distributed Systems: A Statistical Approach for Monitoring
  • source
• Probably Correct: Rethinking Formal Verification for LLM-Driven Systems
  • source
• Programming LLM Reasoning: A Meta-Template for Constraint Specifications
  • source
• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimizat
• Protecting context and prompts: Deterministic security for non-deterministic AI
• PROV-AGENT: Unified provenance for tracking AI agent interactions in agentic workflows
• Provable AI ethics and explainability in medical and educational AI agents: trustworthy ethical firewall
• Prover agent: An agent-based framework for formal mathematical proofs
• Quantum-Enhanced Distributed Systems: A Practical Framework for Autonomous Agent Networks
  • source
• Ranking Formal Specifications using LLMs
  • source
• Ranking LLM-Generated Loop Invariants for Program Verification
  • source
• Real-Time Protocol Engineering with the B Language
  • source
• Recovery Algorithm for Correlated Errors in Permutation-Invariant Quantum Codes
  • source
• RefinedRust: A Type System for High-Assurance Verification of Rust Programs
  • source
• Regular Model Checking Upside-Down: An Invariant-Based Approach
  • source
• Reinforcement Learning for Automated Theorem Proving
  • source
• Reinforcement Learning for Automated Theorem Proving with Symbolic State Representation
  • source
• Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems
  • source
• RvLLM: LLM Runtime Verification with Domain Knowledge
  • source
• Safe: Enhancing mathematical reasoning in large language models via retrospective step-aware formal verificati
• SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols: An Update
  • source
• Scalable Verification and Validation of Concurrent and Distributed Systems (ScaVeri) (Track Summary)
  • source
• SCION and cross-border payments: Enhancing security and compliance in distributed ledger networks
• Secure and efficient cloudlet networks: blockchain integration with agent-based proof of trust mechanism
• Secure Synthesis of Distributed Cryptographic Applications (Technical Report)
  • source
• Securing the model context protocol (mcp): Risks, controls, and governance
• Security analysis and formal verification on blockchain and its applications
• Security of the Lightning Network: Model Checking a Stepwise Refinement with TLA+
  • source
• Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
  • source
• Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds
  • source
• Semi-Formal Verification
  • source
• Septemberember/SG4PM: Specification Generation for Program Maintenance via LLMs and Testing-Based Formal Verification
  • source
• Sieve and Acto (testing Kubernetes controllers for liveness and safety bugs): the search result says 46 bugs for Sieve (OSDI 2022
  • source
• Six-Layer Formal Verification of a Safety-Critical AI Governance Kernel
• Smart Contract Invariants Protect Against Cybercriminals
  • source
• SoK: Agentic Skills–Beyond Tool Use in LLM Agents
• Solving Zebra Puzzles Using Constraint-Guided Multi-Agent Systems
  • source
• SpecFSM: Extracting and Repairing Finite State Machines from Protocol Specification Documents
  • source
• Specification
  • source
• Specification and Verification of a Formal Model for a Real-Time System Using TLA+
  • source
• Specification-Driven Test Generation for Fault Localisation in Dafny
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs Using LLMs
  • source
• Specification of Autonomous Behavior
  • source
• SpecifyThis Bridging Gaps Between Program Specification Paradigms: Track Introduction
  • source
• SpecIntelli: Leveraging LLMs for Formal Specification and Verification from Natural Language Requirements
  • source
• STAFF: Towards Translating Formal Verification Benchmarks between Formal Specification Languages
  • source
• Statically verified refinements for multiparty protocols
  • source
• Supporting software formal verification with large language models: An experimental study
• Surveying the Rust Verification Landscape
  • source
• Swe-bench goes live!
• Symbolic AI for Automated Theorem Proving with Adaptive Rule Synthesis
  • source
• SysMoBench: Evaluating AI on Formally Specifying Complex Real-World Systems
• Systems Engineering With Architecture Modeling, Formal Verification, and Human Interactions for Learning‐Enabled Autonomous Agent
  • source
• TaxDC: A Taxonomy of Non-Deterministic Concurrency Bugs in Datacenter Distributed Systems
  • source
• Teaching Code LLMs to Reason with Intermediate Formal Specifications
  • source
• Technical Report: Exploring Automatic Model-Checking of the Ethereum specification
  • source
• Temporal Logic Verification of Distributed Consensus Algorithms
  • source
• $$\text{HornStr}$$: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses
  • source
• The Accountability Horizon: An Impossibility Theorem for Governing Human-Agent Collectives
  • source
• The Challenges and Triumphs of CSP Based Formal Verification
  • source
• The Missing Layer: Specification Infrastructure for AI Oversight
  • source
• THE MODEL CONTEXT PROTOCOL IN LLM AGENT ARCHITECTURES
• The reemergence of the New World screwworm and its potential distribution in North America
• The Role of Communication Delays in the Optimal Control of Spatially Invariant Systems
  • source
• The semantics of TLA on the PVS theorem prover
  • source
• Theorem proving in artificial neural networks: new frontiers in mathematical AI
  • source
• Three Patterns for 99.9% Reliability in Distributed Payments: Velocity-Aware Idempotency, Cross-Protocol Failover, and Shadow-Compare Migration
  • source
• Title: Self-Organizing Constraint Propagation for Automated Theorem Proving
  • source
• TLA+ Bench
  • source
• TLCrafter: Peeling the Layers of Natural Language to Reveal Temporal Logic Specifications
  • source
• Toward Formal Verification of a Lock-Free Distributed Double Buffer Cache
  • source
• Towards Formal Modeling and Verification of the Stellar Consensus Protocol in Z3
  • source
• Towards Formal Specification of Agent-based Transport Models
  • source
• Towards formal verification of llm-generated code from natural language prompts
• Towards Language Model Guided Proof Automation
• Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software
  • source
• Towards the Formal Specification of Iot Systems
  • source
• Towards the LLM-based generation of formal specifications from natural-language contracts: Early experiments w
• Trainverify: Equivalence-based verification for distributed LLM training
• Transforming Formal Verification - Insights from MALPAS
  • source
• Transforming Natural Language Requirements to Formalism Using LLMs
• Transition Invariants Revisited: Termination Witnesses and Their Validation
  • source
• TrojanSpec-Bench: An Adversarial Benchmark for LLM-Based Formal Specification Elicitation
  • source
• Tunable Automation in Automated Program Verification
  • source
• Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
  • source
• Typestates Specification and Verification in Frama-C
  • source
• Unleashing the power of LLM to infer state machine from the protocol implementation
• Utilizing LLM Chatbots for Formal Descriptions of Cryptographic Protocols
  • source
• Validating Generative AI Outputs Through Co-Generation of Code and Specifications
• Verifiable Lifecycle Assurance for Agentic Software: From Selection and Deployment through Continuous Audit to
• Verification and attack synthesis for network protocols
  • source
• Verification and synthesis of distributed systems with weak synchronisation
  • source
• Verified LLM-Driven Synthesis for Concept Design
• Verifier-supervised fine-tuning for Rust/Verus: vericoding dataset (restricted)
  • source
• Verifying an HTTP Key-Value Server with Interaction Trees and VST
  • source
• Verifying Consensus Protocols from LLM-assisted TLA: A Case Study of Byzantine Reliable Broadcast
• Verifying Distributed Protocols (Mark Yuen capstone, Yale-NUS, TLA+ to Ivy translation of Suzuki-Kasami and NOPaxos)
  • source
• Verifying Graceful Degradation in a Distributed Malware-Detection System with SPIN
  • source
• Verifying Rust code with Verus
  • source
• VerusSeek: Retrieval-Augmented LLM-Based Proof Synthesis for Rust Programs
  • source
• Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models
  • source
• Why Does the Cloud Stop Computing? Lessons from Hundreds of Service Outages
  • source
• WIP: An Engaging Undergraduate Intro to Model Checking in Software Engineering Using TLA+
  • source

Last edited: 2026-10-13