Aura-State – A Formally Verified LLM State Machine Compiler

Name: Aura-State – A Formally Verified LLM State Machine Compiler
Availability: InStock
Author: rohanmunshi08

by rohanmunshi08·Mar 1, 2026·3 points·0 comments

Visit Project View on HN

AI Analysis

●●●BangerBig BrainWizardry

Formal verification for LLM workflows—CTL model checking, Z3 proofs, zero hallucination math.

Strengths

•Applies hardware verification (CTL model checking) to agent workflows, genuinely novel pairing.
•Z3 theorem prover validates extractions against business rules with mathematical proof, not heuristics.
•Conformal prediction wraps uncertainty in distribution-free confidence intervals with 95% calibration guarantee.

Weaknesses

•Requires workflows modeled as directed graphs—incompatible with open-ended agentic reasoning.
•Benchmark on 10 transcripts + 3 temporal properties is narrow; unclear scaling to production complexity.

Post Description

Over the last year, I've watched teams fail at enterprise LLM automation because they let the AI manage state and do math.

So I built Aura-State — an open-source Python framework that compiles LLM workflows into formally verified state machines.

Instead of hoping your agent does the right thing, Aura-State proves it does — using algorithms from hardware verification and statistical learning:

CTL Model Checking — proves workflow safety before execution (same technique used in flight control systems) Z3 Theorem Prover — formally verifies every LLM extraction against business rules Conformal Prediction — calibrated 95% confidence intervals on every field MCTS Routing — Monte Carlo Tree Search scores ambiguous transitions Sandboxed AST — zero-hallucination math, compiled from English rules

Live benchmark results (GPT-4o-mini, 10 transcripts): → 100% budget extraction accuracy → 20/20 Z3 proofs passed → 3/3 temporal properties proven → 65 unit tests passing

The gap between "it usually works" and "it provably works" is smaller than people think.

https://github.com/munshi007/Aura-State