[weitendorf]

I have been working on metaparsing and some related tools for spec-based-development, fuzzing, and property-based-testing off and on for the past few months. I hope to make it easier for application developers to get the benefits of formal verification without having to spend inordinate amounts of time or resources writing unfamiliar, difficult formal-verification software or tests. You're right that it's not useful for most developers to concern themselves with this now, but I think that's mostly just because nothing makes it easy enough yet.

> Even property-based testing is mostly unhelpful for e-commerce apps like these.

Only in practice because of lack of application-developer oriented tooling. Why can you not have a callback assertion or database trigger that alerts or opens a ticket when a refund is not processed within a specified amount of time? Why can't you map out your payment processors' APIs and, if amenable, define a more transactional interface on top of their CRUD API to automatically rollback incomplete or partial state transitions? (Obviously, not all payment processors will expose an interface allowing you to do this in every case; but often times they do provide the fundamental pieces in-practice, just not in a way that is easy to discover or implement). Why can't you define cross-dependency static analysis guaranteeing that eg the core checkout flow continues to work before even running any integration tests? With the right tooling you could, it's just unreasonable to expect every developer working on ecommerce to get a PhD in automated theorem proving to build their own tools for that.

> tricky logic with just a bit of I/O

I actually think that IO is the #1 most important and high ROI surface to apply formal verification (and fuzzing/other related tools which are downstream of formal methods). How many ecommerce apps are secure against DOS or runtime panics from an adversarial client sending them junk data? How many write their own janky/insecure parsers against input formats or external APIs and introduce security vulnerabilities there? I would hazard a guess that most 5+ dev webapps are guilty of basic IO sins that formal verification tools could identify in short time and also prevent from being introduced if they were added to the core development process.

The approach I'm taking is to use codegen to automatically convert OpenAPI specs and grpc service definitions (and in some cases actually just methods and http handlers themselves), and wire-format data, and application-level data structures into formalized representations that I can use downstream with autofuzzing/trace/black-box integration testing/etc tools. There are certain things that only make sense to do with AI, that are very hip and envogue, eg black-box or API-surface-informed adversarial integration testing. But you can actually much more cheaply just use AI to set up deterministic tests like this once; the problem up until now is the lack of good end-user tooling and support for those tools, which are hard to write and test especially in real-world applications that don't conform to the specific industries/academic niches that formal verification are already adopted within. That's getting solved too.