Formal Methods
Overview
This area tracks specification, synthesis, abstraction, verification, and proof-oriented tools for intelligent systems.
Active Questions
- Which formal guarantees survive contact with neural function approximation and partial observability?
- What abstractions give the best tradeoff between tractability and fidelity?
- When should verification optimize expected behavior, full distributions, or explicit tail-risk measures?
- How should verification results be surfaced back into the wiki as reusable conceptual knowledge?
- When does a hierarchical or compositional specification preserve behavior while improving tractability?
- How can model-building and causal-temporal formalisms expose where expressivity, decidability, and strategic agency trade off?
- Which product-game abstractions are strong enough to shield learned agents without requiring a full transition model?
- How far can compositional assume-guarantee reasoning push shield synthesis before local obligations become too conservative or manually brittle?
- How can formal responsibility criteria support strategy selection before a trace is realized?
- How can data-derived safe sets be certified conservatively when the model is unknown but structured?
- When does a proof or specification require constructive evidence rather than a classical truth-value argument?
- When does a specification depend on full second-order semantics, and when is a Henkin or automata-restricted reading enough?
- Which proof-assistant workflows should be treated as reusable formal-methods infrastructure rather than just implementation tooling?
- How can safety shields remain interpretable when their synthesized policy is too large to inspect directly?
- Which numerical model-checking bounds are strong enough to serve as runtime safety certificates rather than only approximate diagnostics?
- Which learned safety value functions are conservative enough to serve as certificates or runtime filters?
- Which constrained-learning guarantees are optimization guarantees, and which are formal runtime-enforcement guarantees?
- When do restricted temporal fragments genuinely lower synthesis complexity, and when do they only make automata construction cleaner?
- Which game objectives are expressive enough for controller synthesis while still supporting symbolic solution methods?
- Which real-time duration requirements can be compiled into executable monitors or shields without falling into undecidable fragments?
- Which specification logics are best handled by direct automata translations, and when does translation blowup force a specialized fragment or symbolic method?
- When is a formal specification naturally a linear trace property, and when is it a branching-time property over possible executions?
- When can subsystem-level RL success guarantees be composed into a verified system-level probability guarantee?
- When does a safety claim need an auditable world model, safety specification, and verifier rather than empirical evaluation alone?
Key Concepts
- Reactive Synthesis
- Automata-Theoretic Logic
- Second-Order Logic
- Higher-Order Logic
- Full and Henkin Second-Order Semantics
- Lean Theorem Prover
- Lean Proof Terms and Tactics
- MSO Automata Correspondence
- Branching-Time Temporal Logic
- Branching-Time Semantics
- Hamilton-Jacobi Reachability
- Discounted Safety Bellman Equation
- Compositional Reinforcement Learning
- ICRL pMDP Specification Decomposition
- Safety Games
- Duration Calculus
- Duration Calculus Pacemaker Shields
- Safety and Co-Safety Properties
- Safety LTL Automata and Games
- Emerson-Lei Objectives
- Emerson-Lei Game Solving
- Probabilistic Controlled Invariant Sets
- Shield Synthesis
- K-Stabilizing Shield Synthesis
- Explainable Shielding
- Shield Risk Decision Trees
- Probabilistic Shielding
- Probabilistic Risk-Budget Shields
- Constrained Markov Decision Processes
- Intuitionistic Logic
- PCIS Safety Predecessor
- EXPTIME
- Probabilistic Model Checking
- Sound Value Iteration
- Sound Value Iteration Bounds
- Probabilistic Strategic Timed CTL
- Runtime Verification
- Predicate Abstraction
- Invariant Synthesis
- Linear Temporal Logic
- Automata Learning
- Reward Machines
- Reward Machine Learning Methods
- Centralized and Factored MARL Shielding
- Distributed Shield Synthesis
- Alternating-Time Temporal Logic
- Dynamic Epistemic Logic
- Temporal Causal Models
- Actual Causality
- Responsibility Anticipation
- Distributional Value Iteration
- Guaranteed Safe AI
Key Sources
- Bartocci2018 - Introduction to Runtime Verification
- Vaananen2024 - Second-Order and Higher-Order Logic
- Karunus2026 - All Lean Books And Where To Find Them
- Hofmann2025 - Automata Theory and Logic
- Goranko2023 - Temporal Logics
- Fisac2019 - Bridging Hamilton-Jacobi Safety Analysis and Reinforcement Learning
- Neary2022 - Verifiable and Compositional Reinforcement Learning Systems
- Bloem2015 - Shield Synthesis
- Rieder2025 - Explainably Safe Reinforcement Learning
- Achiam2017 - Constrained Policy Optimization
- AbuseOfNotation2026 - The Case Against Boolean Logic
- Jamroga2026 - Towards Probabilistic Strategic Timed CTL
- Vinzent2026 - Probabilistic Safety Verification of Neural Policies via Predicate Abstraction
- Luo2022 - Automated Synthesis of Generalized Invariant Strategies
- Elsayed-Aly2024 - Distributional Probabilistic Model Checking
- Alinejad2026 - Dynamic Automaton Refinement and Planning for Non-Markovian RL
- Toro Icarte2022 - Reward Machines
- Furelos-Blanco2023 - Hierarchies of Reward Machines
- ElSayed-Aly2021 - Safe Multi-Agent Reinforcement Learning via Shielding
- Brorholt2025 - Compositional Shielding and Reinforcement Learning for Multi-Agent Systems
- Dolgorukov2024 - Dynamic Epistemic Logic of Resource Bounded Information Mining Agents
- Galimullin2025 - Changing the Rules of the Game
- Varricchione2023 - Synthesising Reward Machines for Cooperative MARL
- Gladyshev2025 - Temporal Causal Reasoning with Non-Recursive SEMs
- Gladyshev2026 - Temporal Causal Models as a Model of Computation
- Parker2024 - Responsibility in a Multi-Value Strategic Setting
- Hashimoto2026 - Data-Driven Synthesis of Probabilistic Controlled Invariant Sets for Linear MDPs
- HamelDeLeCourt2025 - Probabilistic Shielding for Safe Reinforcement Learning
- HamelDeLeCourt2025 - ProSh Probabilistic Shielding for Model-free Reinforcement Learning
- Quatmann2018 - Sound Value Iteration
- Latvala2002 - Efficient Model Checking of Safety Properties
- Zhu2020 - A Symbolic Approach to Safety LTL Synthesis
- Artale2023 - Complexity of Safety and coSafety Fragments of Linear Temporal Logic
- Hausmann2024 - Symbolic Solution of Emerson-Lei Games for Reactive Synthesis
- Dole2023 - Correct-by-Construction Reinforcement Learning of Cardiac Pacemakers from Duration Calculus Requirements
- Dalrymple2024 - Towards Guaranteed Safe AI