I’ve got a prose to code with proof creator at GitHub - the-dark-factory/Crucible_AGPL: CRUCIBLE — a factory that turns a written specification into Ada/SPARK with a machine-checked proof, and refuses to deliver anything it could not prove. AGPL-3.0-or-later. · GitHub which uses the Qwen 2.5 coder and the qwen 3.8 coder to design and build code. GitHub - the-dark-factory/Crucible_AGPL: CRUCIBLE — a factory that turns a written specification into Ada/SPARK with a machine-checked proof, and refuses to deliver anything it could not prove. AGPL-3.0-or-later. · GitHub. , its best used with Claude under MCP but it provides proven code rather than vibed code from prose. Because it runs on local resources it is far more reasonable in electricity! The instructions on how to mcp are at Crucible_AGPL/CONNECTING.md at main · the-dark-factory/Crucible_AGPL · GitHub