Papers

• LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean (2026)
  Simon Jeanteur et al.
  4.39
• Rzk: a Proof Assistant for Synthetic $\infty$-Categories (2026)
  Nikolai Kudasov et al.
  4.39
• Chemical Chain-of-Thought Functions as a Hallucination-Prone Molecular Scratchpad (2026)
  Jiatong Li et al.
  4.39
• Automating Formal Verification with Agent-Guided Tree Search (2026)
  Leo Yao
  4.27
• Proving the Coding Interview: A Benchmark for Formally Verified Code Generation (2025)
  Quinn Dougherty and Ronak Mehta
  4.25
• Theoria: Rewrite-Acceptability Verification over Informal Reasoning States (2026)
  Michael Saldivar et al.
  3.51
• 130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? (2026)
  Josef Urban
  1.67
• CFaults: Model-Based Diagnosis for Fault Localization in C Programs with Multiple Test Cases (2024)
  Pedro Orvalho and Mikol\'a\v{s} Janota and Vasco Manquinho
  0.72
• Polymorphic Type Inference for Machine Code (2016)
  Matthew Noonan et al.
  —
• Formal Modelling, Testing and Verification of HSA Memory Models using Event-B (2016)
  Ashish Darbari et al.
  —
• Stepwise Debugging of Answer-Set Programs (2017)
  Johannes Oetsch et al.
  —
• An Assertion-Based Program Logic for Probabilistic Programs (2018)
  Gilles Barthe and Thomas Espitau and Marco Gaboardi and Benjamin Gr\'egoire and Justin Hsu and Pierre-Yves Strub
  —
• Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation (2018)
  John P. Gallagher et al.
  —
• Lightweight Interactive Proving inside an Automatic Program Verifier (2018)
  Sylvain Dailler (Inria et al.
  —
• Dijkstra Monads for All (2019)
  Kenji Maillard et al.
  —
• ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity (2020)
  Dan Frumin et al.
  —
• SPPL: Probabilistic Programming with Fast Exact Symbolic Inference (2020)
  Feras A. Saad et al.
  —
• Conditional independence by typing (2020)
  Maria I. Gorinova et al.
  —
• CertiStr: A Certified String Solver (technical report) (2021)
  Shuanglong Kan et al.
  —
• Reasoning about Interior Mutability in Rust using Library-Defined Capabilities (2024)
  Federico Poli et al.
  —