2 papers
cs.LO2026
CSLib: The Lean Computer Science Library
Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi +5
We introduce CSLib, an open-source framework for proving computer-science-related theorems and writing formally verified code in the Lean proof assistant. CSLib aims to be for comp…
cs.LO2025
Relational Hoare Logic for Realistically Modelled Machine Code
Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee +4
Many security- and performance-critical domains, such as cryptography, rely on low-level verification to minimize the trusted computing surface and allow code to be written directl…