> A human, you can hold accountable, and you can keep them at a good security posture with short-lived session tokens.
You can do this too (and better) with a repo: OIDC/Workload identity trust relationship between github and aws for short lived tokens + a github environment setup that requires manual approval.
Bonus: It also gives you an audit trail with a github action log as opposed to a sysadmin running something on a laptop.
The problem here was mostly that they (for some reason) happened to use (and leak) a PAT.
This is the way. And the benefit that still makes it more worth it today, is the fact that you can have truly self-service and peer reviewed infra provisioning and don't depend on a single sys admin or several of them colliding on their machines.
Results seem somewhat reasonable given that the amount of verus/TLA/Creusot/Lean code out there is tiny compared to all the other non-formal code.
So it's understandable that the agents wont be able
to go beyond proving trival things, given how much more difficult it is to write such code.
A (more) interesting experiment (to me) would be to write a high level spec manually for a non-trivial system (liveness etc.) and see if the agent can produce an implementation using guided refinements that satisfies this specification.
Yeah, the interesting thing to me with formal methods is where you write some (partial) specs to tell the LLM what you want. It'll do the usual stuff, plus extra proof work to make sure your intent was actually realized.
Throwing tools haphazardly at the LLM and hoping they increase the correctness of its output is expectedly pretty ineffective. Good to see this borne out in the article.
Strongly agree with the author here. The future will belong to programming languages that natively embed theorem proofers into their type systems so LLMs can forego a lot of testing by just validating the implementations they write against the specs with formal proofs. Writing formal specs is probably the main skill a programmer in the future will need to get work done.
Verus (https://github.com/verus-lang/verus) is a good start for the rust ecosystem, but it's essentially a standalone language today (with custom syntax and type system).
Lean has dependant types. Wouldn't something like Haskell or Idris, that are trying to be general purpose dependantly typed languages--wouldn't they be a better start than versus?
Versus appears to just be a formal verification tool. Perhaps I misunderstand?
You want the formal verification built into the language because the tooling can start to get really crazy good. Agda is the dependantly typed language I've used the most (long ago), and the tooling was interactive in a helpful way I've never experienced with other languages.
You don't want a separate language used to verify a base language, because then everyone ends up having to know two languages. Looking at the history of computing though, I wouldn't be surprised if this happens.
The actual programming language and the verification language can be the same language though, if we want.
I did write small programs myself, but mostly with Claude Code. It was very pleasant to work in it with Claude Code. Implemented a shell and 40 of coreutils. Did not really get very far with proving properties of them, but had working programs. Reading Lean4 is pretty nice. Nicer to read than OCaml, almost as nice as Haskell.
I don't see why it would be particularly difficult beyond not already having a lot of IO libraries (like Kafka connectors or whatever). Pure functional programming in Scala with IO monads is quite pleasant.
in case anyone's interested i have a vibe coded fork of verus that replaces the verus-the-language side of verus with plain old Lean 4. It's still two languages, but now at least the second language is as mainstream as it gets in the field and has good automation. i haven't finished wiring up the Lean 4 infoview and vs code extensions and LLM skills into it yet, which makes it not as easy to write yet as lean 4 with the IDE bells and whistles.
I'm also playing around with using the lean's compile-to-C tooling to instead compile to rust instead and it's getting more of my focus than the lean-via-verus route right now.
if people are interested, ping me and i can put them up on gh.
I'm currently writing such a language myself in pure Lean, based on adjoint logic -- as well as graded modes and effects. I started by just trying to formally verify a Rust-like borrow checker and at this point I have a working interpreter and LLVM compiler and a formally verified kernel.
All type checkers are theorem provers, btw, that's just Curry Howard. The question is exactly how expressive they are.
Focus on formal verification is a technique to "harden" an unreliable LLM that produces meaningless slop from arbitrary text into a compiler that produces a correct program from a concise, formal input.
"Writing formal specs" means simply programming, taking a step upward in programming language abstraction level, and whether it's going to be easy remains to be seen.
This is the fantasy that has always driven proof systems research. Nobody is going to run software that has never been tested. Would ride a rollercoaster that had never actually been tested before, only "proven" safe? I wouldn't!
So this stuff is always going to be additive and concerned with edge cases, as almost by definition, stuff that isn't edge cases will be found by comprehensive enough testing procedures.
And yet most software doesn't really need to be correct under edge cases, outside of security and data loss issues. People can tolerate a lot of incorrectness in other areas because it's just annoying, not critical.
Security is a case where formal methods could help, but I don't think LLMs will change the industries lack of interest. If anything it'll reduce it even further. Historically security took place in a fog of war. You don't know your enemies capabilities and may not be able to easily match them. But now LLMs are better at finding security bugs than most (all?) humans and ~everyone has access to them, so, from a liability perspective, all you have to do is point a frontier LLM at your codebase and let it fix as many bugs as it can find. Your enemies don't have access to anything better, so once it's done you can tick the box and say security is good enough. Meaning, nobody will fire you if there are still attacks possible.
So in the end I don't see LLMs changing the adoption formal methods.
- Adhere to rules in "Code Complete" by Steve McConnell.
- Adhere to rules in "The Art of Readable Code" by Dustin Boswell & Trevor Foucher.
- Adhere to rules in "Bugs in Writing: A Guide to Debugging Your Prose" by Lyn Dupre.
- Adhere to rules in "The Elements of Style, Fourth Edition" by William Strunk Jr. & E. B. White
e.g., mentioning Elements of Style and Bugs in Writing certainly has helped our review LLM to make some great suggestions about English documentation PRs in the past.
> - Adhere to rules in "The Elements of Style, Fourth Edition" by William Strunk Jr. & E. B. White
FYI: The third edition was the last one by E. B. White. The fourth edition was revised by someone whose identity is unclear. For something so opinionated, I'd like to know whose opinions I'm reading.
Not that it really matters for your LLM prompt, but it's worth pointing out.
Feldera is an incremental query engine, you can think of it as a specialized database. If you have a set of question you can express in SQL it will ingest all your data and build many sophisticated indexes for it (these get stored on disk). Whenever new data arrives feldera can instantly update the answers to all your questions. This is mostly useful when the data is much larger than what fits in memory because then the questions will be especially expensive to answer with a regular (batch) database.
> Depending on your needs, the right tool might be Parquet or Arrow or protobuf or Cap’n Proto
I think parquet and arrow are great formats, but ultimately they have to solve a similar problem that rkyv solves: for any given type that they support, what does the bit pattern look like in serialized form and in deserialized form (and how do I convert between the two).
However, it is useful to point out that parquet/arrow on top of that solve many more problems needed to store data 'at scale' than rkyv (which is just a serialization framework after all): well defined data and file format, backward compatibility, bloom filters, run length encoding, compression, indexes, interoperability between languages, etc. etc.
> it sounds like helping customers with databases full of red flags is their bread and butter
Yes that captures it well. Feldera is an incremental query engine. Loosely speaking: it computes answers to any of your SQL queries by doing work proportional to the incoming changes for your data (rather than the entire state of your database tables).
If you have queries that take hours to compute in a traditional database like Spark/PostgreSQL/Snowflake (because of their complexity, or data size) and you want to always have the most up-to-date answer for your queries, feldera will give you that answer 'instantly' whenever your data changes (after you've back-filled your existing dataset into it).
You can do this too (and better) with a repo: OIDC/Workload identity trust relationship between github and aws for short lived tokens + a github environment setup that requires manual approval. Bonus: It also gives you an audit trail with a github action log as opposed to a sysadmin running something on a laptop.
The problem here was mostly that they (for some reason) happened to use (and leak) a PAT.
reply