Paper proves no finite rulebook can certify every safe program
Watching can catch every prohibition violation, but no safe program can be cleared for good.
Stories per day · 30 days
2 RSS
Relatedai-agents1confidentiality1dram1gatekeeping1graph-search1information-flow1isabelle1lean1llm-agents1mathlib1memory-safety1program-verification1prompt-injection1retrieval1rowhammer1runtime-monitors1theorem-proving1
17 stories, newest first · one card per story
Stories tagged #formal-methods
PlanTERS formalizes relative security of prompt injection in agents
Revoking injectable tools at the first untrusted read is proved relatively secure on finite runs.
Paper gives probabilistic semantics for Rowhammer-style bit flips
A collapse theorem says physical separation makes protected executions match the fault-free run for every finite prefix.
Lean Graph Search for Formal Theorem Proving
LeanGraphSearch retrieves supporting Lean lemmas via dependency graphs and lifts theorem-proving pass rates.
Verification with Transfer: Exact Information Frontiers and Their Price in Calls
Theory paper prices source-task calls that cut verification cost, with Lean-checked bounds and a transformer test.
Hierarchical Security Monitoring for Edge-IoT: A Formal Methods Approach
Hierarchical TeSSLa and MonPoly monitors detect cross-device edge-IoT attacks while sending only compact verdicts upstream.
Trust a Few: The Weakest Assumptions a Protocol Needs
A verifier loop computes the weakest key, value, and channel assumptions a protocol needs to meet a goal.
Security Properties of Neural Networks as Decision Problems
Researchers classify neural-network security checks as co-NP-complete or harder, including backdoors and parameter faults.
LLM-Assisted Automatic Security Proofs for Cryptographic Protocols: How Far Are We?
LLMs produce useful cryptographic-protocol lemmas but average only 38.82% proof-tree coverage.
Formally Modeling the Terrapin Attack on SSH
Researchers formally model the Terrapin SSH attack and show which AEAD modes remain secure.
Staged Multi-step UTXO Workflows via Recursive Invariants
Paper proposes recursive invariants, a transaction-level logic and typed DSL, to enforce multi-step UTXO workflow rules without shared mutable state.
Probabilistic Linear Explanations
Researchers introduce a unified probabilistic explainability framework using sparse anchored linear models that outperforms LIME and MAPLE on relevance error.
The Mathematical AI Safety Institute wants to prove AI is safe the way cryptographers prove codes are unbreakable
Fields Medalist Jacob Tsimerman founds the Mathematical AI Safety Institute (MAISI) to pursue provable AI safety guarantees, launching January 2027.
On Identifying Sound Conditions for Frontrunning Resistance
Researchers formally define smart-contract frontrunning resistance, showing 55% of 393 audited vulnerabilities escape state-of-the-art detection, and find two undisclosed Ethereum flaws.
Towards Tackling Application Logic Flaws through Autonomous Formal-Logic Modeling and Automated Reasoning
LL-Verifier combines LLMs with logic model checking to automatically discover logic flaws, uncovering vulnerabilities in 27 IoT access-control protocols.
How well do agents use test/verification techniques?
Dan Luu's eval finds coding-agent testing instructions (TDD, formal methods, PBT, skills) mostly fail to beat defaults on Zstd implementation correctness.
CONTINUITY: Security-Context Contracts for Composable LLM Agent Controls
Researchers introduce CONTINUITY, a framework of assume-guarantee contracts that preserves LLM agent security context across components, verified across 2,560 attack instances.