Stream: Coq users

Topic: Coq use at Amazon


view this post on Zulip Karl Palmskog (Jun 17 2020 at 16:11):

From Byron Cook AMA, Amazon is using Coq for verifying security protocols right now https://www.youtube.com/watch?v=jGgQmnPH0dQ

view this post on Zulip Anton Trunov (Jun 17 2020 at 16:11):

cool!

view this post on Zulip Anton Trunov (Jun 17 2020 at 16:12):

do they have any publications on this?

view this post on Zulip Karl Palmskog (Jun 17 2020 at 16:12):

I guess we might find out, the AMA is ongoing. Nothing in his list of current publications though.

view this post on Zulip Anton Trunov (Jun 17 2020 at 16:13):

so Amazon has gone beyond TLA+

view this post on Zulip Karl Palmskog (Jun 17 2020 at 16:13):

he says they are using a lot of different stuff, e.g., Z3 standalone, CVC4 standalone, Dafny.

view this post on Zulip Karl Palmskog (Jun 17 2020 at 16:17):

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.

view this post on Zulip Yao Li (Jun 17 2020 at 16:19):

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

view this post on Zulip Théo Zimmermann (Jun 17 2020 at 17:30):

Yes, Byron already talked about using Coq in his keynote at FLOC 2018.

view this post on Zulip Théo Zimmermann (Jun 17 2020 at 17:31):

IIRC they used it to formally verify some SSL/TLC protocol or stuff like that.

view this post on Zulip Théo Zimmermann (Jun 17 2020 at 17:33):

FWIW, they are not using only Coq since they have John Harrison as one of their employees...

view this post on Zulip Théo Zimmermann (Jun 17 2020 at 17:33):

FWIW, they are not using only Coq since they have John Harrison as one of their employees...

view this post on Zulip Karl Palmskog (Jun 17 2020 at 17:54):

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: Dec 05 2023 at 04:01 UTC