co-founder @kronuscorp
Melbourne, Australia
Joined March 2017
- Tweets96
- Following434
- Followers463
- Likes34.7K
deffo gonna start telling investors that thinking about returns is a pretty shallow way to approach a funding round
yesterday my barber brought up Rocket Lab organically. turns out he's a massive fanboy, tells everyone about the company, bet the house on $RKLB .
we spent the entire haircut talking about rockets and space systems.
not long ago, I was telling investors "I used to work at a company called Rocket Lab. believe it or not, they build rockets."
Patrick Bellamy retweeted
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.
i'd bet ~$800B in future compute and infrastructure commitments prob puts them near the top of some leaderboard too
every company should replace their software architects with AI immediately.
except us.
we're special.
Patrick Bellamy retweeted
@welltyped this is ridiculously cool.
bindgen.well-typed.com
All software and hardware will be verified against a spec nobody reads, by a model that also writes the implementation. This can only end well.
Patrick Bellamy retweeted
Top 9 Formal Methods/Verification predictions:
1. Formal methods alone will not eliminate all kinds of bugs. What I’m calling “Empirical Verification” via sophisticated simulation testing, CUA, etc. will become more important than ever.
2. Languages won’t matter but barriers to adoption will still be relevant especially for startups with customers that they’d need to migrate codebases for, enterprises, etc.
3. For cost and pricing, the economics are improving but there is still high cost demands for infrastructure that are to be figured out. See more in point 7 below.
4. Models will significantly improve and intent alignment will take center stage. Even the best models today prove the wrong thing many times without sophisticated tooling, etc. The model by itself will not be enough here.
5. Engineering workflows are going to drastically change. Engineers will move into long running tasks in parallel that run for overnight to weeks, meaning we will work faster in higher quantity. But fast, iterative work that you push and get back instant results for will not be the norm anymore. Coding agents have tricked us into thinking we’re getting high quality, verified results instantly but that is not the case. This too will improve over time.
6. Vibe coding, consumer/indie development overall, and gaming will have very interesting windfalls as a result of formal methods scaling (at least in terms of applications end users will notice in their day to day). Not including crypto, finance, cloud, hardware, etc. that are already seeing and have been seeing strong results.
7. Languages are only one piece of this. Hardware, and compute are another but there will be an entire class of infrastructure that we’ll need in addition to great work on languages and across the board software. Honestly this is where one of the biggest risks lies. For this to work at scale, the infrastructure doesn’t exist and will require significant innovations and languages are not even there yet. As an engineering community if we want to win we need diversity of choice and we need to avoid lock in. That means helping contribute to different formal languages and you can start with the ones that are tied to your use case. Here’s a brief selection map I wrote:
- Agents writing production code today (especially Rust): Verus
- Checking a distributed design: TLA+
- Math: Lean
- Bend 2, Vera, Vow and Kōdo: worth watching, still very early though.
There’s others so feel free to fill them in, we can have an interesting conversation about them. Just get started for what works for you. Also you help the engineers working on building products around these to accelerate work that comes back for you to use. For example, I’m committing a lot of work to Verus which is OSS to give back. Join me.
It’s pretty obvious the big guys are betting on Lean, Verus, TLA+, Dafny. Which, if you think about the unit economics of this and future vision, makes a lot of sense. Also if you read “FV X”, many of the engineers and researchers that are formal methods experts are pushing these too. There’s a reason. Also, there is less risk of having to rip out your work and start over if you want to get started now. And you can benefit from a rich engineering community already contributing to these languages with large amounts of funding. I like spreading out your contributions so no singular method is locked in and also because each is attuned for specific type of work. The most important thing is to have conviction and just contribute. I’m currently bullish on Rust so I’ve been pushing Verus.
8. Hiring will be impacted. As I mentioned this space is ripe for direct innovation and in tangential research areas, such as intent alignment. Understanding Verification Engineering and I mean understanding it for both Formal and Empirical Verification will help you a lot. This is another reason to look into the above languages as ways for working with the frontier AI labs, neo labs, and big tech companies. There’s a very limited number of formal methods experts today and even less that can combine Formal Verification, Empirical Verification, and Agentic Engineering.
9. “Vibe Verification” via just natural language skills or plugins, etc. will take the market by storm because it’s satisfying to have instant feedback. At times they will maybe even prove valuable, meaningful things and perhaps are good enough for some cases. But they are definitely not good enough for actual commercial or enterprise products or real security today. Be wary of and do not pay for Vibe Verification. Just like with all the test bloat that we had to rip out, if you vibe verify your codebase then it will be filled with slop you’ll have to pull out in the future. As model capabilities improve the last thing you want is poor formal spec examples that are incorrect for these models to reference inside of your codebase. Save yourself the trouble.
I could be wrong about everything and also right about a thing or two, but I think for collective success and transparency we should share our predictions and work together.
Follow me for more on Verification and Agentic Engineering.
Patrick Bellamy retweeted
It is a weird weird year to be a formal methods expert.
Some unorganized thoughts on the new @AnthropicAI and @theoremlabs post on formal verification (anthropic.com/research/forma…):
- This is very cool.
- The main innovation is verifying a later stage of the program. Normally provers take the source code, LLM it into a theorem language, and then prove that, which means you have to make assumptions about source semantics and compilation properties. It's very easy to make a mistake in translating and prove the wrong thing!
What they instead do is compile the code into assembly, and then (if I understand this correctly), compile that assembly into a theorem language (which they call LPS). So as long as the compiler is faithful you can skip the whole divergence problem.
- I'm glad they clarify that you still have to trust the translation process, the "hardware, OS, OCaml" compiler, the LPS model, and also assume that the program is single threaded with fixed memory. The single biggest source of errors in formally verified code is when the proof assumes something that isn't true in practice. It's really, really important to state your assumptions!
- I'm not clear why they need to compile the fuzzer into the theorem. Is it to act as a description of valid inputs and workload? Maybe to embed assertions in as theorems?
- Holy crap, 180 million lines of Rocq. Is that more Rocq than exists in the world already? I notice they say a 600,000 line proof corresponds to roughly 20k CPU instructions. That would be like, 1-2k lines of source code at most? Really goes to show how inefficient this approach is and how it only works because you can throw LLMs at the problem.
- This, probably deliberately, doesn't address the single biggest gap in AI-based verification: AIs cannot come up with good properties. Doesn't matter if you're doing unit testing, property testing, formal verification. I always assumed this was a "frontier labs haven't trained for it yet" thing, but if Anthropic hasn't talked about that here, maybe they've tried and haven't been successful yet. That's interesting to me.
Instead, they take a known universal property (this code doesn't crash or get flagged by UBsan) and prove that instead. Still very useful, but makes it harder to generalize to proving arbitrary things about arbitrary programs.
- Anybody reading the official post should also read their expert review appendix (www-cdn.anthropic.com/files/…). It points out some interesting things, like the fact that most of the code the LLM wrote wasn't used in the proof (over one billion lines of Rocq), that they had to prove the equivalence between fuzzed and unfuzzed programs, and (this is most interesting), some experiments find that the LLM-method of proofwriting may not scale to more complex things.
- Also read the description of LPS (github.com/theorem-labs/oss-…) to understand the limitations of the assembly -> Rocq compilation. In particular, it does not handle concurrency at all (which is one of the main use cases for formal methods!) or OS signals. Also it can't prove things about program arguments with slash characters, meaning they can prove stuff about `rm foo` but not `rm foo/bar`.
- The official skill (github.com/theorem-labs/oss-…) doesn't tell us much about the nature of FM and AI. Probably too much for me to hope of any skill.
- Some of the article's specific caveats and throat clearings make me think someone at Anthropic reads my stuff ( ͡° ͜ʖ ͡°)
Patrick Bellamy retweeted
At this point, if you’re in software and aren’t currently working on a plan for moving to formal verification, it’s irresponsible.
The writing is on the wall. This needs to be your priority now.
New on our Frontier Red Team blog: using Claude to formally verify software at large scale.
Formal verification can prove that code is free of certain bugs, but historically it has only been feasible for small codebases (or required a lot of expert time).
With AI models, however, this is beginning to change. In collaboration with @theoremlabs, we used Claude to prove security properties in over one hundred real-world open-source libraries over the span of a few weeks.
Read our research in full here: anthropic.com/research/forma…
some poor NSA intern is about to become a full time poster
Effective Immediately, all organizations using PHP for their systems are advised to be prepared for an update addressing two critical vulnerabilities. PHP is widely used for web applications. These vulnerabilities often provide a direct path to the server's file system or database. If an immediate update is not feasible, it is recommend that organizations take the system offline until it can be fully mitigated. NSA will follow up shortly with more specific guidance.
Patrick Bellamy retweeted
How do you _guarantee_ your agent's code is correct? You prove it.
Introducing Proof Driven Development Kit (PDD Kit) from @MSFTResearch.
PDD Kit helps turn your plan into a formal spec, then proves the agent's code meets that spec for every input. No vibe verification. PDD Kit is integrated with @GitHubNext's Chopin, so you can plan as a team.
PDD Kit takes an app's login flow from intent to a verified pull request:
It discusses your code, infers your intent as it goes, and proposes a formal spec in Verus, a proof language for Rust.
Once you approve the spec, the Verus verifier automatically proves the code meets it.
Where proof isn't possible, it falls back to empirical verification with tests and computer-use agents (CUAs).
It works on Rust today. No new language, no change in how you produce the underlying code, making formal methods more accessible.
The goal is a verified software factory, where engineers review specifications instead of code.
Come see it in action at GitHub Universe, Oct 28–29. Swing by the Speakeasy and ask for GitHub Next!