This large-scale research project (with european funding) might make proof assistants, and in particular Isabelle/HOL, more usable for mathematicians. The [project plan](https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/DoA.pdf) contains many more details on the expected course of actions. This effor...
Thread
Stories related to "ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician" across the full archive.
This large-scale research project (with european funding) might make proof assistants, and in particular Isabelle/HOL, more usable for mathematicians. The [project plan](https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/DoA.pdf) contains many more details on the expected course of actions. This effor...
You can jump straight to the paper [here](https://www.wireguard.io/papers/wireguard-formal-verification.pdf) but the main page also has git instructions for reproduction.
The interesting meat is in:
* https://github.com/mitls/hacl-star
* https://eprint.iacr.org/2017/536.pdf
* https://github.com/mit-plv/fiat-crypto
* https://people.csail.mit.edu/jgross/personal-website/papers/2018-fiat-crypto-pldi-draft.pdf
Abstract: "We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of network functions and proves properties...
Formal Semantics and Automated Verification for the Border Gateway Protocol (2016)
(conferences.sigcomm.org)
Trimmed abstract: "We present the first mechanized formal semantics of the BGP specification RFC 4271 [14], and we show how to use this semantics to develop reliable tools and guidelines that help BGP administrators avoid router misconfiguration. In contrast to previous semantics, our semantics is f...
Extending the correctness proof of [VigNAT: A Formally Verified Performant NAT](https://vignat.github.io/).
Code available at https://github.com/vignat/vignat
> The ability to tolerate, remediate, and recover from network in-
cidents (caused by device failures and fiber cuts, for example) is
critical for building and operating highly-available web services.
Achieving fault tolerance and failure preparedness requires sys-
tem architects, software devel...
Abstract: "Vehicle-to-Vehicle (V2V) communications is a “connected
vehicles” standard that will likely be mandated in the U.S. within the
coming decade. V2V, in which automobiles broadcast to one another,
promises improved safety by providing collision warnings, but it also
poses a security risk...
Formal CHERI: design-time proof of full-scale architecture security properties
(lightbluetouchpaper.org)
SmartCookie: Blocking large scale SYN floods with a Split-Proxy Defense on Programmable Data Planes
(engineering.purdue.edu)
Formal CHERI: design-time proof of full-scale architecture security properties (2022)
(lightbluetouchpaper.org)
Corrected for original story.
Challenges in Designing at Scale: Formal Methods in Building Robust Distributed Systems
(perspectives.mvdirona.com)