Jonathan Protzenko

@_protz_

Formal verification, cryptography, type systems, and stuff

Joined September 2010

Tweets

You blocked @_protz_

Are you sure you want to view these Tweets? Viewing Tweets won't unblock @_protz_

  1. Jan 31
    Show this thread
    Undo
  2. Jan 31

    Made it to DC. Couldn't get a ticket to attend the impeachment so I'll stick with instead.

    Show this thread
    Undo
  3. Jan 31

    Denis is wise and is not on Twitter. But I'll be forwarding to him the oh-so-vital "tweet impression statistics" and whatnot.

    Show this thread
    Undo
  4. Jan 31

    The corresponding research article, alas, is only in French: time to brush up your skills and parler français

    Show this thread
    Undo
  5. Jan 31

    My student Denis wrote a formal semantics for the French tax code, complete with Coq proof of soundness and SMT queries to uncover unfair tax hikes. PL for fiscal justice!

    Show this thread
    Undo
  6. Jan 24

    For all your cryptographic needs (ahem, e.g., HACL*) use a formally verified, constant time-preserving C compiler! at

    Undo
  7. Jan 22

    Thanks to all who attended and contributed thoughts and conversation to HASE 2020 and made it a great workshop! Now on to

    Undo
  8. Jan 7

    Too many lambdas in your POPL program? Consider registering for HASE ! You'll even get to meet the mythical "practitioner" in a laid-back, interactive setting with an audience-driven agenda...!

    Undo
  9. Retweeted

    Now at , ⁦⁩ and ⁦⁩ talk about EverCrypt and formally verified cryptographic primitives, promoting formally verified crypto as the future for software implementations.

    Undo
  10. Retweeted
    19 Dec 2019

    What to know who will be talking about what? Check out the 2020 list of speakers here:

    Undo
  11. 13 Dec 2019

    * start. I had proofread this twice 😭

    Show this thread
    Undo
  12. 13 Dec 2019

    New blog post! GitHub strange, or the weird repositories you find when you starting digging into commit data... with a cameo appearance by

    Show this thread
    Undo
  13. Retweeted
    10 Dec 2019

    When someone's bonus or promotion depends on them shipping a "spec" or a feature, it's hard for them to accept feedback that the whole thing is a bad idea and should be dropped.

    Undo
  14. Retweeted

    Yes, French GDP has grown more slowly than GDP here. Much of that is slower population growth. And you do need to ask, growth for whom. Most French live *better* than their US counterparts 2/

    Show this thread
    Undo
  15. 27 Nov 2019

    Congratulations ! Thrilled to see verified cryptography finally landing in the Linux kernel. It's been a long road, but hopefully follow-ups will be easier.

    Undo
  16. Retweeted
    27 Nov 2019

    Now that Frankenzinc has landed, v1 of the WireGuard patchset has been submitted upstream to Linux:

    Undo
  17. 22 Sep 2019

    2009, Sept. 19th, commit message "Initial prototype". 10 years later, "Manually sort folders" is still the 4th most used addon for Thunderbird -- the motivation to maintain it is gone but pull requests for fixes keep coming. On to another 10 years I guess?

    Undo
  18. Retweeted
    2 Jul 2019

    EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider: J Protzenko, B Parno, A Fromherz, C Hawblitzel, M Polubelova, K Bhargavan, B Beurdouche, J Choi, A Delignat-Lavaud, C Fournet, T Ramana

    Undo
  19. Retweeted
    11 Jun 2019

    "This is one of the most gorgeous applications of Formal Methods and automated tools that I've ever seen". Watch Peter Neumann make blush at: Rest of the talk is great too!

    Undo
  20. 29 May 2019

    The Dagstuhl Summer School on Metaprogramming is coming up! I'm thrilled (albeit slightly stressed out!) that I'll be giving a course there with other such great speakers. Looking forward to seeing applications coming in

    Undo

Loading seems to be taking a while.

Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.

    You may also like

    ·