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

Ephemaral acts as a hard-filter for your codebase. It helps AI agents converge on a specific shape of code that is easier to verify and that adapts to your company's standards — as verbose or as terse as you want.

There are two main parts of this tool.

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

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

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

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