Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Summer Internships using Coq at CertiK

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Summer Internships using Coq at CertiK


Chronological Thread 
  • From: Vilhelm Sjöberg <vilhelm.sjoberg AT certik.io>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Summer Internships using Coq at CertiK
  • Date: Fri, 1 Apr 2022 17:07:31 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vilhelm.sjoberg AT certik.io; spf=None smtp.mailfrom=vilhelm.sjoberg AT certik.com; spf=None smtp.helo=postmaster AT mail-vs1-f44.google.com
  • Ironport-data: A9a23:a2YS0KAPowfcnBVW/xLlw5YqxClBgxIJ4kV8jS/XYbTApDgh1TcPm moWXWCAOKyJYWf9KoslPI7goU4Cv5WDm4A2OVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yE6jMlkf5KkYAL+EnkZqTRMFWFw0XqPp8Zj2tQy2YThWlvW0 T/Pi5S31GGNi2Yc3l08sPrrRCNH5JwebxtF1rCWTakjUG72zxH5PrpHTU2CByeQrr1vIwKPb 72rIIdVUY/u10xF5tuNyt4Xe6CRK1LYFVDmZnF+A8BOjvXez8A/+v5TCRYSVatYoxbWzu9vy MtWiZ21EV80HKDwleAaVxYNRkmSPYUekFPGCX22sMjW0VafNnWwn7NhC0Y5OYBe8eFyaY1M3 aZAeXZdM1bZ3r3wnO7TpupE3qzPKOH1PYcft3VliyrbCvwrW5/rSKjQ+d5bmjw3g6iiGN6EN pRCM2c0NXwsZTUWEVw6NrAVmduq3GTSTSFfuWzKrLMotj27IAtZieCxarI5YOeiTsJM202cu 2ju5HX8GhhcNdqFyDPD/GjEuwPUtSbyWYZXCqbhs/A23BucwWscDBBQXly+yRWktqKgc/EAe nMK+jQ1kak3rBS2bNTBUhm/pHHR63bwROFsO+E97QiMzI/d7ACYGnUIQ1Z9hDoO5J9eqdsCh g/hoj/5OdB8mObKFi/Fp994uRv3aHdFdzZTDcMRZVJdu4GLnW0lsv7Yoj9e/EOdi9T0HXTu2 GnPonRiwboUisEP2uOw+lWvb9OQSnrhHlRdCub/BDrNAuZFiGiNOdbABb/zs6woEWphZgPd1 EXoYuDHhAz0MbmDlTaWXMIGF6yz6vCOPVX02AAzT8Z8rmj1oyX+LOi8BQ2Swm85Yq7onhe5M CfuVf95ufe/wVP2Nf8mOtrvYyjU5fi+TIy/PhwrUja+SsEpKFXvENBGakmX0GTg+HXAYoluU ap3hf2EVC5AYYw+lGTeb75EjdcDm35jrUuOGsiT50n2idK2OS/OIZ9YYQvmRr5jsMus/l6Om /4BbJvi9vmqeLehCsUh2dVDcw5iwLlSLcyelvG7gcbYeVU2QDhxUqCJqV7jEqQ895loei7z1 inVcidlJJDX3BUr8C2GNSJubq3BR5F6oS5pNCAgJw/wiXMue5qu7+EUcJ5uJesr8+lqzPhVS fgZepTQXqsUGm2WozlNP4PgqIFCdQiwgV3cNSSSZj86b5M9FRfC/cXpf1S++XBWXDa3r8Y3v 5apyhjfHcgYXw1nAcuPMKCvwlq9sGIzguV3W0eUcNBfdF+9ooNnMTDwjbk2JJhUexnEwzKb0 SeQAAsZ/LSU/dFsq4iW263d9tWnCepzGEZeDlL317fuOHmI5HenzK9BTP2MImLXWlTy/6Cya LgH1Pr7KvAGwwdH6tIuD7ZxwKsizNLzvLsGnB98FXDGYln3WLNtJn6KgZtGuqFXnOQLvAK3X geR4YAfN+nVfsziF1EVKUwuaeHajaMYnTzb7PIUJkTm5X8ooODWDx0KZxTc2jZAKLZVMZ8+x btzssAh7QHi2AEhNcyLj3wJ+mnQfGYMVb4r6sMTDIPx0FF5z1hDZdnCEXaz7s3TLdpLNUYuL 3mfg6+b3+ZQwU/LcnwSE3nR3LoC2c5f5kgSlFJSdU6Untflh+Ms2EED+zoASAkInA5M1Ph+O zQ2OkB4TUlUE+yEWCSRs6GQ9wB96Nmx/0Xwzx4XjzScQRX0EGPKK2I5NKCG+0VxH6ewuNRE1 Onw9YoneW+CkALNMu8aUkN/t/3gC9d282UuXSxh89utR/EHjPmMvkNqTWEFsQfmAoUwgyUrY AWsEPlYMcXGCMLbn0H350R2G1jdpNBo6VGumc1cwZ4=
  • Ironport-hdrordr: A9a23:qV42G6Pm8PsfVMBcTsyjsMiBIKoaSvp037BL7TEXdfUxSKalfq +V7ZcmPHPP6Ar5O0tApTnjAtjjfZq0z/ccirX5Vo3SOTUO1lHYSL2KLrGP/9QjIUDDHyJmup uIupIRNOHN
  • Ironport-phdr: A9a23:rTLSsRxd4IM8l0nXCzIjwVBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z haZvKszxwaUAM3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmT owZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsipyey+4YDfbgRJiTayfL9/L BW7phjNu8cLhodvNrw/wQbTrHtSfORWy2JoJVaNkBv5+8y94p1t/TlOtvw478JPXrn0cKo+T bxDETQpKHs169HxtRnCVgSA+H0RWXgLnxVSAgjF6Bb6Xortsib/q+Fw1jWWMdHwQLspXzmp8 qVlRwLyiCofODE38G/ZhM9tgqxFvB2svAZwz5LObYyPKPZyYqHQcNUHTmRBRMZRUClBD5uzY IsOC+oBPfhXr434p1QWsBW+Bw+0C/jxxT9SiX/9wKo30/ogEQHC3AwvAdYOsHHOoNXuNqcSV vu6w7fSzTXMdP5ZxSny6JLUchAgovGAR7Nwcc3IxEQpCgjKgUmep5b/MDOJyuQCrXKb7+x4W O+rimMqpBx8ryaxysoolITFmp4Yx1HZ+Ct33Ys4Jt22RVJ0b9O6H5VcqT2XO5Z4TM0sQmxkp ig3x74atZC7YiUHzoksyRDYa/yCaYeI4xTjWf6VIThmmnJqZqi/iwyu/kinzOD3S8q60E5So yZbjtXBsmoB2h/T58SdVPdx40Ws1SyA2g3c7OxPPFo6mrDBK5E7x749jpoTvlrHHi/xgEj2i bWZdkQg+uSx9eTneajqqoaSN4J7hQzyKKsumsu4AeQ3NggBQXKX9vi71L3m5UH5QbNKgeMqk qTBrpzWOcAWqrS6DgJVyIov9QuzAjW83NkXknQLNFdFdwiGj4jtNVHOOvf4DfKnjlSykTdrw /DGMaPlApXINHTDi7XhfbFm5EFC0gozwstS6I5KBbEbPPLzW0zxuMbEAR8+Ngy42+DnB85l2 YMERW2PGrOZML/VsVKQ++4jO/OMa5MNuDbhN/gl4ObjgmM+mV8EZKWmwZ8XaG2jEfl9OEWYY X/sgs8bHmsQvwo+SvbqiFyYXjJJaXayRfF02jZuA4W/SIzHW4qFgbqb3S79EIcFSHpBDwWyE HPoeoGBbMwO9iifOMApxiIFUbisT4pnzhOpvgLgxJJsI/DI+y5etJW1h4s93PHaiRxnrW88N M+ayWzYFwmc/0sNTj4yhuVkpFBlj02E2u5+iuBZEtpa47VIVB07PNjS1b8yEMj8DyTGeNrBU 1O6WpO+GzhkUNM1w9IKZgBmGdKogwrM9yGnGaMUlPqKA8986brSil72Ics10HPazO8khlgiT NFIMDi4h6p/+gzWQZXLlE+UjamCfqkGwC/OsmyEyDnGp1lWBSh3V6iNRnUDfg3WoND+s1vFV KOrAK87PxFpzMeDLu5UcYSsgwkaAvjkP9vabiS6nGLY6Q+g4LSKYcKqfmwc2H+YE00Yi0UJ+ n3AMwEiByCnqmaYDTp0FFupbVm+ue954Gi2SEM51WToJwVoyqa19xgJhPedV+Jb37QKvz0ko il1G1D11szfCt6JrQ5sNKtGZtZ17FBC3GPf/wtzW/7oZ75jgl4TdwExpEHp3RhtBa1LnNI2r XBszQ0zYaOU3VVddi+JiIjqM+6ySCG69xSuZqjKn1DGhYzOq+FftbJi8gql4F36cyhqu29q2 NRUzXaGs5DDDQ5IFIn0Tl5y7R9x4bfTfig64YrQk3xqK6i99DHYiLdLTKMozAite9BHPeaKD gj3RocEBsyuJegv3UOraRgJJu96/6MuI8KlMfCB3eT4WYQo1CLjlmlB7I1nhwiS9i58R+rNm Y0HxPuVxASvXDrmkFai9MHw09MhB3laDi+0zi7qA5RUb6t5cNMQCGugFMaww813m5/nX3MwG EeLIVQA1YfpfBOTawa4xghMzQENpnfhnyKkzjtymjVvr6yF3SWIzf6wPBwAcnVGQmVvlzKOa cC9kswaUU60bgMoiArt5ED0wLJerbh+KG+bSFlBfiz/JWVvGqWqsb/Kb8lK4ZIu+SJZNYb0K U6bTr7wpx5cyCHkFWZEyxgweiu2u5a/lBt/ySqcIHt1sHvFaJR1zBbb6sbbQK00vHJOTy15h D/LQ1mkaoPxrJPEytGZ67/4Cz7yM/8bOTPmxo6BqiahsGhjABnl2uu2hsWiCw8xlynyy9htU yzM6hf6eIjikaqgYocFNgFlAkHx781iF8RwiIw10dsO2Hwai5GQu2EFlm3+K9pz0q/kcHsOA zUMxpSGhWqtkF0mNX+Py4/jAz+Dw89hat2/JHgU3Sgw9c9iA6qO8L1H2yBypxDryGCZKeg4l TAbx/w07XcciOxcowshwBKWBbUKFFVZNyjh//iRx/a5qqgfJGOmcLzqkVF7gcjkFraJ5AdVR Hf+fJ4mWy529MR2dlzWgjX17cn/dd/cYMh21FXcmgrcj+VTNJM6l+YbzSthN2XnuHQ5yuk9x RVw1JC+tYKDJi1j5qW8ShJfMzT0YYsU9FSPxe5Gmd2K2om0Aph7MjACXZ+tU+nxVTxO6bLoM AGBFDB6oXCeWPLeEQKZ9EZ6vifPHpSsZBT1bDESydRvQgXYJVQK2lhFGmVn2MRgSUb2mJ+EE g8x/D0a61/mpwEZz+tpM0O6SWLDvEKybTxyTpGDLR1Q5wUE5kHPMMXY4PggekMQtpCnsgGJL XSWIgpSCmRcEFKFA1DuOrzo/tvH+eWCCcK1IuHSYLbIoutbHaTtp9rnws598jCAO9/adGFlF OE+01FfUGpRHs3Yn3ARUHVSmX6RKcGcoxi492t8qcX1o5GJEEr/oICIDbVVK9Bm/Ru71LyCO +CnjyF8MT9E15kIyBcgKZAa1V8Wzj91LnyjTehGuinKQ6bd3KRQCkxDA8ucHMBF9b493U9GP suJ0rsdM5Zzg+QpClQDVFuzwqmU
  • Ironport-sdr: aE20CLe0ylDM8Wj2nHbiL/xHhLqTZX7RxrCYrlLu+HB8lUV6xyY6me2i4Zd3wX70m3LRwzDPAx FbaqF60BIBEuKoGXyj6zyAgOFS5xmnUL44BdcfS1zs69lo6qPbD1GVD7IaK6HJShfwvJ7m1tg1 QKgSEfOGIaFogg9kTcrpQ//X4QFwE0S00LALZ5QitmNDFOXV8nrr6LAH+VxjeDFaeQWh0O0W7y RccrWucH/nzRHkjJdQfV9wwzWOKcr+NYq1k/5gNehYloWpcTSuX+NDGpGgTP0W6IuaOO7CA5c1 8i3qCcRw8SXzC/ZLA1wGT4oJ

