13 ms·

This doesn't make too much sense to me. * This isn't a language, it's some tooling to map specs to code and re-generate * Models aren't deterministic - every

This doesn't make too much sense to me. * This isn't a language, it's some tooling to map specs to code and re-generate * Models aren't deterministic - every time you would try to re-apply you'd likely get different output (without feeding the current code into the re-apply and let it just recommend changes) * Models are evolving rapidly, this months flavour of Codex/Sonnet/etc would very likely generate different code from last months * Text specifications are always under-specified, lossy and tend to gloss over a huge amount of details that the code has to make concrete - this is fine in a small example, but in a larger code base? * Every non-trivial codebase would be made up of of hundreds of specs that interact and influence each other - very hard (and context - heavy) to read all specs that impact functionality and keep it coherent I do think there are opportunities in this space, but what I'd like to see is: * write text specifications * model transforms text into a *formal* specification * then the formal spec is translated into code which can be verified against the spec 2 and three could be merged into one if there were practical/popular languages that also support verification, in the vain of ADA/Spark. But you can also get there by generating tests from the formal specification that validate the implementation.

davedx 6mo ago
My process has organically evolved towards something similar but less strictly defined: - I bootstrap AGENTS.md with my basic way of working and occasionally one or two project specific pieces - I then write a DESIGN.md. How detailed or well specified it is varies from project to project: the other day I wrote a very complete DESIGN.md for a time tracking, invoice management and accounting system I wanted for my freelance biz. Because it was quite complete, the agent almost one-shot the whole thing - I often also write a TECHNICAL-SPEC.md of some kind. Again how detailed varies. - Finally I link to those two from the AGENTS. I also usually put in AGENTS that the agent should maintain the docs and keep them in sync with newer decisions I make along the way. This system works well for me, but it's still very ad hoc and definitely doesn't follow any kind of formally defined spec standard. And I don't think it should, really? IMO, technically strict specs should be in your automated tests not your design docs.
- the_duke 6mo ago
  I think many have adopted "spec driven development" in the way you describe. I found it works very well in once-off scenarios, but the specs often drift from the implementation. Even if you let the model update the spec at the end, the next few work items will make parts of it obsolete. Maybe that's exactly the goal that "codespeak" is trying to solve, but I'm skeptical this will work well without more formal specifications in the mix.
  - intrasight 6mo ago
    > specs often drift from the implementation > Maybe that's exactly the goal that "codespeak" is trying to solve Yes and yes. I think it's an important direction in software engineering. It's something that people were trying to do a couple decades ago but agentic implementation of the spec makes it much more practical.
  - dworks 6mo ago
    You need to lock the specs and implementation plan and verify the implementation about the previous phase docs. https://github.com/doubleuuser/rlm-workflow https://github.com/doubleuuser/rlm-workflow
- jbonatakis 6mo ago
  I have been building this in my free time and it might be relevant to you: https://github.com/jbonatakis/blackbird https://github.com/jbonatakis/blackbird I have the same basic workflow as you outlined, then I feed the docs into blackbird, which generates a structured plan with task and sub tasks. Then you can have it execute tasks in dependency order, with options to pause for review after each task or an automated review when all child task for a given parents are complete. It’s definitely still got some rough edges but it has been working pretty well for me.
- rebolek 6mo ago
  AGENTS.md is nice but I still need to remind models that it exists and they should read it and not reinvent the wheel every time.
