My guest appearance on fulltimenix is out now. fulltimenix.com/episodes/hor…

Mouse users are like "Just click a button."

"Why is formal verification exploding NOW?" 1. Nobody understands the code LLMs write 2. Everybody hopes for some deus ex machina

If you’re formally verifying software with Lean and you’re not proving inductive specs you’re doing it wrong Inductive specs allow you to describe and prove powerful properties like “this app will never crash” or “nobody can steal funds”

"Why is formal verification exploding NOW?" 1. Cost of proofs is going DOWN (as AI gets more capable) 2. Cost of exploits is going UP (as AI gets more dangerous) 3. Proofs exterminate exploits 4. Bonus: proof checking = perfect math/coding RL reward The rest is economics

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 ( ͡° ͜ʖ ͡°)

Used visible forall in a GADT today.

You can't hack a function.

Should have used Haskell.

I'm looking for Haskell/Nix positions. Contract or Perm considered. Send me a whistle. openfp.net

On deterministically generated AI documentation. I think you could combine New Ithkuil with a variant of DisCoCirc to create a free monad DSL that you could interpret deterministically into natural sounding English. The LLMs would only be able to construct valid Ithkuil circuits and anything else would fail to type check.

Here's my public quality control handbook that I give to my agents on load. Covers a lot of things, but most importantly how to avoid using python, bash, or basically anything other than Haskell 100% of the time. openfp.net/quality-control/h…

"But why do you need a Haskell console in that?" vortex.openfp.net

Try this prompt. If you have a webapp and want to port it to Haskell. "Can you send ':commands' to this websocket at nixlab.openfp.net/ws, inspect all the projects to learn how to use vortex, then port me over to miso on horizon-javascript at GHC 10.0 with a vortex API on the backend using horizon-platform at GHC 10.0. Keep all my branding and frontend design. Then show me what I can do with this that I can't do with REST."

Here's how I make a merge request on nixlab.openfp.net ``` do mr <- openMergeRequest "systems/ashenvale" "Update README" "This is a description" let n = mrNumber mr a <- setAutoMerge n True b <- setAutoTag n "1.0.0" pure (n, a, b) ``` Then send that over a websocket and it's processed on the server completely safely.

Whether your code is written by a human, clanker, monkey, potato, spatula or white noise generator The answer is still "Use pure functions statically checked with algebraic data types."

Entropy is universal. Just like how search engines died. If you don't put effort into the system the models will eventually collapse. Another way of saying use Haskell.

An excerpt from my QC handbook: ``` #law("Script in vortex, never Python", kind: "review")[ A task you would reach for a script to do — fetching, reading, transforming data — is a vortex program run by a Haskell host. Never Python, and never a bash loop. If no DSL covers the domain, invent one: a typed effect row over a pure interpreter, a host folding it to the answer. Bash and Python have no type, no error value and no composition, so their failures are silent: a lost reply reads as an empty result, a pipe truncates output, and a sweep of 151 calls yields one answer with no error at all. A vortex program fails by refusing to compile, and every answer is a typed value that reaches the reader in full. Whenever a problem is solvable in a single vortex call with a monadic block, it is written as one. ] ```