▲ 378 points
back
126 comments
I used to do proof of correctness work, decades ago.[1] We had more proof automation than many of the later systems. The easy stuff was solved by the first SAT solver, the Oppen-Nelson simplifier. The harder stuff used the Boyer-Moore prover, which uses heuristics and previous lemmas to guide the theorem prover. The Boyer-Moore prover had to be helped along by suggesting lemmas, which it would try to prove and which would then be used for later proofs. That was the tough human job.
Later systems seemed to have less automation. What tended to go wrong with formal methods was that the people doing them were too into the formalism. I was working on this for a commercial project that wanted bug-free code, not as an academic. The academic projects tended to get too clever. They had the mathematician's bias of wanting a terse notation and not much case analysis. That's not a good solution. You want lots of automated grinding and don't want to need much insight. The clever people kept inventing new logics - modal logic, temporal logic, etc, - to avoid verbosity in paper and pencil proof work. That wasn't really all that helpful. The basic truth of this business is that most of the theorems are rather banal.
As the Jane Street people point out, there's a big advantage in having control of the language. You want the verification statements integrated into the programming language. In many systems, they're embedded in comments, in a different syntax than the programming language, or even in completely separate files. This adds unnecessary work. It's good to see them pushing this forward.
We were doing this too early, over 40 years ago. It took about 45 minutes of compute back then to build up number theory from a cold start with the Boyer-Moore prover. Now it takes less than a second.
[1] https://archive.org/details/manualzilla-id-5928072/page/n3/m...
I've worked in formal methods for quite a long time, and I disagree a bit with your statement that new logics are not helpful. Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way. Logic is to computer science and software engineering what calculus is to physics and mechanical or civil engineering [1, 2]. Things like LTL or, more recently, separation logic, have been incredible breakthroughs.
TLA+, which has gained quite a lot of popularity, is a testament to that. Model checking is eminently practical. The exciting thing now is that heavier formal methods, in particular theorem proving, might become cheap enough to use in regular systems software. Writing formal specifications for functions and getting them synthesized and proven correct by some SAT/SMT, theorem prover & LLM hybrid may become the norm in the not-too-distant future.
[1] On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf
[2] From Philosophical to Industrial Logics. https://www.cs.rice.edu/~vardi/papers/icla09.pdf
Human interpretebility and human construction is going to be really important for formal specifications.
My fear is that we will get inscrutable maths that will be guarded by tiny coteries of devoties. The different inscrutable notations will be mutually incompatible, understanding one will not really help with the others. Most people will simply write english statements that cannot be verified properly.
Worse even, people will get machines to formalise their statements, and will not understand the formalism or the proofs, but will take part in the theatre of verification and act shocked when everything explodes.
Have you looked at ADA Spark?
If you have does it match your intuition of how things should be done?
I am slowly working on something where I hope to integrate such a capability for the things that type systems can't handle quickly.
So I would be interested in perspectives of people who have been down this route before.
Love this. I've shifted in the past few months to using highly expressive types in Scala 3 to have types carry more and more compile-time proofs (without macros, though a couple are warranted).
Not only does it help with agentic test "sprawl", it seems to prevent agents from falling into lower-quality modes of operation. One of the more annoying things I've been preventing is what I call "noun accretion", where agents try and make a new monomorphic type for everything, instead of clearly genericizing when sensible.
My bet is on formal-method-shaped tooling (including languages with strong type systems) to accelerate decent-quality agentic coding.
When I say "highly expressive types", I mean techniques I'd likely not want to ship in a typical codebase, unless the team was already on the typelevel programming bandwagon (i.e. having HKT and type functions being basic blocks already, not weird). Agents are better at "math" than basically most devs (even category-theory-pilled ones), at least in terms of knowledge. Better yet, they are decent at pedagogy, especially when considering they have "infinite" patience for dialogue.
In a more personal setting, I've had Codex Lean-ify a couple of my hobby proofs, it was extremely easy. Note: not saying it did this 100% "correctly" (gotta learn more Lean 4 to check more thoroughly), but it also seems to check for classic proof gotchas by default. Very excited for the future of formal methods.
In other words, because GEN AI a lot of code, the idea is to shift human value toward verification. Sometimes I think about what programming really is. In fact, learning programming itself is a huge challenge for a non English speaker like me. I have to rely on machine translation to understand English documents that have no translation. The materials in my language are about 5 to 6 years behind.
Now, since it's impossible to code review the tens of thousands of lines of code that AI produces, I see discussions about establishing an absolute rule like mathematical proofs. Reading this reminds me of Rust's borrow checker. In fact, after writing in Rust a few times, it often leads to bad practices where people use tricks to avoid the borrow checker.
Actually, when mathematical rigor goes too far, humans tend to find ways around it. An undereducated programmer like me is especially prone to that.
Looking back at this kind of attempt, it will probably result in writing code only for specific formalized answers. If it becomes that standardized, I'm not sure it will be able to respond to human needs.
I think these defensive programming attempts are fine, but I want to do offensive programming (I coined that term). You take risks, but you fix things quickly and ship. Believing that over time, it will become good enough. Of course, for established industries where accuracy matters and the scope of work is well defined, like Jane Street, the approach in this article is correct. In other words, because there is enough data to adequately model the market's demands
But for social losers like me trying to make money, constantly moving from place to place looking for gold mines, these kinds of methodologies seem like a luxury.Established businesses with mature modeling need highly educated and specialized personnel to continuously optimize. But I know that realistically, I can't keep up with that demand. So I look for places where modeling is unstructured, but I'm not sure if I can use this approach even then.
> I want to do offensive programming (I coined that term). You take risks, but you fix things quickly and ship.
Nice, I like the term too. But the paradigm is absolutely status quo in the industry. The thing is: with Gen AI the cost of "defensive programming" has gone way down, while the cost of (human) verification has gone way up. On the other hand, formal methods make verification cheap but come with massive implementation overhead (writing specs, types, proofs, and generally bending the implementation into a rigid framework). But Gen AI can automate all that laborious work. It's a match made in heaven.
You have to see it from janestreet's perspective. They're an HFT and trading high volume (millions if not 10's of millions) of stock & instruments. There is no "fix". By the time you understand what's wrong you've lost billions.
So yeah - offensive may work in non-critical areas.
Fwiw - you already use defensive everywhere. Python, Java, etc. come with garbage collectors. It's verified that the code is executing your intent.
I was wondering when we would start seeing formal verification. It makes sense that we would go from worrying about implementation details to a scientific/mathematical description of the problems.
Your ideas about Formal Methods are not clear nor quite correct.
Read first the paper On Formal Methods Thinking in Computer Science Education to understand the different levels of practice available. Here is a previous comment of mine which explains and links to the paper - https://news.ycombinator.com/item?id=46298961
Carroll Morgan just published his Formal Methods, Informally: How to Write Programs That Work which teaches you how to think in a formal method manner before you start using the heavyweight tools - https://www.cambridge.org/highereducation/books/formal-metho...
Also read Understanding Formal Methods by Jean-Francois Monin to get an overview of some of the tools and the concepts/mathematics embodied in those tools.
With just the basic ideas from the above viz. Set Theory, Predicate Calculus, learning to think of a Program as a trajectory through a state space, you can start enforcing the trajectory using simple asserts(i.e. predicates) for preconditions/postconditions/invariants. Now because of Curry-Howard Isomorphism (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...) you can treat "propositions/formulae as types" and thus exploit the type system itself as constraints enforcing the above trajectory.
Once the above is grokked, you can move on to more complex logics (eg. FOL/HOL/Temporal/Separation etc.) and learn about tools/methodologies which implement them (eg. Alloy/B-Method/TLA+ etc.).
Finally, with AI tools, the threshold for the practice of formal methods has dramatically come down. This enables one to do Formal Specification and Verification with guaranteed traceability for AI-generated code which IMO is a necessity.
>Now, since it's impossible to code review the tens of thousands of lines of code that AI produces
I would simply not ask the AI to write me more code until I'm satisfied with the code it's already written! But it is true there's more of an opportunity to let the thing rip if you can give the harness the ability to meaningfully verify its own work.
> these kinds of methodologies seem like a luxury
Absolutely. The article acknowledges this. Jane Street is pretty uniquely equipped to benefit from this.
> I have to rely on machine translation to understand English documents that have no translation. The materials in my language are about 5 to 6 years behind.
Pretty much off topic, but I strongly recommend you learn English. It takes a little bit of effort, but getting rid of that constant translation overhead will be an enormous boost for you.
I don't understand the point of your comment here. Yes of course JaneStreet published that since its relevant to them. Yes, it doesn't generally apply to all programming. How is you being a "social loser" or not following these practices in your career relevant to this?
I've been playing with related ideas recently, and can talk about them at length... but one thing that's surprised me is just how effective frontier models (ChatGPT-5.5 in particular) are at completing certain manual proofs in the Roqc (né Coq) proof assistant. The proofs aren't always pretty, but ChatGPT can often prove something in minutes and 10 - 100 iterations that would take me, a human who has limited but non-zero proof assistant experience but significant domain experience in the lemmas being proven, much much longer.
The reason I think this is relevant and interesting in the context of the (short) article is because it challenges basic assumptions about how certain formal method tooling works. Frama-C, Ada/SPARK, etc are focused on generating proof obligations that can be automatically discharged by CVC5, Z3, etc; with a relatively painful fallback of manually proving the obligation in Rocq. The most common workflow seems to be to discover that an obligation is "hard" (not automatically discharged), and to restructure the set of visible lemmas and assertions at the obligation generation point in the code to try to make it "easy"; or even restructuring the code to try to make it easy. Which, in a world where Roqc proofs are doubly expensive (first because they're a challenge for a human to write; second because they tend to require quite a bit of maintenance churn as the code and proof around them evolves), makes sense. But if Roqc proofs are "automatically discharged with AI in the loop", this cost delta goes away -- and it becomes possible to think about writing proofs the same we (usually) write code, with human readability and clarity as the first goal, and [compiler|prover] optimization a distant second.
Which I find quite exciting, although I haven't fully digested the implications yet.
How often will AI look at something that can't be proven because you change requirements and decide to change the code and your requirements to make the proof easier though? I haven't played with proofs at all, but I do know that occasionally when I say, this test failed after making a change, AI will just change the test instead of making the code pass both the old test and the new test which is most often my intent.
This mirrors my own experience, except I went with Lean. It was more relevant to the features I wanted to build.
Exciting times ahead.
> how effective frontier models (ChatGPT-5.5 in particular) are at completing certain manual proofs in the Roqc (né Coq) proof assistant. The proofs aren't always pretty, but ChatGPT can often prove something in minutes and 10 - 100 iterations that would take me, a human who has limited but non-zero proof assistant experience but significant domain experience in the lemmas being proven, much much longer.
... How do you know that the proofs are themselves correct?
Whenever I read about formal specs it always seems to me like “write the same tests just in a different way”, or worse, “write the same implementation but in a different way”.
I guess doing things twice can help catch errors, but I fail to see what’s so special about formal specs if they can suffer from the exact same bugs as the tests/implementation.
I guess the root of the problem is if you want to formally prove that a program does something, you have to be very specific (heh) about what that something is, at which point you are basically just writing tests/implementation all over again.
I have been looking into this on and off for years now, and I keep feeling like I’m missing something, but I don’t know what it is.
Can anyone enlighten me?
There's a famous quote from Dijkstra: "Program testing can be used to show the presence of bugs, but never to show their absence." The flaw of testing is that it can only test the behaviors that you think might be problematic. To actually reach into the category of proactively fixing behaviors that you didn't know could go wrong, you have to reach for more exotic tools in the toolkit. Fuzz testing is a start down this path; formal verification is a different start down this path.
Obviously, the quality of these sorts of tools is dependent on your ability to write a formal model that is comprehensive in allowing behavior you want to be acceptable and disallowing behavior you want to be unacceptable, and we're still surprisingly far from that in many fields.
> Whenever I read about formal specs it always seems to me like “write the same tests just in a different way”, or worse, “write the same implementation but in a different way”. [...] Can anyone enlighten me?
A big difference is that formal methods allow you to use the "for all" quantifier.
For example, you might write a unit test that says "foo('abc') returns a string with no trailing whitespace".
But with formal methods, you can prove that "for any input x, foo(x) returns a string with no trailing whitespace".
This is a trivial example, but you could imagine something more complicated, such as "for any program P, compile(P) has the same behavior as P".
Of course, you have to define what "has the same behavior as" means!
I don’t write software, but in asic and fpga design, formal method specifications enable the use of things like SAT solvers to determine if the underlying test article meets the specification.
You specify properties of the design and the tooling tests the design in a variety of ways to see if it can violate those properties.
Let’s say you have a system that controls turn signals. You can specify properties that say things like lanes that cross each other can’t both have a green light at the same time or even within some period of time of each other.
The tooling can exhaustively check the design for this and surface code traces that violate it.
The powerful difference is between specific testing and exhaustive proving. If you fail to think of a test for an edge case, whoops. If you have a good model, you can know that it exists—and fix it—before you ship.
This is particularly valuable IMO in concurrent/distributed/multi-threaded situations where race-conditions and deadlocks are extremely hard to test and reason about. "Can A, B, C happen in the order 'A, C, B'" types of things.
I have a rough hypothesis that maturity in this space looks something like:
1) LLMs will allow much faster learning and usage of formal methods, even if initially just for "do it a second time" post-hoc verification
2) From there you move towards automation of LLM-checking "hey, the implementation code changed, does it look like it broke the model" - though this is still not deterministic, but it's likely a lot better than a human review requirement of something that only changed infrequently would've been
3) And then the real jump will be taking tooling for "write just the formal spec, let the implementation get generated" to the next level. There's various mostly-not-fully-baked-for-what-most-companies-would-want projects already out there for codegen like this, what if the LLM tools can accelerate the year-or-two of manual work it would take to make one of them fit your needs?
It's more than just "write the same tests just in a different way", because each test is largely independent, or grows to unmanageably large, and you have to do the work of figuring out the completeness of your test suite by e.g. branch coverage or other relatively crude overlap methods.
Statically proven type systems let you do this in a way that each contributing piece is checked in advance against all the other pieces, guaranteeing not just "this test passes" but, in combination, "all these tests create a reasonable, coherent whole", and it disallows incoherent models from being implemented in the code. An example of this is like Rust's match, which requires complete coverage of all the possible branches, but writ large across an entire codebase.
You're right that it does nothing for you if you make a fundamental logic or theory error, it can't catch that kind of error, but you'd be surprised how much more robust it is than "merely" e.g. Haskell's type system + ad hoc functional testing + property testing - which I would consider a quite strong system overall, but formally proven e.g. cryptography is a much higher bar.
Lamport phrases this as "Thinking doesn't guarantee we will be right; not thinking guarantees we will be wrong" - specifications are for reasoning about systems in the deepest sense
The book "Program = Proof" by Samuel Mimram starts with a formula which is true for all n below
n = 15 341 178 777 673 149 429 167 740 440 969 249 338 310 889
I don't think you can catch it with any test suite.
That can definitely be a problem, and I have definitely written formal specs (for hardware in SVA) where I'm like "I'm just implementing this again". And actually that's a totally valid formal verification task to do - formal equivalence checking of an implementation against a model (which is just another implementation). I can feel (and sometimes is) tautological.
However you usually try to not do that. If possible (and it usually is possible) your formal spec will be either:
1. Another implementation, but a much simpler one. For example you can formally verify the equivalence of a pipelined dual issue CPU, with a combinatorial single cycle model.
2. More general properties that much be true about the implemention, rather than exactly what the implementation must be. The classic example is compression: decompress(compress(x)) == x.
The same with unit tests, they're best suited for problems where the specification is much simpler than the implementation. A sorting algorithm can be long and complicated, but a unit test just needs to present unordered input and assert that the output matches ordered output. A sorting algorithm is also well suited for formal verification.
If you're rewriting the implementation, I think it's probably not a good use for unit tests or formal verification.
As another commenter said, unlike unit tests which cover a specific case, and where you need multiple tests for edge cases and both positive and negative results, formal verification will cover all cases.
For trivial functions they can be. Function: isPrime. Impl: loop to sqrt(n) and check divisibility. Spec: returns true if nothing divides. Impl: return true at the end if we didn't return false.
It's not exactly the same because your spec says nothing divides, not just up to sqrt(n). It's definitely not a test if you do it right.
See previous kleppmann post https://martin.kleppmann.com/2025/12/08/ai-formal-verificati..., and yes, obviously anything that you can put in the typesystem or the linter, you should weigh doing so.
Hopefully we get more ergonomic ways to do this? Like of the tools listed in the post, dafny + iris are the closest to being industrial I think. And amzn S3 has a history of TLA use in-house I think. But we probably haven't seen the typescript in this space yet, a zero cost abstraction that drops into existing tools, and people genuinely prefer it to the old way.
(And custom linters are also still pretty bad to write. Like golangci-lint is a painful codebase, haven't tried semgrep but the rules engine seemed intimidating. I've yet to use an AST API that I liked)
As usual, this paean to deductive reasoning (“formal methods”) leaves out its fundamental limit: how closely do the postulates and definitions fit the domain they purport to map? (“In theory, there is no difference between theory and practice. In practice ...”) My guess is that Jane Street maintains large code bodies where the mapping is 1:1, because the purpose of the code is to implement a deterministic algorithm. Many other coders work in such areas. But millions of us don’t: most UIs, most exploratory work, etc.
There is a movement parallel to formal methods to define acceptance criteria at high resolution but not logico-mathematically, which at least grapples with the mapping problem but can’t resolve it where the map isn’t the territory, which is most places. Has Google’s results page, with its extremely evolved internal optimization frameworks really hit an optimum? Could that prototype you whipped up to capture a hazy idea have better illustrated it? These questions are best answered by looking outside the system to what the system serves.
I caught the religion on using types in conjunction with LLMs about eighteen months ago, but I only really got serious about `lean4` like six to eight months ago and now I wouldn't even consider using AI assist in software work with a `CIC` proof substrate that has practical C/C++ (and therefore, everything) FFI.
We've banned everything from JSON to Python, rewritten `nix` to have a compiler, and almost everything we write is not only property tested and multiply fuzzed to within an inch of it's life, but we have proofs in `lean4` that at a minimum drive property tests via `.olean` linkage, and when we have the bandwidth we prove exhaustiveness over the domain and property test that.
We skip the whole C++/Rust thing because all of the fast stuff is generated from `lean4` and so it doesn't really matter (C++ has advantages when bugs in it are actually bugs in `lean4` code, but you could go either way).
This is a big departure, and I certainly don't blame anyone who is skeptical: "ban JSON and Python wtf?!?!", but we've done millions of lines (checked) of this stuff and AI + formal systems is a dramatically bigger leap than no AI -> AI and Python. The latter in our experience is not monotone in progress, the former is almost always monotone in progress.
And you can do wild shit, this is a formal proof of the polyhedral tensor calculus that is modeled by things like ISL and CuTe, and using that we can get swizzling and tiling using `mdspan` in C++23 on device and prove it's right (up to some L'Hopital arugment about the coverage which this example doesn't demonstrate well: https://github.com/b7r6/mdspan-cute
That in turn, well, it goes real fast. On the first try.
Relevant keynote I wrote about
Formal methods won, now what? https://muratbuffalo.blogspot.com/2026/04/bugbash26-keynote....
As someone with a bit of interest in programming languages (design and implementation) this was really interesting to me:
> For most people who work on programming languages, the easy part is coming up with new and better ideas about how to make programming better. The hard part is convincing anyone to actually use those ideas for real work.
Totally agree, there's only so much strangeness you can introduce in a new language[1] regardless of benefit.
But AI agents should not feel much resistance to radically new ideas in PL design. I've been thinking for a while now about how PL design will evolve post agentic AI. I think it will be very interesting to see what new ideas we can come up with to improve programming languages when we worry much less about adoption.
[1] https://steveklabnik.com/writing/the-language-strangeness-bu...
We are working toward applying formal methods from the application security testing side, but I believe the same kind of approach can be applied to business logic verification as well. For that, we are using the taint analysis technique — a fairly well-established formal methods approach, but still not widely applied in the field because of the complexity of dataflows in real codebases.
Scaling formal methods beyond AST pattern matching and some simple type checking turns out to be a really hard task! It took years of research and development to reach the point where taint analysis enables us to trace interprocedural dataflows in real codebases in minutes and find deeply hidden vulnerabilities.
If this sounds interesting to you, take a look at our project: https://github.com/seqra/opentaint
seL4 despite being formally verified contained gnarly bugs, like [1]. Thus, it's not a silver bullet as some people think. Yes, it improves the quality, but only one of the aspects of hardening software, like ASAN, SAST, fuzzing, strict languages, and so on.
I nearly adopted OCaml for my current math research, in no small part because of Jane Street contributions. I instead chose Lean 4, as LLMs became able to help code in Lean. I give up a factor of two in performance (a gap likely to close) for what reads to me as the clearest expression of each algorithm. Lean is a beautiful language that makes OCaml read like Old English.
Lean is designed to be optionally verified; proof is its primary (but not only) application. It seems an impedance mismatch for Jane Street to explore this direction without also migrating to Lean 4.
I wonder how formal methods can help us move faster with GenAI.
Is it that they can help write formulas faster? That they can help ensure formulas match the system they're modeling faster? If the problem you think formal methods will help with is sloppy code, isn't the verification code going to be sloppy as well, unless some (not sloppy) intelligence carefully confirms that the specification matches the target system, which was the labor that previously made formal methods too expensive? I guess I don't understand how the argument works if code was previously less sloppy and verification was too expensive, and now code is more sloppy, and there's more of it, but somehow the sloppy intelligence will make verification move fast enough to make it worthwhile.
Unless we have some non-sloppy intelligence that's less of a bottleneck on verification than humans, how are we in a better place?
Maybe it's that investing that huge amount of labor of verification by human experts is now worth it because so much code will be produced that uses the verification systems that the investment will now pay off. But that requires creating pretty general verification systems, such as type system verification or something (which is what they seem to be aimed at), rather than individually verifying software systems like the micro-kernel example.
In other words, maybe the play is to invest in reusable verification systems that can be run tons of times on new code and systems. If so, it's surprising that this wasn't always the strategy.
I was playing around with stuff trying to get Claude produce a JavaCard VM with the idea that the VM was hand written from the spec with a separate, independently produced, spec file used to generate tests for ESBMC to verify so an identical bug would have to exist in both to make it through. Worked out pretty well, found a few bugs in both projects, but my poor laptop can't handle the full 32-bit space so that part never got the full verification -- 16-bit, rock solid though.
Then I really got serious about the yak shaving and, well, am probably in need of an intervention as I don't get Claude to write a VM but to make the tools to generate a VM from an assortment of DSL and that has snowballed a bit as I really liked shaving yaks before the daffy robot revolution.
--edit--
Almost forgot, I tried that with the little less dodgy banned Claude and the wasm standard it wrote a python script to parse the spec pdf, the official bytecode implementation in OCaml (or whatever) and generate a TOML file (Claude loves the TOML) to generate the type headers and for cross-referencing in the other tools. Was so impressed I just let it go on its merry way and it did the deed.
He mentions the seL4 microkernel. The specification is written in Isabelle, and it's relatively complex: PDF https://sel4.systems/Info/Docs/seL4-spec.pdf
The bottleneck seems to be that clearly it's critical to be certain about the spec.
Maybe not for kernels, but I can see use for cryptographic algorithms, etc?
I think it's a good time to learn Lean. It positions itself as a proof assistant that's also good at practical programming. I'm not sure how mature the ecosystem is for the latter.
Sounds like Jane Street would be interested in the Lean framework I've been working on for formally verified frontends. https://github.com/JacobAsmuth/qed
I am already seeing the uptake on Spec-Driven Development as the Rational Unified Process revenge.
I have been testing formal verification methods with multiple products. It will be great to also understand more about what’s tried and how it was done. For example attempting to verify the spec is what I have been trying to implement.
Quis custodiet ipsos custodes?
Interesting read. Formal methods seem to matter most when the architectural complexity grows faster than human intuition can track.
Formal methods is like a plan. Everyone has one until they are punched in the face (real world requirements and trust boundaries).
I’ve had huge success with TDD and nothing more formal than that; test frameworks are great for verifying “business correctness”. But they can also verify other aspects - eg. asserting that 3 queries ran instead of 103 for a request, to prove absence of N+1 queries.
Really any technique that lets the agent create its own verification is ideal, as it makes verification scale.
I am not a language nerd but I keep on experimenting in my own ways to use the type system to generate code that is more reliable.
I build a coding agent specifically for small models, which makes everything harder. I started this chat with Claude to build the next step: https://claude.ai/share/4264e5f6-b334-426c-afe4-904d233ef946 - how can I go from PRD to a typed representation of the business logic.
The I started building as per https://github.com/brainless/nocodo/blob/feature/praxis_agen.... The praxis crate: https://github.com/brainless/nocodo/tree/feature/praxis_agen... and a sample Todo app: https://github.com/brainless/nocodo_example_todo_app
Generating unit tests for the library functions of any project would be done via a separate agent than the one coding the functions. And then use tree-sitter to statically check code to PRD (provenance graph).
Again, not a language nerd, just enjoying chasing a goal.