Winkle

Okay, let's do this. Isabelle, Lean, and Rocq (formerly Coq*) are theorem provers. They are meant to prove mathematical theorems. We use them for formal verification by either 1) translating a program to the theorem prover (risking a translation error) or 2) using a language built into the theorem prover that extracts into a working binary. Fizzbee, TLA+, Spin, Alloy, Quint, and P are specification languages. They are meant for checking high-level blueprints of programs. After checking the blueprint, you still need to make sure your program matches it, which is a hard problem. Specification languages differ in what they make easy to express. P, Spin, and Fizzbee are designed to be closer to the code implementations. P looks like interacting state machines, Spin looks like C with CSP, Fizzbee looks like a dialect of Python. It's easier to use a codelike specification language and refine it to code, but you can't do as much with it. Alloy, TLA+, and Quint are more abstract. Alloy looks like a bunch of algebraic relationships, TLA+ is a much of logical formula, and Quint is a programmer-oriented (and statically typed) condensation of TLA+. Abstract modeling languages are harder to get started with and harder to represent things, but you can represent a wider class of systems with them. I believe UPPAAL is a specification language for realtime systems. This is a field I have no experience in. It seems a graphical language, though, which would make LLM-assistance difficult. Dafny is a verifiable programming language. It has regular programming language features, but also a bunch of features to express and prove properties of the program. It uses SMT solvers to actually prove the properties, meaning you don't need to learn a proof language (though you need to learn to cajole the solver). Dafny is probably the easiest thing on your list to get started with, but also the least likely to meet any weirder needs you might have. I don't know what Ivy is but some cursory Kagiing suggests it falls in the specification language category. Some other things @spin_lock_init didn't mention: - Other theorem provers: Agda, Metamath - Other abstract specification languages: mcrl2, NuXMV, Event-B - Other verifiable programming languages: Idris, F*, Whiley - There's also using a verifiable subset of a language, like Verus for Rust or SPARK for Ada. So, what you need to pick depends on what you want to do. You'll get the maximum power with a theorem prover. Lean is the de facto language for vibeproving, but Anthropic recently published a post about vibeproving in Rocq so YMMV. If you want to make abstract models of software systems, go for a specification language. Which you choose depends on a lot of factors. If your system can be represented as lots of simple communicating state machines over a network, try P. Spin, I believe, is close to simple C/Go with a network and channels. I have never used Fizzbee. Alloy is good for domain modeling, but struggles with really complicated temporal actions, nested data structures, and largish numbers. Also AIs aren't to good at it (last I checked, in March). Runs fast and makes good visualizations though. TLA+ and Quint are for modeling complex temporal systems. I'm partial to TLA+ but know a lot of people who say Quint is easier to get into. Note P, Fizzbee, and Quint all claim to have features for testing a codebase against a spec. I can't vouch for any of them, though. None of the languages I mentioned (except maybe NuXMV?) are particularly good at modeling sequential, deterministic algorithms. Use Dafny if you need to just write a verified program and don't care which language it's in. I don't think other verifiable programming languages are as user-friendly for the time being. Consider a verified subset if you already know a language and want to just augment it with more correctness. You may need other, more exotic tools depending on your particular needs. Regardless of the above advice, don't be afraid to use the wrong tool for the job. If you vibe well with a language, and you achieve good LLM-sympathy with it, you'll be able to go farther than using a "right tool" you don't like.

Pleased to announce my first @AntithesisHQ project: a property testing webinar! In property testing, instead of checking "this input to the function has this output", we check "given a million random inputs, all the outputs have this property". PBT has been around for a quarter century now and is fairly well known in functional programming and distributed system circles. Which is why we're gonna do something very experimental and target a community that almost never uses PBT: web developers. See, there's a thousand PBT tutorials out there, and they all use examples like "reversing a list twice returns the original list" and "add(x, y) should return the same result as add(y, x)". These are stateless properties on the code's functions, where we randomize inputs to a fixed test sequence. People have a hard time finding useful stateless properties in their systems. I've come to believe that most intuitive and useful business properties are instead stateful properties on what must always hold about the system's states. For example, "our total spend is always below our budget cap", or "two talks must never be scheduled for the same room and time", or "free users can't access premium features". We can property test these by randomizing the test sequence itself, to simulate a user doing whatever the heck they want, and testing that no matter what they do, our properties still hold. So, if you've ever had your data model get corrupted because you forgot to validate one update method, or seen a 500 when the user clicks `send` three times in a row, or gotten mad at SQL for not enforcing cross-table constraints, this webinar is for you. We'll be live on October 29. Sign up here: pages.antithesis.com/webinar…