Max von Hippel

• Max von Hippel 10 Sep 2026 18:39 UTC

  5 points

  0

  in reply to: StanislavKrym’s comment on: Can you hear the shape of a Lean sound­ness bug? A wa­ger.

  Relevant yes, but not to the outcome of the conjecture. Ramana found this bug and used it cheekily as part of the rollout for his company, which uses Candle, a verified verifier he co-authored. But in that case, anyone (including Claude) who reviewed his Collatz proof, was able to find the fact that the “proof” was cheating. My claim (which Thomas disputes) is that within one year, such a “proof” will survive AI-based and human scrutiny, despite being incorrect.

Can you hear the shape of a Lean sound­ness bug? A wa­ger.

• Max von Hippel 7 Sep 2026 14:25 UTC

  1 point

  0

  in reply to: Jason Gross’s comment on: Fund­ing For­mal Meth­ods for the Cyberpocalypse

  Sorry for the slow reply here Jason! And thank you for the thoughtful comment.

  If you carve reality at the right points, specification is easy.

  I think I am just very skeptical this can, in general, be done. In your example of a sandbox, your spec would have excluded anything with any kind of web access whatsoever, since any web access necessarily opens the door to side-effects. Such a sandbox would never have been used by the big labs on account of excluding the specific web-browsing behaviors they want to train for. Therefore, it is a useless, academic specification.

  In general, I maintain nearly all systems which are “easily” specified like that are actually not easily specifiable, once the specifier encounters the reality of the needs of capital.

  Alas, nobody has released a full machine-readable model of any hardware used in production yet.

  MIPS is used in production, e.g. in some internet routers, and is simple enough you could do this quite quickly with Claude. I’m sure there’s plenty of hardware that’s simple enough to reverse engineer and formalize. Maybe it’s worth doing so just to show it’s possible?

  Verified compilers are just a cost-saving (proof sharing) technique for binary-level verification.

  Totally disagree, they are also a way to bootstrap specification, since all the types in the language form a kind of latent spec. Moreover it is considerably easier to write a spec relative to an abstraction than it is relative to a concretization.

  If we are verifying everything, why not just verify that we have caught all bugs that could ever be caught by fuzzing?

  I assume an adversarial world in which, due to the needs of capital, many systems remain black boxes, and it is nevertheless a social good to report bugs/​vulns to maintainers. This is a considerably more realistic assumption than the idea that you will get to formally verify Microsoft Word.

• Max von Hippel 2 Sep 2026 9:28 UTC

  1 point

  0

  on: A Mechanis­tic Ex­pla­na­tion of Prompt In­jec­tion (and why you should study roles)

  I found this really interesting. One thing which I feel you did not address is DoS attacks. There are certain kinds of attacks which DoS a model by making it collapse into repeating the same string over and over … I feel like these are more of an information theory problem than a role-hacking problem.

• Max von Hippel 18 Aug 2026 21:08 UTC

  2 points

  1

  in reply to: Quinn’s comment on: Fund­ing For­mal Meth­ods for the Cyberpocalypse

  Hi Quinn, this is really interesting and I’d love to see it written up when you get a chance!

  I know Wil Robertson has had some success with agentic fuzzing. I wonder if we can get him to comment on what’s worked and what hasn’t, and why …

• Max von Hippel 18 Aug 2026 21:07 UTC

  2 points

  2

  in reply to: Adam Chlipala’s comment on: Fund­ing For­mal Meth­ods for the Cyberpocalypse

  Hi Adam! I strongly agree RE the benefits of longstanding institutions. When I went through YC I found it really striking how few SF engineers understood the degree to which American academic institutions are totally load-bearing for industry. For all its foibles, there’s no other institution as effective as the PhD program for producing new foundational research and skilled researchers.

  I hadn’t seen your post on regularly regenerating all code. I just read it and I think it’s really good! I’m curious what you think about the problem I bring up, of spec elicitation (what Mike is working on). IE, how do we know which properties of pre-existing software are important to preserve when we rewrite, formalize, and so forth? Is this something you’ve thought about, or have opinions about? It seems very challenging to me (I am not at all sure that this is something we can rely on AI for ..) but maybe I am thinking about the problem incorrectly.

Fund­ing For­mal Meth­ods for the Cyberpocalypse

• Max von Hippel 3 Aug 2026 2:13 UTC

  2 points

  0

  in reply to: Sam Marks’s comment on: Is Mythos good at cy­ber be­cause it kept hack­ing An­thropic’s sand­boxes dur­ing train­ing?

  Hi Sam, I wonder if this is just because none of the tasks during training were ones where hacking Anthropic would, in fact, be the shortest route to success?

  Additionally, I would argue that this distinction is pretty moot:

  In the case of privilege escalation, the Mythos Preview acquired greater permissions within its sandboxed RL environment than it was intended to have, but not by breaking out of the sandbox.

  Surely part of the definition of the sandbox is the enforcement of the permissions any agent within it is assigned, thus, the agent still broke the sandbox. It just … didn’t need further privilege escalation than what it achieved, in order to accomplish its goals. Or am I wrong?

  On a separate note, I’d really like to know if Anthropic is aware of any instances, ever, of a model hacking a formal verification tool as a form of reward hacking? Since I (maybe) have your attention here, if you do know the answer to this question and are willing to share, I’d really appreciate it! (E.g., Lean, Rocq, z3, etc.)