pessimizer 6mo ago
I think your objections miss the point. My informal specs to a program are user-focused. I want to dictate what benefits the program will give to the person who is using it, which may include requirements for a transport layer, a philosophy of user interaction, or any number of things. When I know what I want out of a program, I go through the agony of translating that into a spec with database schemas, menu options, specific encryption schemes, etc., then finally I turn that into a formal spec within which whether I use an underscore or a dash somewhere becomes a thing that has to be consistent throughout the document. You're telling me that I should be doing the agonizing parts in order for the LLM to do the routine part (transforming a description of a program into a formal description of a program.) Your list of things that "make no sense" are exactly the things that I want the LLMs to do. I want to be able to run the same spec again and see the LLM add a feature that I never expected (and wasn't in the last version run from the same spec) or modify tactics to accomplish user goals based on changes in technology or availability of new standards/vendors. I want to see specs that move away from describing the specific functionality of programs altogether, and more into describing a usefulness or the convenience of a program that doesn't exist. I want to be able to feed the LLM requirements of what I want a program to be able to accomplish, and let the LLM research and implement the how. I only want to have to describe constraints i.e. it must enable me to be able to do A, B, and C, it must prevent X,Y, and Z; I want it to feel free to solve those constraints in the way it sees fit; and when I find myself unsatisfied with the output, I'll deliver it more constraints and ask it to regenerate.
- darkwater 6mo ago
  > I want to be able to run the same spec again and see the LLM add a feature that I never expected (and wasn't in the last version run from the same spec) or modify tactics to accomplish user goals based on changes in technology or availability of new standards/vendors. Be careful what you wish for. This sounds great in theory but in practice it will probably mean a migration path for the users (UX changes, small details changed, cost dynamics and a large etc.)
- jbritton 6mo ago
  I tried this recently with what I thought was a simple layout, but probably uncommon for CSS. It took an extremely long back and forth to nail it down. It seemingly had no understanding how to achieve what I wanted. A couple sentences would have been clear to a person. Sometimes LLMs are fantastic and sometimes they are brain dead.
hkonte 6mo ago
[dead]
onion2k 6mo ago
Models aren't deterministic - every time you would try to re-apply you'd likely get different output (without feeding the current code into the re-apply and let it just recommend changes) If the result is always provably correct it doesn't matter whether or not it's different at the code level. People interested in systems like this believe that the outcome of what the code does is infinity more important than the code itself.
- SpaceNoodled 6mo ago
  That's a huge "if."
  - gentooflux 6mo ago
    I usually invert those to reduce nesting
- jrm4 6mo ago
  I would be very comfortable with - re-run 100 times with different seeds. If the outcome is the same every time, you're reliably good to go.
  - SpaceNoodled 6mo ago
    Even when it's wrong each time?
    - onion2k 6mo ago
      If it's wrong then it's not provably correct (for any value of 'proof'). How you define your proof is up to you. It might be a simple test, or an exhaustive suite of tests, or a formal proof. It doesn't matter. If the output of the code is correct by your definition, then it doesn't matter what the underlying code actually is.
- Copyrightest 6mo ago
  [dead]
fnord77 6mo ago
[delete]
- dist-epoch 6mo ago
  Software products specifications are written in real language, not in first order logic.
- koolala 6mo ago
  It isn't a formal language, look at the goose example: https://codespeak.dev/blog/greenfield-project-tutorial-20260209 https://codespeak.dev/blog/greenfield-project-tutorial-20260... It is a formal "way" aka like using json or xml like tons of people are already doing.
DrJokepu 6mo ago
> Models aren't deterministic Is that really true? I haven’t tried to do my own inference since the first Llama models came out years ago, but I am pretty sure it was deterministic: if you fixed the seed and the input was the same, the output of the inference was always exactly the same.
- bigwheels 6mo ago
  LLMs are not deterministic: 1.) There is typically a temperature setting (even when not exposed, most major providers have stopped exposing it [esp in the TUIs]). 2.) Then, even with the temperature set to 0, it will be almost deterministic but you'll still observe small variations due to the limited precision of float numbers. Edit: thanks for the corrections
  - comboy 6mo ago
    Limited precision of float numbers is deterministic. But there's whole parallelism and how things are wired together, your generation may end up on a different hardware etc. And models I work with (claude,gemini etc) have the temperature parameter when you are using API.
  - dwohnitmok 6mo ago
    > but you'll still observe small variations due to the limited precision of float numbers No. Floating number arithmetic is deterministic. You don't get different answers for the same operations on the same machine just because of limited precision. There are reasons why it can be difficult to make sure that floating point operations agree across machines, but that is more of a (very annoying and difficult to make consistent) configuration thing than determinism. (In general it is mildly frustrating to me to see software developers treat floating point as some sort of magic and ascribe all sorts of non-deterministic qualities to it. Yes floating point configuration for consistent results across machines can be absurdly annoying and nigh-impossible if you use transcendental functions and different binaries. No this does not mean if your program is giving different results for the same input on the same machine that this is a floating point issue). In theory parallel execution combined with non-associativity can cause LLM inference to be non-deterministic. In practice that is not the case. LLM forward passes rarely use non-deterministic kernels (and these are usually explicitly marked as such e.g. in PyTorch). You may be thinking of non-determinism caused by batching where different batch sizes can cause variations in output. This is not strictly speaking non-determinism from the perspective of the LLM, but is effectively non-determinism from the perspective of the end user, because generally the end user has no control over how a request is slotted into a batch.
