LLMLL 开源项目：AI智能体在形式化合约下生成代码并由SMT求解器验证

LLMLL是一个编程语言和验证管道，允许AI智能体在形式化合约下生成代码，编译器通过Z3求解器验证每个函数体是否满足合约，拒绝类型正确但逻辑错误的实现。项目提供JSON-AST格式供AI代理使用，支持通过llmll checkout、patch、refine等命令协调智能体协作，验证失败的代码不会被合并。