IronFleet: proving practical distributed systems correct
1 points by aiono
1 points by aiono
If you prefer reading, they also have a paper.
Is there newer work that follows from this?
There’s work on using Verus which is from the same folks working on IronFleet to verify a couple of different systems https://verus-lang.github.io/verus/publications-and-projects/. Also there’s folks using Iris which is non SMT based to verify MVCC and distributed systems.
The goods, as best I can tell: https://github.com/microsoft/Ironclad/tree/main/ironfleet#:~:text=this%20directory%20contains%20experimental%20verified%20ironfleet%20code%2C%20as%20described%20in (MIT)