dist-epoch 6mo ago
> Models aren't deterministic - every time you would try to re-apply you'd likely get different output So like when you give the same spec to 2 different programmers.
- kennywinker 6mo ago
  Except each time you compile your spec you’re re-writing it from scratch with a different programmer.
- rco8786 6mo ago
  Yes, if you had each programmer rewrite the code from scratch each time you updated the spec.
  - orbital-decay 6mo ago
    In reality you give the same programmer an update to the existing spec, and they change the code to implement the difference. Which is exactly what the thing in OP is doing, and exactly what should be done. There's simply no reason to regenerate the result. The entire thing about determinism is a red herring, because 1) it's not determinism but prompt instability, and 2) prompt instability doesn't matter because of the above. Intelligence (both human and machine) is not a formal domain, your inputs lack formal syntax, and that's fine. For some reason this basic concept creates endless confusion everywhere.
    - xigoi 6mo ago
      > your inputs lack formal syntax, and that's fine It’s not fine. I program using formal syntax precisely because I want the computer to do exactly what I tell it to.
      - orbital-decay 6mo ago
        Then program, instead of telling someone else (humans, LLMs) to do it.
rco8786 6mo ago
How is your 2 step process not susceptible to all the exact same pitfalls you listed above?
deleted 6mo ago
[deleted]
pron 6mo ago
If what you're after is determinism, then your solution doesn't offer it. Both the formal specification and the code generated from it would be different each time. Formal specifications are useful when they're succinct, which is possible when they specify at a higher level of abstraction than code, which admits many different implemementations.
- vidarh 6mo ago
  The point would presumably be to formalise it, then verify that the formal version matches what you actually meant. At which point you can't/shouldn't regenerate it, but you can request changes (which you'd need to verify and approve).
  - pron 6mo ago
    But the code produced from the formal spec would still be nondeterministic. And I believe CodeSpeak doesn't wish to regenerate the entire program with each spec change, but apply code changes based on the changes to the spec. Maybe there could be other benefits to formalisation in this case, but determinism isn't one of them.
    - vidarh 6mo ago
      It doesn't matter if the code is different if the spec is formal enough to validate the software against it. I have no idea about codespeak - I was responding to the comments above, not about codespeak.
      - pron 6mo ago
        Validating programs against a formal spec is very, very hard for foundational computational complexity reasons. There's a reason why the largest programs whose code was fully verified against a formal spec, and at an enormous cost, were ~10KLOC. If you want to do it using proofs, then lines of proof outnumber lines of code 10-1000 to 1, and the work is far harder than for proofs in mathematics (that are typically much shorter). There are less absolute ways of checking spec conformance at some useful level of confidence, and they can be worthwhile, but they require expertise and care (I'm very much in favour of using them, but the thought that AI can "just" prove conformance to a formal spec ignores the computational complexity results in that field).
