Ephemaral

Ephemaral is an open-source tool, built on Lean and Z3, that you (or your agent of choice) can run locally directly from the terminal. It allows you to prove that your code is logically and mathematically correct.

This tool tries to solve the two biggest problems with LLM-generated code in practice:

• Code slop: diverging into verbose, difficult-to-maintain code
• Trust: that it actually follows your business rules

How it works

There are two main parts of this tool.

One is the verifier itself based on Lean 4 proofs and Z3 SMT solver, that you can clone or download here.

The other part is the parser that translates your business software original language (TypeScript, PHP, Python, Java, etc.) into a highly symbolic but verifiable language that Ephemaral can operate on, in a complete deterministic way.

Currently we only have a TypeScript parser, but given the modularity of the project anyone can contribute with a parser of their own!

For targeted information and examples, please refer to the official Ephemaral wiki.