Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

đŸ€– 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.

no abstract found

190 leads.

  • A Comparative Review of ZFC, NBG, and MK Axiom Systems: Theoretical Foundations and Formalization in Coq
  • A Formal Framework for Requirements Engineering in Large Language Model-Integrated Cyber-Physical Systems (2026)
  • A formal framework for the specification and verification of robotic skills composition for autonomous behaviors
  • A Formal Framework for the Specification, Verification and Validation of Robotic Skills Composition for Autonomous Behaviors (2025)
  • A Formal Verification Method for Real-Time Embedded Systems (2026)
  • A lean-based language for teaching proof in high school
  • A model-driven formal methods approach to software architectural security vulnerabilities specification and verification (2025)
  • A Novel Approach for Specification and Verification of Symmetric Distributed Algorithms Using SPIN (2024)
  • A temporal logic for the specification and verification of real-time systems
  • About Trust and Proof: a situation, a contemplation, and a framework
  • Advancing Formal Verification: Fine-Tuning LLMs for Translating Natural Language Requirements to CTL Specifications (2024)
  • Advancing multi-agent systems through model context protocol: Architecture, implementation, and applications
  • Adventures in FRET and Specification (2024)
  • AF-SGS: Blockchain-assisted secure authentication framework for smart grid systems (2026)
  • 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 (2025)
  • An approach to using Golang programs for the specification and verification of distributed systems (2024)
  • An LLM Benchmark Suite for Specification Inference
  • Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Sy
  • AutoJML: Generation and Verification of JML Specifications Using LLM Agents (2026)
  • Automated Theorem Proving with Deep Reinforcement Learning (2026)
  • Automated Theorem Proving with Interactive Machine Learning (2026)
  • Automated Theorem Proving with Reinforcement Learning and Symbolic Reasoning
  • Autonomous Theorem Proving via Hierarchical Reinforcement Learning
  • AutoReSpec: A Framework for Generating Specification using Large Language Models (2026)
  • Beyond Monotonicity: Specification and Design of Concurrent Distributed Systems
  • 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 (2025)
  • Bridging the gap: a systematic framework for agentic AI root cause analysis in hybrid distributed systems
  • 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 (2024)
  • Checking Sanity of Software Requirements (2012)
  • 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 (2026)
  • Computational Cooperation Boundary Theorem: A Unified Theoretical Framework for Distributed and Multi-Agent Systems
  • Computational Invariant Fusion Theory (CIFT): A Framework for Deriving Higher‑Level Computational Laws from Low‑Level Invariants
  • Constrained Synchronization of Multi-Agent Systems Using Distributed MPC and Invariant Families of Terminal Sets (2024)
  • Context-Aware Contracts as a Lingua Franca for Behavioral Specification
  • Contract-LIB: A Proposal for a Common Interchange Format for Software System Specification (2024)
  • Controller Synthesis for Linear Systems with Reach-avoid Specification (2024)
  • Correct Programs, Executed Correctly: Verifying Specifications And Executions
  • Cross-Chain Interoperability: Formal Verification and Recursive Zero-Knowledge Architectures for Heterogeneous Distributed Systems
  • Cross-Model Evaluation of LLMs for Generating Formal Specification of Distributed Industrial Control Systems (2025)
  • Cross-protocol Attack Surface Analysis in Multi-agent AI Systems: Formal Verification and Categorical Modelling of Translation-boundary Vulnerabilities (2026)
  • Data Consistency Verification and Detection Based on Formal Methods in Distributed Environment (2025)
  • Deep Reinforcement Learning for Automated Theorem Proving
  • Deepscholar-bench: A live benchmark and automated evaluation for generative research synthesis
  • Design and Implementation of a Protocol for the SagaMAS Framework to Manage Distributed Transactions in Micros
  • Distributed Discontinuous Adaptive Impulsive Consensus of Uncertain Multi-agent Systems (2024)
  • Distributed Impulsive Consensus of Delayed Multi-agent Systems (2024)
  • Distributed Proximal-Gradient Algorithms for Nonsmooth Convex Optimization of Second-Order Multi-agent Systems (2025)
  • Distributed safe control design and probabilistic safety verification for multi-agent systems (2025)
  • Distributed Theorem Proving with Evolutionary Strategies
  • Distributed Variable Impulsive Consensus of Multi-agent Systems
  • Encoding TLA+ proof obligations safely for SMT (2025)
  • Ensuring Convergence and Invariants Without Coordination
  • Equilibrium analysis of live-streaming e-commerce supply chain in the AI era
  • Event-based stochastic Lyapunov-type theorem and its application to leader-following multi-agent systems (2025)
  • Exploring LLMs for Verifying Technical System Specifications Against Requirements (2024)
  • Extracting Formal Smart-Contract Specifications from Natural Language with LLMs (2024)
  • Formal Consistency Checking over Specifications in Natural Languages
  • Formal Methods for Distributed Computing in Future Railway Systems (2024)
  • Formal Modeling and Verification of Blockchain Consensus Mechanisms using Process Algebra
  • Formal Specification and Implementation of Distributed Lazy Group Membership Protocol (2025)
  • Formal specification and SMT verification of quantized neural network for autonomous vehicles (2025)
  • Formal Specification, and Verification of a Cooperative Multi-robots System for Delivery Service
  • Formal Specification and Verification of API Security Based on Design by Contract (2024)
  • Formal Specification and Verification of MQTT Protocol Using CoQ Proof Assistant (2024)
  • Formal Specification and Verification of Protection in Transit (PIT) Protocol Using UPPAAL (2025)
  • Formal Specification and Verification of Time-Sensitive Drone Systems using TLA+: A Case Study (2024)
  • Formal Specification-Based Code Review via LLMs (2026)
  • Formal Specification of Distributed Consensus with Partial Observability
  • Formal Verification (2025)
  • Formal Verification and Security Analysis (2026)
  • Formal Verification of a Crash-Safe File System Based on Non-Persistent Conditions Extended Concurrent Separation Logic (2025)
  • Formal Verification of a JIT Backend Compiler (2025)
  • Formal Verification of a Memory Allocator for Rust Hypervisors: From Verified to Deployable Code with Functional Equivalence Guarantees
  • Formal Verification of a Pacemaker (2025)
  • Formal Verification of a Rust-Based Buddy Physical Memory Allocator (2026)
  • Formal Verification of BDI Agents (2024)
  • Formal Verification of Blockchain Consensus Protocols Using Temporal Logic (2026)
  • Formal Verification of Data Integrity and API Security in Distributed Analytics Systems (2026)
  • Formal Verification of Decentralized Consensus Algorithms Using Abstract Interpretation
  • Formal Verification of Decentralized Consensus Algorithms Using Process Algebra
  • Formal Verification of Decentralized Consensus Protocols using Abstract Interpretation
  • Formal Verification of Distributed Byzantine Fault Tolerance Protocols via Abstract Interpretation
  • Formal Verification of Distributed Consensus Algorithms using Model Checking
  • Formal Verification of Distributed Consensus Algorithms using Temporal Logic
  • Formal Verification of Distributed Consensus Algorithms with Symbolic Execution
  • Formal Verification of Distributed Consensus Algorithms with Temporal Logic (2026)
  • Formal verification of distributed, data-intensive microservice applications using Petri Nets
  • Formal Verification of Impure Coq JITs (2025)
  • Formal verification of time-bounded BPMN model with message broker using timed automata (2026)
  • Formalization of security
  • Formalizing Requirements into Dafny Specifications with LLMs (2025)
  • Formally Verified Lock-Free Software Transactional Memory for Scientific Measurement
  • ForMAt: Formal Verification of Scalable Multiply and Accumulate Units (2025)
  • From C to verifiable Rust: Towards practical migration of code and specifications (2026)
  • 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 (2026)
  • Graphical-Probabilistic Modeling of Generative Flows in LLM-Native Software Systems
  • HAMILTON’S PRINCIPLE AND THE INVARIANTS
  • Heterogeneous Face Recognition Using Domain Invariant Units (2024)
  • 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
  • Interoperability Challenges and Machine Learning Protocols for Scalable Distributed Automation Systems Across Intelligent Industrial Workcells
  • Investigation of Formal Verification of Autonomous Vehicle Control Systems Through Specification Translation from Cafeobj to Real-Time Maude
  • Is truth futureproof?
  • Is truth futureproof? On the possible futures of mechanized proofs
  • LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean
  • Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification (2025)
  • Leveraging Cryptographic Simulator Synthesis for Formally Verifying the FOO E-Voting Protocol
  • Leveraging LLMs for Formal Software Requirements–Challenges and Prospects
  • Live: Learning Video LLM with Streaming Speech Transcription at Scale
  • LLM-aided automatic modeling for security protocol verification (2025)
  • 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 Predicate Discovery and Data Augmentation for Learning Likely Program Invariants (2025)
  • LLM-Powered Structurer: Normalizing Natural Language to Information Delivery Specification for Industrial Data (2026)
  • Machine-Checked Proofs and Automated Verification for Post-Quantum Distributed Systems
  • Machine Learning for Automated Theorem Proving using Reinforcement Learning (2021)
  • Map the blockchain world: A trustless and scalable blockchain interoperability protocol for cross-chain applic (2025)
  • MASA: A Modular Framework for LLM-Driven Multi-Agent Systems for Autoformalization
  • MASA: LLM-Driven Multi-Agent Systems for Autoformalization (2025)
  • Meet MASKS: integrating distributed knowledge and verification for multi-agent systems (2025)
  • Meta-Learning for Automated Theorem Proving
  • Model verification of real-time and distributed stream processing architecture (2024)
  • Moving Beyond Specification Validation to Specification Refinement with Mutation Verification
  • Multi-Agent Systems and Control Theory (2025)
  • Neuro-Symbolic Programming with Reinforcement Learning for Automated Theorem Proving
  • On the Formal Verification of Smart Contracts and Blockchain: Challenges and Future Directions (2024)
  • OpenProver: Agentic and Interactive Theorem Proving with Lean 4 (2026)
  • Operational intelligence at enterprise scale: Federated control assurance, multi-agent coordination, and value
  • Parameterized Verification of Timed Networks with Clock Invariants
  • Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support
  • Privacy-preserving techniques in biometric systems: Approaches and challenges
  • Probabilistic Formal Verification of Distributed Consensus Algorithms
  • Probabilistic Safety Verification of Distributed Systems: A Statistical Approach for Monitoring (2025)
  • Probably Correct: Rethinking Formal Verification for LLM-Driven Systems (2025)
  • ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimizat
  • PROV-AGENT: Unified provenance for tracking AI agent interactions in agentic workflows (2025)
  • Provable AI ethics and explainability in medical and educational AI agents: trustworthy ethical firewall
  • Quantum-Enhanced Distributed Systems: A Practical Framework for Autonomous Agent Networks (2025)
  • Ranking Formal Specifications using LLMs (2025)
  • Reinforcement Learning for Automated Theorem Proving
  • Reinforcement Learning for Automated Theorem Proving with Symbolic State Representation
  • RvLLM: LLM Runtime Verification with Domain Knowledge (2025)
  • Safe: Enhancing mathematical reasoning in large language models via retrospective step-aware formal verificati (2025)
  • SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols: An Update (2024)
  • Scalable Verification and Validation of Concurrent and Distributed Systems (ScaVeri) (Track Summary)
  • SCION and cross-border payments: Enhancing security and compliance in distributed ledger networks
  • Secure Synthesis of Distributed Cryptographic Applications (Technical Report) (2024)
  • Securing the model context protocol (mcp): Risks, controls, and governance
  • Security of the Lightning Network: Model Checking a Stepwise Refinement with TLA+ (2025)
  • Semi-Formal Verification (2025)
  • Sieve and Acto (testing Kubernetes controllers for liveness and safety bugs): the search result says 46 bugs for Sieve (OSDI 2022
  • Six-Layer Formal Verification of a Safety-Critical AI Governance Kernel
  • SoK: Agentic Skills–Beyond Tool Use in LLM Agents
  • SpecFSM: Extracting and Repairing Finite State Machines from Protocol Specification Documents (2026)
  • Specification (2026)
  • Specification-Driven Test Generation for Fault Localisation in Dafny
  • Specification of Autonomous Behavior
  • SpecIntelli: Leveraging LLMs for Formal Specification and Verification from Natural Language Requirements
  • STAFF: Towards Translating Formal Verification Benchmarks between Formal Specification Languages (2026)
  • Symbolic AI for Automated Theorem Proving with Adaptive Rule Synthesis (2026)
  • Temporal Logic Verification of Distributed Consensus Algorithms
  • 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 (2026)
  • Title: Self-Organizing Constraint Propagation for Automated Theorem Proving
  • TLCrafter: Peeling the Layers of Natural Language to Reveal Temporal Logic Specifications (2026)
  • Towards Formal Modeling and Verification of the Stellar Consensus Protocol in Z3 (2025)
  • Towards Formal Specification of Agent-based Transport Models
  • Towards Language Model Guided Proof Automation
  • Towards the Formal Specification of Iot Systems (2024)
  • Towards the LLM-based generation of formal specifications from natural-language contracts: Early experiments w
  • Trainverify: Equivalence-based verification for distributed LLM training (2025)
  • Typestates Specification and Verification in Frama-C (2025)
  • Utilizing LLM Chatbots for Formal Descriptions of Cryptographic Protocols (2025)
  • Validating Generative AI Outputs Through Co-Generation of Code and Specifications
  • 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)
  • Verifying Rust code with Verus
  • VerusSeek: Retrieval-Augmented LLM-Based Proof Synthesis for Rust Programs (2026)

