Systems Correctness Practices at AWS: Leveraging Formal and Semi-Formal Methods

I've noticed that the formalization of methods described by AWS parallels what we need in technical documentation. Complex systems require not just formal verification but also structured documentation following MECE principles (Mutually Exclusive, Collectively Exhaustive).

In my experience, the interfaces between components (where most errors occur) are exactly where fragmented documentation fails. I implemented a hierarchical documentation system for my team that organizes knowledge as a conceptual tree, and the accuracy of code generation with AI assistants improved notably.

Formal verification tools and structured documentation are complementary: verification ensures algorithmic correctness while MECE documentation guarantees conceptual and contextual correctness. I wonder if AWS has experimented with structured documentation systems specifically for AI, or if this remains an area to explore.

Could you explain how your "hierarchical documentation system" works? Does the tree parallel the code? Is there a particular tool that you use?

I'm interested in learning more about the benefits of MECE - I've never heard that before. In particular, it seems radically different from Divio's system [0], which presents the same information in many different ways.

0: https://docs.divio.com/documentation-system/

Is this not https://diataxis.fr/ ?

(I'm engaged somewhat in trying to get our team to write any documentation; once I've got that, I'll start trying to organize along exactly these principles)

Formalization, correctness is about models. [1]

There are formal methods where the underlying model is mathematically sound. There are semi-formal methods where the underlying model is structured but not proven to be sound.

For example, in your case ("organizes knowledge") a formal method is ologs from category theory. That method assures that the concepts and their relationship in your knowledge base are mathematically correct.

When you want to transfer that knowledge base into a documentation system you might want look for a mathematically sound model, but I'm afraid there is no such model, so what's left is a semi-formal method / a likely-correct model.

Right now I'm building such a likely-correct model for writing, contact me for more info.

[1] https://www.osequi.com/slides/formalism-correctness-cost/for...

Thank you for introducing me to ologs - they're fascinating. I'm intrigued by the distinction you make between formal methods and semi-formal approaches.

I'd love to explore how your "likely-correct model for writing" might complement the MECE-based documentation system I've been developing. Since you're building a model focused on writing correctness, perhaps there's an opportunity to collaborate?

My approach addresses the organizational structure of documentation, while your work seems to focus on ensuring correctness at the content level. Together, these could potentially create a more comprehensive solution that combines hierarchical organization with formal correctness principles.

Would you be interested in discussing further? I'm curious to learn more about your model.

The hierarchical system I've developed organizes knowledge in nested MECE categories (Mutually Exclusive, Collectively Exhaustive). Rather than paralleling code exactly, it creates a conceptual tree that represents the mental model behind the system.

For example, in an e-commerce API: - Level 1: Core domains (Products, Orders, Users) - Level 2: Sub-domains (Product variants, Order fulfillment, User authentication) - Level 3: Implementation details (Variant pricing logic, Fulfillment status transitions)

I'm currently using plain Markdown with a specific folder structure, making it friendly to version control and AI tools. The key innovation is the organization pattern rather than the tooling - ensuring each concept belongs in exactly one place (mutually exclusive) while collectively covering all needed context (collectively exhaustive).

I should note that this is a work in progress - I've documented the vision and principles, but the implementation is still evolving. The early results are promising though: AI assistants navigating this conceptual tree find the context needed for specific coding tasks more effectively, significantly improving the quality of generated code.

There is another way formal methods parallel documentation: both are futile unless you can prove that the modelized/documented system matches the actual, live one.

"This is just a matter of discipline" is not very convincing, especially when the discipline involves long unpaid afterhours.

The examples I've seen in this report from AWS are mostly about one-shot events (helping going through important changes). It's good to see formal methods used in these cases of course, but I'd really like to read stories about how sustained use of formal methods helps reclaiming the high costs of the initial investment as the actual system evolves alongside the modelization.

Great question about MECE vs Divio's system! They actually complement each other rather than conflict.

MECE (Mutually Exclusive, Collectively Exhaustive) comes from management consulting and focuses on organizing concepts without overlap or gaps. Divio's system focuses on documentation types (tutorials, how-to, reference, explanation).

In the AI era, your question raises a fascinating point: if AI can dynamically adapt content to the user's needs, do we still need multiple presentation formats? I believe we do, but with a shift in approach.

With AI tools, we can maintain a single MECE-structured knowledge base (optimized for conceptual clarity and AI consumption) and then use AI to dynamically generate Divio-style presentations based on user needs. Rather than manually creating four different document types, we can have AI generate the appropriate format on demand.

In my experiments, I've found that a well-structured MECE knowledge base allows AI to generate much more accurate tutorials, how-tos, references, or explanations on demand. The AI adapts the presentation while drawing from a single source of truth.

This hybrid approach gives us the best of both worlds: conceptual clarity for AI consumption, and appropriate presentation for human needs - all while reducing the maintenance burden of multiple document versions.

Yes, that's Diataxis (formerly Divio). I faced similar challenges and found that combining it with MECE principles in my PAELLADOC framework made documentation much easier, especially with AI tools. Good luck getting your team started

The question would be whether with AI assistants you need to go through the effort of enforcing MECE or just strive for exhaustiveness and let them sort out repetition. I am also wondering whether there is a signal in repetition or even conflicts in documentation.

MECE seems to be just a mathematical partition, so it seems there is not need of a new term and acronym.

The part about S3 using lightweight formal methods in their ShardStore rust codebase is ongoing and operates on the system itself, not a model

At least in the TLA+ community, the new state-of-art approach is to use the formal model to generate a test suite.

That is interesting. Link?