From Byron Cook AMA, Amazon is using Coq for verifying security protocols right now https://www.youtube.com/watch?v=jGgQmnPH0dQ
cool!
do they have any publications on this?
I guess we might find out, the AMA is ongoing. Nothing in his list of current publications though.
so Amazon has gone beyond TLA+
he says they are using a lot of different stuff, e.g., Z3 standalone, CVC4 standalone, Dafny.
he says one could/should use massive distributed proof search (e.g., for inductive invariants), and this is not widely done in any system/proof assistant right now. Take single question, apply 10k machines, get linear speedups.
One example where they have used Coq: Continuous Formal Verification of Amazon s2n, CAV '18 https://link.springer.com/chapter/10.1007/978-3-319-96142-2_26
Yes, Byron already talked about using Coq in his keynote at FLOC 2018.
IIRC they used it to formally verify some SSL/TLC protocol or stuff like that.
FWIW, they are not using only Coq since they have John Harrison as one of their employees...
FWIW, they are not using only Coq since they have John Harrison as one of their employees...
if I understood correctly they've recently hired Michael Ernst (part-time?) and previously they have Rustan Leino as well. Lots of FM expertise there.
Last updated: Oct 13 2024 at 01:02 UTC