🔥The 9th Round of Easy Loan, Earn $40 Reward is in progress❗️ ⏰ Promotion Period: January 15th - Feburary 15th, 2025 👉 Register now and check more details at gate.io/campaigns/358

Ep #21: Nikhil Swamy of Microsoft Research joins Shpat Morina and Joey Dodds on the Building Better Systems podcast to discuss a dependently typed language called F*, what makes it unique, and some of its applications. Listen wherever you find podcasts or watch here: youtu.be/ezoAtruDURY

In an article published in IEEE S&P, Mike Dodds discusses Galois's approach to formal verification of cryptographic systems, focusing on the challenges of building and deploying proofs in demanding industry environments. Thanks to Joey Dodds for contributing. ieeexplore.ieee.org/document/97331…

I’m at PLDI! Here are some ongoing projects that I’m involved with at Galois. I'd be excited to chat about any of these. Free to drop me a DM or come up and bug me in person 🧵

Today is my last day at Galois. Taking a month off then another adventure in automated reasoning begins!

I'm one week in as an applied scientist at Amazon Web Services. Automated reasoning for cryptography and systems already... This is going to be fun!

I wanted to learn some post-quantum crypto, so I formalized a configuration of one of the NIST candidates, Classic Mceliece in Lean 4 theorem prover: github.com/joehendrix/lea…

Ah! This Thursday is Rust Day! Come chat *Adopting Rust on your team* 🦀😀👩‍💻 opensourcelive.withgoogle.com/events/rust-da…

From Joey Dodds and my Strange Loop talk on verifying cryptographic primitives!

"Formally Verifying Everybody's Cryptography" by Mike Dodds Mike Dodds, Joey Dodds Joey Dodds from Strange Loop 2022 youtube.com/watch?v=B_WAb4…

A few years back, Rob Dockins and I implemented and verified an RCV tabulator in Coq. The tabulator is pretty easy to implement and prove, I think it only took a week or two. github.com/FreeAndFair/fo…

So many friends, and role models in this group (even some who are both!). This is a group that will prove to the world that Automated Reasoning is an indespensible component of high quality software. It feels great to be part of it.

Can your verification system of choice prove this function and spec to check if intervals overlap? function overlap l1 h1 l2 h2 : nat -> bool = ! (h1<l2 || h2 < l1) overlap l1 h2 l2 h2 <-> exists x. contains x l1 h1 /\ contains x l2 h2 If so do you have to guide it and how?

I don't think I realized sledgehammer could do things like this. Pretty impressive

IMO the difference at more selective schools is the students, not the teaching. An important reason to go to school in person is for the culture, and in my experience the culture at selective schools is more work and learning centric than at less selective schools.

Just like all relationships, I say love all you want. You also have to set boundaries and have reasonable expectations. Once those aren't respected you can reevaluate. Life isn't as fun if you think of yourself as a mercenary, even if it means disappointment is painful later

Exactly what happens to startup founders with VCs. The only good reason to undertake a PhD or a startup is because you want to do the work itself, not as a means to an end.

I'm not a huge meta fan, and have no idea why metaverse is a "blown" investment, but I do respect them for taking a big shot on innovating with a lot of strong people.

It looks very likely there will be automated reasoning intern spots open with me and others on my team this year. Reach out here if you'd like to chat. Topics include: Program analysis Program synthesis Concurrent systems code and protocol proof Correctness for machine learning

More about these research internships opening this year: Publication is a goal. Out of 5 interns this year we had 3 submitted papers. Possible locations include Portland, Arlington or Seattle. The team is a science team embedded in an engineering org.

I’ve done a lot of formal methods “technical sales” - trying to scope projects for Galois clients that solve their problem and fit into a budget. I gave a talk last week on some things that I learned along the way: mikedodds.github.io/files/talks/20…