not judged yet

78 leads.

  • A design science research approach to Large Language Model-Based Agents for Requirements Specification (LLMBA4RS) in low-code applications.
  • A Distributed Network-Based Runtime Verification of Full Regular Temporal Properties.
  • A formal framework for black-box conformance testing of distributed real-time systems.
  • A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors.
  • A Novel Design in Formal Verification Corresponding to Mixed Signals by Differential Learning.
  • A Proof-of-Transactions Blockchain Consensus Protocol for Large-Scale IoT.
  • Achieving Distributed Control through Model Checking.
  • An efficient Proof-of-Authority consensus scheme against cloning attacks
  • An Iterative Decision Refinement Framework for LLM-based Flight Control System
  • Applying Formal Methods to SOA and SaaS Service Compositions for ERP Systems
  • Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models.
  • Blockchain Technology: Consensus Protocol Proof of Work and Proof of Stake
  • Checking That Finite State Concurrent Programs Satisfy Their Linear Specification.
  • Compositional Synthesis of Concurrent Systems through Causal Model Checking and Learning.
  • Conformal PID Control for Time Series Prediction
  • Conformalized matrix completion
  • Consistency-preserving propagation for SMT solving of concurrent program verification.
  • Counterexample-guided abstraction refinement for symmetric concurrent programs.
  • Dealing with practical limitations of distributed timed model checking for timed automata.
  • Design and verification of multi-rate distributed systems.
  • Distributed Symbolic Model Checking for ”-Calculus.
  • Efficient parametric model checking using domain-specific modelling patterns
  • End-to-End Statistical Model Checking for Parameterization and Stability Analysis of ODE Models.
  • End-to-End Statistical Model Checking for Parametric ODE Models
  • Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes
  • Firefly: Shedding Light on Verification Gaps using LLM-Powered Mutation Testing.
  • Formal Behavioural Specification of Concurrent Systems Without Globality Assumptions.
  • Formal methods
  • Formal Modeling and Verification of a Federated Byzantine Agreement Algorithm for Blockchain Platforms
  • Formal Semantics of a Class of High-Level Primitives for Coordinating Concurrent Processes
  • Formal Verification of Network Interlocking Control by Distributed Signal Boxes.
  • FV-PAL: Scalable Formal Verification through Partitioning and LLM-Guided Property Generation.
  • GPU Accelerating Statistical Model Checking for Extended Timed Automata.
  • Impact of ChatGPT on Educational Strategies for Future-Proof Business Data Analyst: Machine Learning Code Generation in Teaching and Learning
  • Improving and Optimizing Verification and Testing Techniques for Distributed Information Systems.
  • Integrating Predicate Transition Nets with First Order Temporal Logic in the Specification and Verification of Concurrent Systems.
  • Interlocking Control by Distributed Signal Boxes: Design and Verification with the SPIN Model Checker.
  • Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking
  • iscasMc: A Web-Based Probabilistic Model Checker
  • Issues in distributed timed model checking.
  • LASP: LLM Assisted Security Property Generation for SoC Verification.
  • LASSO: LLM-Aided Security Property Generation for Assertion-based SoC Verification.
  • LBFL: A Lightweight Blockchain-Based Federated Learning Framework With Proof-of-Contribution Committee Consensus.
  • LLM-Based Multi-Artifact Consistency Verification for Programming Exercise Quality Assurance
  • LLM-Based Scheme for Synthesis of Formal Verification Algorithms.
  • LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference.
  • LTL Model Checking of Interval Markov Chains.
  • Model checking concurrent systems with MSVL.
  • Model Checking of -Independent Unbounded Petri Nets for an Unbounded System.
  • Model Checking Probabilistic Distributed Systems.
  • Modeling and Verification of a Fault-Tolerant Real-Time Startup Protocol Using Calendar Automata.
  • MPC-Coder: A Dual-Knowledge Enhanced Multi-Agent System with Closed-Loop Verification for PLC Code Generation
  • On the abstract specification and formal analysis of synchronization properties of concurrent systems.
  • Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem
  • Partial Orders for Efficient Bounded Model Checking of Concurrent Software.
  • PoTN: A Novel Blockchain Consensus Protocol with Proof-of-Trust Negotiation in Distributed IoT Networks.
  • Priority Scheduling of Distributed Systems Based on Model Checking.
  • Proof-of-Contribution consensus mechanism for blockchain and its application in intellectual property protection
  • Proof of Learning (PoLe): Empowering neural network training with consensus building on blockchains
  • Proof of Previous Transactions (PoPT): An Efficient Approach to Consensus for JCLedger
  • Proof of service power: A blockchain consensus for cloud manufacturing
  • Quality Prediction of Service Compositions through Probabilistic Model Checking
  • Reliability of Run-Time Quality-of-Service evaluation using parametric model checking
  • Rule Verification Method for Power Operation Order Instructions based on Large Language Model
  • Run-time efficient probabilistic model checking
  • Scaling MPE Inference for Constrained Continuous Markov Random Fields with Consensus Optimization
  • Sequential and distributed model checking of Petri nets.
  • Specification and verification of concurrent systems in CESAR.
  • Specification of highly parallel and distributed resource management.
  • Stateless model checking concurrent programs with maximal causality reduction.
  • Towards LLM-Assisted HDL Generation and Verification.
  • Towards random-honest miners selection and multi-blocks creation: Proof-of-negotiation consensus mechanism in blockchain networks
  • True Concurrency Semantics: Towards a Verification of Timed Systems.
  • Unifying Generative and Classification-Based Relation Extraction via MCTS for nextG Protocol Formal Verification.
  • Verifying Concurrent System Specification in COSY.
  • Verifying Non-functional Properties of Software Product Lines: Towards an Efficient Approach Using Parametric Model Checking
  • Weighted Voting on the Blockchain: Improving Consensus in Proof of Stake Protocols.
  • Ymer: A Statistical Model Checker

Last edited: