Sam MillerBenjamin: An AI Assistant for a Proof AssistantI am heading for the home stretch on self-studying Software Foundations Volume 1. I have a few more questions in the last chapter I plan on…Dec 2, 2023Dec 2, 2023
Sam MillerFormal Education: Self-Study with Coq and ChatGPTThere are many different tools available to verify whether or not a system will run correctly. While mostly I’ve explored model checkers…Oct 7, 2023Oct 7, 2023
Sam MillerCounting Vowels the Hard Way: or, How to Save a Tenth of a Second Every 100 MegabytesAt work we have daily messages in slack, and sometimes, there are coding challenges. They’re all generally pretty basic, focusing on…Apr 19, 2023Apr 19, 2023
Sam MillerAn Introduction to Model Checking with TLA+This month, I’m challenging myself to complete an online university lecture series in Introduction to Model Checking. The course is taught…Mar 28, 2023Mar 28, 2023
Sam MillerDebugging a YouTube Code AlongI think YouTube is one of the greatest education resources in the world. There are probably hundreds, maybe thousands, of free…Mar 19, 2023Mar 19, 2023
Sam MillerMeta-Models for Web APIs in TLA+ and FORMULAModel-driven engineering (or architecture, or development, or whatever) is not very popular in most web development shops. There are…Jan 26, 2023Jan 26, 2023
Sam MillerConcurrent Bank Withdrawals in Pluscal and PI had so much fun playing around with TLA+ and Coyote (see the most recent) that I decided to keep going with comparing some other formal…Jan 9, 2023Jan 9, 2023
Sam MillerManaging Accounts in Coyote and PluscalBuilding off the previous examples of the Bounded Buffer in TLA+ and Coyote, this time I did a little reverse engineering. If there’s an…Dec 14, 2022Dec 14, 2022
Sam MillerBounded Buffers with TLA+ and Coyote — Part 2: ConditionalsWhen I wrote Part 1, I wasn’t really expecting a Part 2 so soon. However, funny things happen when you post on Twitter. Markus Kuppe, who…Dec 3, 2022Dec 3, 2022
Sam MillerBounded Buffers with TLA+ and CoyoteI’ve been exploring formal methods for the better part of the past year, ever since a graduate course on Automated Verification put the…Nov 27, 2022Nov 27, 2022