jnpnj 6mo ago
Maybe we're entering the non-deterministic applications too. No more mechanical predictable thing.. more like 90% regular and then weird. Slightly sarcastic but not sure this couldn't become a thing.
wenc 6mo ago
Rehashing my comment from before: I use Kiro IDE (≠ Kiro CLI) primarily as a spec generator. In my experience, it's high-quality for creating and iterating on specs. Tools like Cursor are optimized for human-driven vibing -- they have great autocomplete, etc. Kiro, by contrast, is optimized around spec, which ironically has been the most effective approach I've found for driving agents. I'd argue that Cursor, Antigravity, and similar tools are optimized for human steering, which explains their popularity, while Kiro is optimized for agent harnesses. That's also why it’s underused: it's quite opinionated, but very effective. Vibe-coding culture isn't sold on spec driven development (they think it's waterfall and summarily dismiss it -- even Yegge has this bias), so people tend to underrate it. Kiro writes specs using structured formats like EARS and INCOSE (which is the spc format used in places like Boeing for engineering reqs). It performs automated reasoning to check for consistency, then generates a design document and task list from the spec -- similar to what Beads does. I usually spend a significant amount of time pressure-testing the spec before implementing (often hours to days), and it pays off. Writing a good, consistent spec is essentially the computer equivalent of "writing as a tool of thought" in practice. Once the spec is tight, implementation tends to follow it closely. Kiro also generates property-based tests (PBTs) using Hypothesis in Python, inspired by Haskell's QuickCheck. These tests sweep the input domain and, when combined with traditional scenario-based unit tests, tend to produce code that adheres closely to the spec. I also add a small instruction "do red/green TDD" (I learned this from Simon Willison) and that one line alone improved the quality of all my tests. Kiro can technically implement the task list itself, but this is where agents come in. With the spec in hand, I use multiple headless CLI agents in tmux (e.g., Kiro CLI, Claude Code) for implementation. The results have been very good. With a solid Kiro spec and task list, agents usually implement everything end-to-end without stopping -- I haven’t found a need for Ralph loops. (agents sometimes tend to stop mid way on Claude plans, but I've never had that happen with Kiro, not sure why, maybe it's the checklist, which includes PBT tests as gates). didn't have the strongest start, but the Kiro IDE is one of the best spec generators I've used, and it integrates extremely well with agent-driven workflows.
abreslav 6mo ago
> * model transforms text into a formal specification formal specification is no different from code: it will have bugs :) There's no free lunch here: the informal-to-formal transition (be it words-to-code or words-to-formal-spec) comes through the non-deterministic models, period. If we want to use the immense power of LLMs, we need to figure out a way to make this transition good enough
dworks 6mo ago
>I do think there are opportunities in this space, but what I'd like to see is: >* write text specifications >* model transforms text into a formal specification >* then the formal spec is translated into code which can be verified against the spec This skill does just that: https://github.com/doubleuuser/rlm-workflow https://github.com/doubleuuser/rlm-workflow Each stage produces its own output artifact (analysis, implementation plan, implementation summary, etc) and takes the previous phases' outputs as input. The artifact is locked after the stage is done, so there is no drift.

davedx 6mo ago

My process has organically evolved towards something similar but less strictly defined: - I bootstrap AGENTS.md with my basic way of working and occasionally one or two project specific pieces - I then write a DESIGN.md. How detailed or well specified it is varies from project to project: the other day I wrote a very complete DESIGN.md for a time tracking, invoice management and accounting system I wanted for my freelance biz. Because it was quite complete, the agent almost one-shot the whole thing - I often also write a TECHNICAL-SPEC.md of some kind. Again how detailed varies. - Finally I link to those two from the AGENTS. I also usually put in AGENTS that the agent should maintain the docs and keep them in sync with newer decisions I make along the way. This system works well for me, but it's still very ad hoc and definitely doesn't follow any kind of formally defined spec standard. And I don't think it should, really? IMO, technically strict specs should be in your automated tests not your design docs.

the_duke 6mo ago
I think many have adopted "spec driven development" in the way you describe. I found it works very well in once-off scenarios, but the specs often drift from the implementation. Even if you let the model update the spec at the end, the next few work items will make parts of it obsolete. Maybe that's exactly the goal that "codespeak" is trying to solve, but I'm skeptical this will work well without more formal specifications in the mix.
- intrasight 6mo ago
  > specs often drift from the implementation > Maybe that's exactly the goal that "codespeak" is trying to solve Yes and yes. I think it's an important direction in software engineering. It's something that people were trying to do a couple decades ago but agentic implementation of the spec makes it much more practical.