• Max von Hippel 3 Aug 2026 2:07 UTC

  1 point

  0

  in reply to: Azimov’s comment on: The Scal­able For­mal Over­sight Re­search Program

  I agree with everything you’ve said! (If this is a research program you want to work on, please email me, and I will connect you with very well funded people working on these problems.)

• Max von Hippel 29 Jul 2026 6:05 UTC

  2 points

  0

  in reply to: BryceStansfield’s comment on: Your soft­ware should build itself

  Hi Bryce! I like this point a lot. I think however that there are several semantic features which are possible in my formulation, but not in yours. For example, it would be nice to have some safety features, such as certain kinds of memory safety, laid out, and then require that these features are preserved by any change to the language (so the agent must supply a proof thereof). I can imagine a number of safety criteria which I might want preserved in this fashion. Another, in a cryptographic context, might be “constant time” (more precisely: runtime is independent of secret inputs).

Your soft­ware should build itself

• Max von Hippel 17 Jun 2026 18:51 UTC

  2 points

  0

  in reply to: Koby Lewis’s comment on: The Scal­able For­mal Over­sight Re­search Program

  I am concerned about this, and I am also a bit defeatist about timelines for AI “solving” SWE … not sure how to balance these things. I think my loose intuition, which I am open to changing, is that AI will get superhuman at SWE in less than 2 years (maybe much less) and it’s unclear if they’ll be any good at formal methods on such a timeline, so I may as well push for FM so we have some possibility of control via formalism. However, I may be disastrously wrong here and invite any argument to the contrary ..

• Max von Hippel 17 Jun 2026 18:49 UTC

  2 points

  0

  in reply to: β-redex’s comment on: Lies, Damned Lies, and Proofs: For­mal Meth­ods are not Slopless

  Yes! I believe Axiom AI has been involved with this effort.

How to Solve Se­cure Pro­gram Synthesis

• Max von Hippel 23 Feb 2026 18:58 UTC

  2 points

  0

  on: The Scal­able For­mal Over­sight Re­search Program

  FYI: Jocelyn Qiaochu Chen and collaborators just this morning released VeriSoftBench, “a benchmark for repository-scale Lean 4 verification proofs”, which I think is a really compelling project and highly relevant to the benchmarks/​evals section of my post above.

• Max von Hippel 23 Feb 2026 2:21 UTC

  9 points

  6

  in reply to: Nathan Helm-Burger’s comment on: The Scal­able For­mal Over­sight Re­search Program

  Bend is extremely cool. I’ve been following HigherOrderCo for a while. They were invited to the last two FMxAI conferences but never wrote back. We’d really love to get them to come to the 2026 one. If you know anyone there please make an intro :)

The Scal­able For­mal Over­sight Re­search Program

• Max von Hippel 8 Feb 2026 18:08 UTC

  1 point

  0

  in reply to: Stanislav Fort’s comment on: AI found 12 of 12 OpenSSL zero-days (while curl can­cel­led its bug bounty)

  Hi Stanislav, can you expand on what you mean when you say you’re using FM? I.e., are you referring to symbolic analysis /​ concolic analysis techniques, model checking, formal methods in the sense that you dispatch a question of “go right or go left?” to z3, formal methods in the sense of grammar-based fuzzing or property based testing (lightweight FM), or do you mean you’re doing full-blown theorem proving (I don’t exactly see why you would be doing this but I’m open to being told I’m wrong :) )

• Max von Hippel 28 Jan 2026 3:19 UTC

  15 points

  0

  on: AI found 12 of 12 OpenSSL zero-days (while curl can­cel­led its bug bounty)

  This is a really interesting post, thank you! I recently tried to explore the bottom of the capability curve (what can you one-shot?) but have been struggling to get a glimpse at the top (what can the most well orchestrated, well designed AI systems achieve?) and appreciate your detailed writeup as offering some clear insight into that latter question.

  Coming from academia, my strong prior is that system designers kind of know what to look for ahead of time, and build tools to find outcomes they strongly suspect will exist. IE, often a fuzzer will seem perfectly designed to find just the specific bug(s) reported in the paper, and nothing else … almost as if the authors knew about those ahead of time, or strongly suspected they’d exist, and designed the system accordingly. I wonder if you could comment, along those lines, on what findings Aisle has produced autonomously or semi-autonomously which surprised you and fell outside the envelope of results you’d deliberately designed the system to prosecute?

• Max von Hippel 26 Jan 2026 15:59 UTC

  1 point

  0

  in reply to: noahzuniga’s comment on: Can you just vibe vuln­er­a­bil­ities?

  Thanks @noahzuniga ! I think the continuum of AI capability very, very roughly looks like:

  1. AI cannot even help with this task.

  2. AI can help an expert human with this task.

  3. AI can mostly do this task autonomously, with some light steering and feedback from a human.

  4. AI can do this task autonomously provided the right harness design.

  5. AI can basically one-shot this task.
     
     My blog post, IMO, confirmed we are not at stage 5 yet. I am very confident we are at least at stage 2. I am not certain where in the range [2, 4] we fall currently, though. I plan to do more work to further refine my assessment.