CertiK is a world-leading cybersecurity firm that focuses on smart contract analysis and blockchain auditing. It was founded by prof. Ronghui Gu (Columbia) and prof. Zhong Shao (Yale), drawing on their research about formal verification.

Currently the CertiK Certified Systems group is developing tooling to verify smart contracts and blockchain implementations. We are looking for summer interns to help us develop these tools, and to use them to reason about real-world blockchain software.

Available project include developing embeddings of more programming languages into Coq; and to prove theorems about applications such as decentralized finance, bytecode interpreters, and consensus protocols. The internship is suitable for current master/phd students, or strong undergraduates looking for research experience. The position is completely remote, and is open on a year-round basis.

Qualifications

You should be familiar with formal verification using Coq (e.g. from the Software Foundations textbook or similar), and ideally have experience with non-trivial Coq projects.

[Preferred] Proficient in Haskell, Plutus, Rust, Go, or Solidity; or experience with blockchain and smart contracts; or knowledgeable about SMT-based systems like Why3 or Boogie.

Please send applications via https://jobs.lever.co/certik/d961cd21-44cf-4757-bc72-cc742fb7da2e

Best regards,
Vilhelm Sjöberg


  • [Coq-Club] Summer Internships using Coq at CertiK, Vilhelm Sjöberg, 04/01/2022

Archive powered by MHonArc 2.6.19+.

Top of Page