- dworks 6mo ago
  You need to lock the specs and implementation plan and verify the implementation about the previous phase docs. https://github.com/doubleuuser/rlm-workflow https://github.com/doubleuuser/rlm-workflow
jbonatakis 6mo ago
I have been building this in my free time and it might be relevant to you: https://github.com/jbonatakis/blackbird https://github.com/jbonatakis/blackbird I have the same basic workflow as you outlined, then I feed the docs into blackbird, which generates a structured plan with task and sub tasks. Then you can have it execute tasks in dependency order, with options to pause for review after each task or an automated review when all child task for a given parents are complete. It’s definitely still got some rough edges but it has been working pretty well for me.
rebolek 6mo ago
AGENTS.md is nice but I still need to remind models that it exists and they should read it and not reinvent the wheel every time.

pessimizer 6mo ago

I think your objections miss the point. My informal specs to a program are user-focused. I want to dictate what benefits the program will give to the person who is using it, which may include requirements for a transport layer, a philosophy of user interaction, or any number of things. When I know what I want out of a program, I go through the agony of translating that into a spec with database schemas, menu options, specific encryption schemes, etc., then finally I turn that into a formal spec within which whether I use an underscore or a dash somewhere becomes a thing that has to be consistent throughout the document. You're telling me that I should be doing the agonizing parts in order for the LLM to do the routine part (transforming a description of a program into a formal description of a program.) Your list of things that "make no sense" are exactly the things that I want the LLMs to do. I want to be able to run the same spec again and see the LLM add a feature that I never expected (and wasn't in the last version run from the same spec) or modify tactics to accomplish user goals based on changes in technology or availability of new standards/vendors. I want to see specs that move away from describing the specific functionality of programs altogether, and more into describing a usefulness or the convenience of a program that doesn't exist. I want to be able to feed the LLM requirements of what I want a program to be able to accomplish, and let the LLM research and implement the how. I only want to have to describe constraints i.e. it must enable me to be able to do A, B, and C, it must prevent X,Y, and Z; I want it to feel free to solve those constraints in the way it sees fit; and when I find myself unsatisfied with the output, I'll deliver it more constraints and ask it to regenerate.

darkwater 6mo ago
> I want to be able to run the same spec again and see the LLM add a feature that I never expected (and wasn't in the last version run from the same spec) or modify tactics to accomplish user goals based on changes in technology or availability of new standards/vendors. Be careful what you wish for. This sounds great in theory but in practice it will probably mean a migration path for the users (UX changes, small details changed, cost dynamics and a large etc.)
jbritton 6mo ago
I tried this recently with what I thought was a simple layout, but probably uncommon for CSS. It took an extremely long back and forth to nail it down. It seemingly had no understanding how to achieve what I wanted. A couple sentences would have been clear to a person. Sometimes LLMs are fantastic and sometimes they are brain dead.

hkonte 6mo ago

[dead]

onion2k 6mo ago

Models aren't deterministic - every time you would try to re-apply you'd likely get different output (without feeding the current code into the re-apply and let it just recommend changes) If the result is always provably correct it doesn't matter whether or not it's different at the code level. People interested in systems like this believe that the outcome of what the code does is infinity more important than the code itself.

SpaceNoodled 6mo ago
That's a huge "if."
- gentooflux 6mo ago
  I usually invert those to reduce nesting
jrm4 6mo ago
I would be very comfortable with - re-run 100 times with different seeds. If the outcome is the same every time, you're reliably good to go.
- SpaceNoodled 6mo ago
  Even when it's wrong each time?
  - onion2k 6mo ago
    If it's wrong then it's not provably correct (for any value of 'proof'). How you define your proof is up to you. It might be a simple test, or an exhaustive suite of tests, or a formal proof. It doesn't matter. If the output of the code is correct by your definition, then it doesn't matter what the underlying code actually is.
Copyrightest 6mo ago
[dead]

fnord77 6mo ago

[delete]

dist-epoch 6mo ago
Software products specifications are written in real language, not in first order logic.
koolala 6mo ago
It isn't a formal language, look at the goose example: https://codespeak.dev/blog/greenfield-project-tutorial-20260209 https://codespeak.dev/blog/greenfield-project-tutorial-20260... It is a formal "way" aka like using json or xml like tons of people are already doing.

DrJokepu 6mo ago

> Models aren't deterministic Is that really true? I haven’t tried to do my own inference since the first Llama models came out years ago, but I am pretty sure it was deterministic: if you fixed the seed and the input was the same, the output of the inference was always exactly the same.

bigwheels 6mo ago
LLMs are not deterministic: 1.) There is typically a temperature setting (even when not exposed, most major providers have stopped exposing it [esp in the TUIs]). 2.) Then, even with the temperature set to 0, it will be almost deterministic but you'll still observe small variations due to the limited precision of float numbers. Edit: thanks for the corrections
- comboy 6mo ago
  Limited precision of float numbers is deterministic. But there's whole parallelism and how things are wired together, your generation may end up on a different hardware etc. And models I work with (claude,gemini etc) have the temperature parameter when you are using API.
