ramxx/machinery

machinery is a design methodology and toolchain built around one idea: describe your software as a state machine first, and let everything else, tests, architecture rules, build instructions, and formal mathematical proofs of correctness, be generated from that single description instead of written by hand and then hoped to match it. The project exists because AI coding tools make it easy to write software quickly but do not make it easy to write software that stays correct as it grows. On anything beyond a small toy project, the actual code tends to drift away from the original design over time, an important rule gets broken somewhere far from where it was defined, and problems only surface once something breaks in production. The usual fix, reviewing code carefully by hand, really just means trusting the AI model, and that does not hold up at scale. machinery instead treats correctness as something you build and check mechanically, not something you simply hope for. To do this, machinery splits a software design into three layers that build on each other: a domain model describing the entities and rules that must always hold true, an architecture layer describing the system's components and what happens when each dependency fails, and finally state machines describing every state, transition, and failure mode, much of which is automatically derived from the earlier layers rather than written from scratch. The end result is a build document detailed enough for a coding assistant with no prior context to implement it under strict test driven development, plus the state machines themselves, which double as both the tests and the formal specification. The formal checking is done with established academic tools rather than invented ones: TLA+ and its model checker TLC exhaustively verify that a design terminates correctly and avoids deadlocks, while a separate tool called Alloy checks structural rules that are not about sequences of steps over time, such as access control or uniqueness constraints. The project also applies this thinking to AI agents themselves, modeling the surrounding control loop, tool calls, budgets, and approval steps as a provable state machine, while treating the AI's own decision making as something it constrains but does not try to formally prove. The project is written in Go and ships continuous integration, formal verification, security, and nightly test pipelines, visible as badges on its repository page.