- dwohnitmok 6mo ago
  > but you'll still observe small variations due to the limited precision of float numbers No. Floating number arithmetic is deterministic. You don't get different answers for the same operations on the same machine just because of limited precision. There are reasons why it can be difficult to make sure that floating point operations agree across machines, but that is more of a (very annoying and difficult to make consistent) configuration thing than determinism. (In general it is mildly frustrating to me to see software developers treat floating point as some sort of magic and ascribe all sorts of non-deterministic qualities to it. Yes floating point configuration for consistent results across machines can be absurdly annoying and nigh-impossible if you use transcendental functions and different binaries. No this does not mean if your program is giving different results for the same input on the same machine that this is a floating point issue). In theory parallel execution combined with non-associativity can cause LLM inference to be non-deterministic. In practice that is not the case. LLM forward passes rarely use non-deterministic kernels (and these are usually explicitly marked as such e.g. in PyTorch). You may be thinking of non-determinism caused by batching where different batch sizes can cause variations in output. This is not strictly speaking non-determinism from the perspective of the LLM, but is effectively non-determinism from the perspective of the end user, because generally the end user has no control over how a request is slotted into a batch.

dist-epoch 6mo ago

> Models aren't deterministic - every time you would try to re-apply you'd likely get different output So like when you give the same spec to 2 different programmers.

kennywinker 6mo ago
Except each time you compile your spec you’re re-writing it from scratch with a different programmer.
rco8786 6mo ago
Yes, if you had each programmer rewrite the code from scratch each time you updated the spec.
- orbital-decay 6mo ago
  In reality you give the same programmer an update to the existing spec, and they change the code to implement the difference. Which is exactly what the thing in OP is doing, and exactly what should be done. There's simply no reason to regenerate the result. The entire thing about determinism is a red herring, because 1) it's not determinism but prompt instability, and 2) prompt instability doesn't matter because of the above. Intelligence (both human and machine) is not a formal domain, your inputs lack formal syntax, and that's fine. For some reason this basic concept creates endless confusion everywhere.
  - xigoi 6mo ago
    > your inputs lack formal syntax, and that's fine It’s not fine. I program using formal syntax precisely because I want the computer to do exactly what I tell it to.
    - orbital-decay 6mo ago
      Then program, instead of telling someone else (humans, LLMs) to do it.

rco8786 6mo ago

How is your 2 step process not susceptible to all the exact same pitfalls you listed above?

deleted 6mo ago

[deleted]

pron 6mo ago

If what you're after is determinism, then your solution doesn't offer it. Both the formal specification and the code generated from it would be different each time. Formal specifications are useful when they're succinct, which is possible when they specify at a higher level of abstraction than code, which admits many different implemementations.

vidarh 6mo ago
The point would presumably be to formalise it, then verify that the formal version matches what you actually meant. At which point you can't/shouldn't regenerate it, but you can request changes (which you'd need to verify and approve).
- pron 6mo ago
  But the code produced from the formal spec would still be nondeterministic. And I believe CodeSpeak doesn't wish to regenerate the entire program with each spec change, but apply code changes based on the changes to the spec. Maybe there could be other benefits to formalisation in this case, but determinism isn't one of them.
  - vidarh 6mo ago
    It doesn't matter if the code is different if the spec is formal enough to validate the software against it. I have no idea about codespeak - I was responding to the comments above, not about codespeak.
    - pron 6mo ago
      Validating programs against a formal spec is very, very hard for foundational computational complexity reasons. There's a reason why the largest programs whose code was fully verified against a formal spec, and at an enormous cost, were ~10KLOC. If you want to do it using proofs, then lines of proof outnumber lines of code 10-1000 to 1, and the work is far harder than for proofs in mathematics (that are typically much shorter). There are less absolute ways of checking spec conformance at some useful level of confidence, and they can be worthwhile, but they require expertise and care (I'm very much in favour of using them, but the thought that AI can "just" prove conformance to a formal spec ignores the computational complexity results in that field).

jnpnj 6mo ago

Maybe we're entering the non-deterministic applications too. No more mechanical predictable thing.. more like 90% regular and then weird. Slightly sarcastic but not sure this couldn't become a thing.

wenc 6mo ago

Rehashing my comment from before: I use Kiro IDE (≠ Kiro CLI) primarily as a spec generator. In my experience, it's high-quality for creating and iterating on specs. Tools like Cursor are optimized for human-driven vibing -- they have great autocomplete, etc. Kiro, by contrast, is optimized around spec, which ironically has been the most effective approach I've found for driving agents. I'd argue that Cursor, Antigravity, and similar tools are optimized for human steering, which explains their popularity, while Kiro is optimized for agent harnesses. That's also why it’s underused: it's quite opinionated, but very effective. Vibe-coding culture isn't sold on spec driven development (they think it's waterfall and summarily dismiss it -- even Yegge has this bias), so people tend to underrate it. Kiro writes specs using structured formats like EARS and INCOSE (which is the spc format used in places like Boeing for engineering reqs). It performs automated reasoning to check for consistency, then generates a design document and task list from the spec -- similar to what Beads does. I usually spend a significant amount of time pressure-testing the spec before implementing (often hours to days), and it pays off. Writing a good, consistent spec is essentially the computer equivalent of "writing as a tool of thought" in practice. Once the spec is tight, implementation tends to follow it closely. Kiro also generates property-based tests (PBTs) using Hypothesis in Python, inspired by Haskell's QuickCheck. These tests sweep the input domain and, when combined with traditional scenario-based unit tests, tend to produce code that adheres closely to the spec. I also add a small instruction "do red/green TDD" (I learned this from Simon Willison) and that one line alone improved the quality of all my tests. Kiro can technically implement the task list itself, but this is where agents come in. With the spec in hand, I use multiple headless CLI agents in tmux (e.g., Kiro CLI, Claude Code) for implementation. The results have been very good. With a solid Kiro spec and task list, agents usually implement everything end-to-end without stopping -- I haven’t found a need for Ralph loops. (agents sometimes tend to stop mid way on Claude plans, but I've never had that happen with Kiro, not sure why, maybe it's the checklist, which includes PBT tests as gates). didn't have the strongest start, but the Kiro IDE is one of the best spec generators I've used, and it integrates extremely well with agent-driven workflows.

abreslav 6mo ago

> * model transforms text into a formal specification formal specification is no different from code: it will have bugs :) There's no free lunch here: the informal-to-formal transition (be it words-to-code or words-to-formal-spec) comes through the non-deterministic models, period. If we want to use the immense power of LLMs, we need to figure out a way to make this transition good enough

dworks 6mo ago

>I do think there are opportunities in this space, but what I'd like to see is: >* write text specifications >* model transforms text into a formal specification >* then the formal spec is translated into code which can be verified against the spec This skill does just that: https://github.com/doubleuuser/rlm-workflow https://github.com/doubleuuser/rlm-workflow Each stage produces its own output artifact (analysis, implementation plan, implementation summary, etc) and takes the previous phases' outputs as input. The artifact is locked after the stage is done, so there is no drift.