diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index cb7320eb..cef21501 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -74,3 +74,18 @@ jobs:
       - name: difftest regressions and differential sweep
         working-directory: internal/difftest
         run: go test ./...
+
+  # The prover's solver-backed tests skip when z3 is missing, so they need a
+  # job that installs it and makes a missing solver a failure.
+  Prove:
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@v7
+      - uses: actions/setup-go@v7
+        with:
+          go-version-file: go.mod
+      - name: install z3
+        run: sudo apt-get update && sudo apt-get install -y z3
+      - name: prover tests
+        run: NUMSCRIPT_REQUIRE_Z3=1 go test ./internal/prove/... ./internal/cmd/...
diff --git a/flake.nix b/flake.nix
index 5d0fd199..2c1d1fde 100644
--- a/flake.nix
+++ b/flake.nix
@@ -47,6 +47,7 @@
             goperf
             gotools
             just
+            z3
           ];
           unstablePackages = with pkgs-unstable; [
             golangci-lint
diff --git a/internal/cmd/ir.go b/internal/cmd/ir.go
new file mode 100644
index 00000000..f11cfa67
--- /dev/null
+++ b/internal/cmd/ir.go
@@ -0,0 +1,89 @@
+package cmd
+
+import (
+	"fmt"
+	"os"
+
+	"github.com/formancehq/numscript/internal/compiler"
+	"github.com/formancehq/numscript/internal/ir"
+	"github.com/formancehq/numscript/internal/parser"
+
+	"github.com/spf13/cobra"
+)
+
+type IRArgs struct {
+	OutputPath string
+}
+
+// compileScriptToIR reads a numscript source file and compiles it to IR,
+// printing parse and compile errors on stderr the way `run` does.
+func compileScriptToIR(scriptPath string) ([]ir.Instr, error) {
+	content, err := readIRSource(scriptPath)
+	if err != nil {
+		return nil, err
+	}
+	src := string(content)
+
+	parseResult := parser.Parse(src)
+	if len(parseResult.Errors) != 0 {
+		fmt.Fprint(os.Stderr, parser.ParseErrorsToString(parseResult.Errors, src))
+		return nil, fmt.Errorf("parsing failed")
+	}
+
+	instrs, _, err := compiler.CompileToIR(parseResult.Value, nil)
+	if err != nil {
+		fmt.Fprintln(os.Stderr, err.Error())
+		if ranged, ok := err.(parser.Ranged); ok {
+			fmt.Fprintln(os.Stderr, ranged.GetRange().ShowOnSource(src))
+		}
+		return nil, fmt.Errorf("compilation failed")
+	}
+	return instrs, nil
+}
+
+func dumpIR(scriptPath string, opts IRArgs) error {
+	instrs, err := compileScriptToIR(scriptPath)
+	if err != nil {
+		return err
+	}
+
+	text := ir.Dump(instrs)
+	if opts.OutputPath == "" || opts.OutputPath == stdioPath {
+		_, err := os.Stdout.WriteString(text)
+		return err
+	}
+	return os.WriteFile(opts.OutputPath, []byte(text), 0o644)
+}
+
+func getIRCmd() *cobra.Command {
+	opts := IRArgs{}
+
+	cmd := cobra.Command{
+		Use:   "ir <file.num>",
+		Short: "Compile a numscript file and dump its textual IR",
+		Long: `Compile a numscript file and dump the textual IR the compiler produces, before
+it is assembled into bytecode. The output goes to stdout unless --output says
+otherwise, so it can be piped into assemble:
+numscript ir folder/my-script.num | numscript assemble - > folder/my-script.numb
+
+Pass - as the path to read the script from stdin.
+
+The IR format tracks an unstable instruction set and is not a public interface.
+`,
+		Args: cobra.ExactArgs(1),
+		RunE: func(cmd *cobra.Command, args []string) error {
+			err := dumpIR(args[0], opts)
+			if err != nil {
+				cmd.SilenceErrors = true
+				cmd.SilenceUsage = true
+				return err
+			}
+
+			return nil
+		},
+	}
+
+	cmd.Flags().StringVarP(&opts.OutputPath, "output", "o", "", "Path where to write the IR ('-' for stdout)")
+
+	return &cmd
+}
diff --git a/internal/cmd/ir_test.go b/internal/cmd/ir_test.go
new file mode 100644
index 00000000..3d6fe6f6
--- /dev/null
+++ b/internal/cmd/ir_test.go
@@ -0,0 +1,42 @@
+package cmd
+
+import (
+	"os"
+	"path/filepath"
+	"testing"
+
+	"github.com/formancehq/numscript/internal/ir"
+	"github.com/stretchr/testify/require"
+)
+
+func TestDumpIRRoundTrips(t *testing.T) {
+	dir := t.TempDir()
+	scriptPath := filepath.Join(dir, "x.num")
+	require.NoError(t, os.WriteFile(scriptPath, []byte(`send [USD/2 10] (
+  source = @src
+  destination = @dest
+)`), 0o644))
+
+	outPath := filepath.Join(dir, "x.ir")
+	require.NoError(t, dumpIR(scriptPath, IRArgs{OutputPath: outPath}))
+
+	text, err := os.ReadFile(outPath)
+	require.NoError(t, err)
+
+	instrs, errs := ir.Parse(string(text))
+	require.Empty(t, errs)
+	require.Equal(t, string(text), ir.Dump(instrs))
+	require.NoError(t, ir.Typecheck(instrs))
+}
+
+func TestDumpIRReportsCompileErrors(t *testing.T) {
+	dir := t.TempDir()
+	scriptPath := filepath.Join(dir, "x.num")
+	require.NoError(t, os.WriteFile(scriptPath, []byte(`send [USD/2 10] (
+  source = @src
+  destination = $dest
+)`), 0o644))
+
+	err := dumpIR(scriptPath, IRArgs{OutputPath: filepath.Join(dir, "x.ir")})
+	require.EqualError(t, err, "compilation failed")
+}
diff --git a/internal/cmd/prove.go b/internal/cmd/prove.go
new file mode 100644
index 00000000..609ec51d
--- /dev/null
+++ b/internal/cmd/prove.go
@@ -0,0 +1,214 @@
+package cmd
+
+import (
+	"context"
+	"errors"
+	"fmt"
+	"os"
+	"path/filepath"
+	"strings"
+	"time"
+
+	"github.com/formancehq/numscript/internal/ir"
+	"github.com/formancehq/numscript/internal/prove"
+	"github.com/formancehq/numscript/internal/prove/encode"
+	"github.com/formancehq/numscript/internal/prove/prop"
+	"github.com/formancehq/numscript/internal/prove/smt"
+
+	"github.com/spf13/cobra"
+)
+
+type ProveArgs struct {
+	Props        []string
+	PropsPath    string
+	Solver       string
+	Timeout      time.Duration
+	EmitSMT      string
+	OutFormatOpt string
+}
+
+// exitCodeError carries the exit code the prove command ends with.
+type exitCodeError struct {
+	code int
+}
+
+func (e exitCodeError) Error() string { return fmt.Sprintf("exit %d", e.code) }
+
+func loadInstrs(scriptPath string) ([]ir.Instr, error) {
+	if !strings.HasSuffix(scriptPath, ".ir") {
+		return compileScriptToIR(scriptPath)
+	}
+	content, err := readIRSource(scriptPath)
+	if err != nil {
+		return nil, err
+	}
+	src := string(content)
+	instrs, irErrs := ir.Parse(src)
+	if len(irErrs) != 0 {
+		for _, irErr := range irErrs {
+			fmt.Fprintln(os.Stderr, irErr.Error())
+			fmt.Fprintln(os.Stderr, irErr.Range.ShowOnSource(src))
+		}
+		return nil, fmt.Errorf("parsing failed")
+	}
+	return instrs, nil
+}
+
+func loadProps(scriptPath string, opts ProveArgs) ([]prop.Property, error) {
+	var props []prop.Property
+	for i, src := range opts.Props {
+		p, errs := prop.ParseInline(src)
+		if len(errs) != 0 {
+			for _, e := range errs {
+				fmt.Fprintf(os.Stderr, "--prop[%d]: %s\n", i+1, e.Error())
+				fmt.Fprintln(os.Stderr, e.Range.ShowOnSource(src))
+			}
+			return nil, fmt.Errorf("invalid property")
+		}
+		if p.Name == "" {
+			p.Name = fmt.Sprintf("prop%d", i+1)
+		}
+		props = append(props, p)
+	}
+
+	path := opts.PropsPath
+	if path == "" && len(opts.Props) == 0 {
+		path = scriptPath + ".props"
+		if _, err := os.Stat(path); err != nil {
+			return nil, fmt.Errorf("no properties: pass --prop, or create '%s'", path)
+		}
+	}
+	if path != "" {
+		content, err := os.ReadFile(path)
+		if err != nil {
+			return nil, err
+		}
+		src := string(content)
+		parsed, errs := prop.ParseFile(src)
+		if len(errs) != 0 {
+			for _, e := range errs {
+				fmt.Fprintf(os.Stderr, "%s:%s\n", path, e.Error())
+				fmt.Fprintln(os.Stderr, e.Range.ShowOnSource(src))
+			}
+			return nil, fmt.Errorf("invalid properties file")
+		}
+		props = append(props, parsed...)
+	}
+	return props, nil
+}
+
+func proveScript(scriptPath string, opts ProveArgs) error {
+	instrs, err := loadInstrs(scriptPath)
+	if err != nil {
+		return err
+	}
+	props, err := loadProps(scriptPath, opts)
+	if err != nil {
+		return err
+	}
+
+	solver := smt.Solver{Path: opts.Solver, Timeout: opts.Timeout}
+	if err := solver.Available(); err != nil {
+		return err
+	}
+
+	report, err := prove.Check(context.Background(), instrs, props, prove.Options{Solver: solver})
+	if err != nil {
+		var unsupported encode.UnsupportedError
+		var propErr prove.PropertyError
+		switch {
+		case errors.As(err, &unsupported):
+			return fmt.Errorf("cannot prove: %w", err)
+		case errors.As(err, &propErr):
+			for _, e := range propErr.Errors {
+				fmt.Fprintf(os.Stderr, "property %q: %s\n", propErr.Property.Name, e.Error())
+			}
+			return fmt.Errorf("invalid property")
+		}
+		return err
+	}
+
+	if opts.EmitSMT != "" {
+		for _, res := range report.Results {
+			if opts.EmitSMT == stdioPath {
+				fmt.Printf("; ---- %s\n%s\n", res.Property.Name, res.SMT)
+				continue
+			}
+			if err := os.MkdirAll(opts.EmitSMT, 0o755); err != nil {
+				return err
+			}
+			if err := os.WriteFile(filepath.Join(opts.EmitSMT, res.Property.Name+".smt2"), []byte(res.SMT), 0o644); err != nil {
+				return err
+			}
+		}
+	}
+
+	switch opts.OutFormatOpt {
+	case OutputFormatJson:
+		out, err := report.JSON(scriptPath)
+		if err != nil {
+			return err
+		}
+		if _, err := os.Stdout.Write(out); err != nil {
+			return err
+		}
+	case OutputFormatPretty:
+		if _, err := os.Stdout.WriteString(report.Pretty(scriptPath)); err != nil {
+			return err
+		}
+	default:
+		return fmt.Errorf("invalid output format: %s", opts.OutFormatOpt)
+	}
+
+	if code := report.ExitCode(); code != 0 {
+		return exitCodeError{code}
+	}
+	return nil
+}
+
+func getProveCmd() *cobra.Command {
+	opts := ProveArgs{}
+
+	cmd := cobra.Command{
+		Use:   "prove <file.num|file.ir>",
+		Short: "Prove properties of a script for every initial balance",
+		Long: `Compile a numscript file (or parse a textual IR file) and check properties
+written in the property language against it, for every initial balance. Each
+property is either proved, refuted with a counterexample (initial balances the
+real vm confirms), or left unknown when the solver times out.
+
+Properties come from --prop (repeatable) and/or --props <file>; with neither,
+'<script>.props' next to the script is used. See prove.md for the language.
+
+Exit codes: 0 every property holds; 1 a property has a counterexample; 2 no
+counterexample but a property is unknown; 3 the script is not supported, a
+property is invalid, the solver is missing, or the prover disagrees with the vm.
+
+Needs an SMT-LIB2 solver on PATH: z3 (default) or cvc5 (--solver cvc5).
+`,
+		Args: cobra.ExactArgs(1),
+		RunE: func(cmd *cobra.Command, args []string) error {
+			err := proveScript(args[0], opts)
+			if err != nil {
+				cmd.SilenceUsage = true
+				var exit exitCodeError
+				if errors.As(err, &exit) {
+					os.Exit(exit.code)
+				}
+				cmd.SilenceErrors = true
+				fmt.Fprintln(os.Stderr, err)
+				os.Exit(3)
+			}
+			return nil
+		},
+	}
+
+	cmd.Flags().StringArrayVar(&opts.Props, "prop", nil, "A property to check ('[name:] formula'); repeatable")
+	cmd.Flags().StringVar(&opts.PropsPath, "props", "", "Path of a properties file (default: '<script>.props')")
+	cmd.Flags().StringVar(&opts.Solver, "solver", "z3", "SMT-LIB2 solver executable: z3, cvc5, or a path")
+	cmd.Flags().DurationVar(&opts.Timeout, "timeout", 10*time.Second, "Solver time limit per property")
+	cmd.Flags().StringVar(&opts.EmitSMT, "emit-smt", "", "Write each property's SMT-LIB2 problem to this directory ('-' for stdout)")
+	cmd.Flags().StringVarP(&opts.OutFormatOpt, "output-format", "o", OutputFormatPretty, "Set the output format. Available options: pretty, json.")
+
+	return &cmd
+}
diff --git a/internal/cmd/prove_test.go b/internal/cmd/prove_test.go
new file mode 100644
index 00000000..adb180b5
--- /dev/null
+++ b/internal/cmd/prove_test.go
@@ -0,0 +1,73 @@
+package cmd
+
+import (
+	"os"
+	"path/filepath"
+	"testing"
+	"time"
+
+	"github.com/formancehq/numscript/internal/prove/smt"
+	"github.com/stretchr/testify/require"
+)
+
+func requireZ3(t *testing.T) {
+	t.Helper()
+	if err := (smt.Solver{}).Available(); err != nil {
+		if os.Getenv("NUMSCRIPT_REQUIRE_Z3") != "" {
+			t.Fatal(err)
+		}
+		t.Skip(err)
+	}
+}
+
+func writeProveFixture(t *testing.T) string {
+	t.Helper()
+	dir := t.TempDir()
+	scriptPath := filepath.Join(dir, "x.num")
+	require.NoError(t, os.WriteFile(scriptPath, []byte(`send [USD/2 10] (
+  source = @src
+  destination = @dest
+)`), 0o644))
+	return scriptPath
+}
+
+func TestProveExitCodes(t *testing.T) {
+	requireZ3(t)
+	scriptPath := writeProveFixture(t)
+	base := ProveArgs{Solver: "z3", Timeout: 5 * time.Second, OutFormatOpt: OutputFormatJson}
+
+	opts := base
+	opts.Props = []string{"success => received(@dest, USD/2) == 10"}
+	require.NoError(t, proveScript(scriptPath, opts))
+
+	opts = base
+	opts.Props = []string{"holds: success => received(@dest, USD/2) == 10", "refuted: success"}
+	require.Equal(t, exitCodeError{1}, proveScript(scriptPath, opts))
+
+	// no --prop and no sidecar file
+	require.ErrorContains(t, proveScript(scriptPath, base), "no properties")
+
+	opts = base
+	opts.Props = []string{"after(@nobody, USD/2) == 0"}
+	require.ErrorContains(t, proveScript(scriptPath, opts), "invalid property")
+
+	opts = base
+	opts.Props = []string{"success =>"}
+	require.ErrorContains(t, proveScript(scriptPath, opts), "invalid property")
+}
+
+func TestProvePropsFileAndEmitSMT(t *testing.T) {
+	requireZ3(t)
+	scriptPath := writeProveFixture(t)
+	require.NoError(t, os.WriteFile(scriptPath+".props", []byte(`prop ok: before(@src, USD/2) >= 10 => success`), 0o644))
+	smtDir := filepath.Join(filepath.Dir(scriptPath), "smt")
+	require.NoError(t, proveScript(scriptPath, ProveArgs{Solver: "z3", Timeout: 5 * time.Second, EmitSMT: smtDir, OutFormatOpt: OutputFormatPretty}))
+	emitted, err := os.ReadFile(filepath.Join(smtDir, "ok.smt2"))
+	require.NoError(t, err)
+	require.Contains(t, string(emitted), "(assert (not property))")
+
+	// an unsupported script is a hard error
+	require.NoError(t, os.WriteFile(scriptPath, []byte(`vars { account $d }
+send [USD/2 10] (source = @src destination = $d)`), 0o644))
+	require.ErrorContains(t, proveScript(scriptPath, ProveArgs{Solver: "z3", OutFormatOpt: OutputFormatPretty}), "script variables are not supported")
+}
diff --git a/internal/cmd/root.go b/internal/cmd/root.go
index ebd8f3de..622fc9a0 100644
--- a/internal/cmd/root.go
+++ b/internal/cmd/root.go
@@ -34,7 +34,7 @@ func Execute(options CliOptions) {
 	// of --help unless NUMSCRIPT_EXPERIMENTAL_CLI is set. It is always registered
 	// and runnable, like lsp and mcp.
 	hidden := os.Getenv("NUMSCRIPT_EXPERIMENTAL_CLI") == ""
-	for _, experimentalCmd := range []*cobra.Command{getAssembleCmd(), getBytecodeRunCmd()} {
+	for _, experimentalCmd := range []*cobra.Command{getAssembleCmd(), getBytecodeRunCmd(), getIRCmd(), getProveCmd()} {
 		experimentalCmd.Hidden = hidden
 		rootCmd.AddCommand(experimentalCmd)
 	}
diff --git a/internal/compiler/compiler.go b/internal/compiler/compiler.go
index 24b6ec02..ecd0da8c 100644
--- a/internal/compiler/compiler.go
+++ b/internal/compiler/compiler.go
@@ -21,21 +21,32 @@ import (
 // interpreter.RunProgram, the script's own #![feature(..)] declarations are
 // unioned in.
 func Compile(program parser.Program, featureFlags map[string]struct{}) (VarsEncoder, vm.Program, error) {
-	compiled, cErr := compileProgramToIR(program, featureFlags)
-	if cErr != nil {
-		return VarsEncoder{}, vm.Program{}, cErr
-	}
-
-	if err := ir.Typecheck(compiled.instructions); err != nil {
+	instrs, varsEncoder, err := CompileToIR(program, featureFlags)
+	if err != nil {
 		return VarsEncoder{}, vm.Program{}, err
 	}
 
-	prog, err := ir.Assemble(compiled.instructions)
+	prog, err := ir.Assemble(instrs)
 	if err != nil {
 		return VarsEncoder{}, vm.Program{}, err
 	}
 
-	return compiled.varsEncoder, prog, nil
+	return varsEncoder, prog, nil
+}
+
+// CompileToIR lowers a parsed program to its typechecked IR stream, for tools
+// that consume the IR rather than bytecode (the ir dump command, the prover).
+func CompileToIR(program parser.Program, featureFlags map[string]struct{}) ([]ir.Instr, VarsEncoder, error) {
+	compiled, cErr := compileProgramToIR(program, featureFlags)
+	if cErr != nil {
+		return nil, VarsEncoder{}, cErr
+	}
+
+	if err := ir.Typecheck(compiled.instructions); err != nil {
+		return nil, VarsEncoder{}, err
+	}
+
+	return compiled.instructions, compiled.varsEncoder, nil
 }
 
 type compiledProgramIR struct {
diff --git a/internal/prove/encode/__snapshots__/encode_test.snap b/internal/prove/encode/__snapshots__/encode_test.snap
new file mode 100755
index 00000000..d748991e
--- /dev/null
+++ b/internal/prove/encode/__snapshots__/encode_test.snap
@@ -0,0 +1,27 @@
+
+[TestSimpleSendText - 1]
+(set-logic QF_LIA)
+(set-option :produce-models true)
+(declare-const |before(@dest,USD/2)| Int)
+(declare-const |before(@src,USD/2)| Int)
+; 18: $r9 = pull_account(account: $r6, cap: $r4, overdraft: $r7)
+(define-fun available@18 () Int (ite (< |before(@src,USD/2)| 0) 0 |before(@src,USD/2)|))
+(define-fun $r9@18 () Int (ite (< 10 available@18) 10 available@18))
+(define-fun |bal(@src,USD/2)@18| () Int (- |before(@src,USD/2)| $r9@18))
+(define-fun fail@20 () Bool (not (= $r9@18 10)))
+(define-fun alive@20 () Bool (= $r9@18 10))
+; 22: send_to_account(account: $r10)
+(define-fun |bal(@dest,USD/2)@22| () Int (+ |before(@dest,USD/2)| $r9@18))
+
+; outputs: the ledger applies nothing on failure
+(define-fun fails () Bool fail@20)
+(define-fun success () Bool (not fails))
+(define-fun |sent(@dest,USD/2)| () Int 0)
+(define-fun |received(@dest,USD/2)| () Int (ite fails 0 $r9@18))
+(define-fun |after(@dest,USD/2)| () Int (+ |before(@dest,USD/2)| (- |received(@dest,USD/2)| |sent(@dest,USD/2)|)))
+(define-fun |sent(@src,USD/2)| () Int (ite fails 0 $r9@18))
+(define-fun |received(@src,USD/2)| () Int 0)
+(define-fun |after(@src,USD/2)| () Int (+ |before(@src,USD/2)| (- |received(@src,USD/2)| |sent(@src,USD/2)|)))
+(define-fun |moved(@src,@dest,USD/2)| () Int (ite fails 0 $r9@18))
+
+---
diff --git a/internal/prove/encode/encode.go b/internal/prove/encode/encode.go
new file mode 100644
index 00000000..4ef47c88
--- /dev/null
+++ b/internal/prove/encode/encode.go
@@ -0,0 +1,630 @@
+package encode
+
+import (
+	"errors"
+	"fmt"
+	"math/big"
+
+	"github.com/formancehq/numscript/internal/funds"
+	"github.com/formancehq/numscript/internal/ir"
+	"github.com/formancehq/numscript/internal/prove/smt"
+	"github.com/formancehq/numscript/internal/vm"
+)
+
+type encoder struct {
+	instrs []ir.Instr
+	sc     *smt.Script
+
+	keys     map[Key]struct{}
+	moves    map[MoveKey]struct{}
+	accounts map[string]struct{}
+	assets   map[string]struct{}
+
+	pending map[ir.Label][]*state
+	fails   []FailSite
+	cur     *state
+}
+
+// Encode models instrs. extraKeys and extraMoves are pairs a property names
+// that the program may never touch; they get a free before input and zero
+// movements.
+func Encode(instrs []ir.Instr, extraKeys []Key, extraMoves []MoveKey) (*Problem, error) {
+	if err := ir.Typecheck(instrs); err != nil {
+		return nil, err
+	}
+	prog, err := ir.Assemble(instrs)
+	if err != nil {
+		if errors.Is(err, ir.ErrRegisterBankOverflow) || errors.Is(err, ir.ErrProgramTooLarge) {
+			return nil, UnsupportedError{Index: -1, Reason: err.Error()}
+		}
+		return nil, err
+	}
+	if err := vm.Verify(prog); err != nil {
+		return nil, err
+	}
+
+	e := &encoder{
+		instrs:   instrs,
+		sc:       smt.NewBareScript(),
+		keys:     map[Key]struct{}{},
+		moves:    map[MoveKey]struct{}{},
+		accounts: map[string]struct{}{},
+		assets:   map[string]struct{}{},
+		pending:  map[ir.Label][]*state{},
+		cur:      newState(),
+	}
+	if err := e.prescan(); err != nil {
+		return nil, err
+	}
+	for pos, in := range instrs {
+		if lm, ok := in.(ir.LabelMarker); ok {
+			edges := append([]*state{e.cur}, e.pending[lm.Label]...)
+			delete(e.pending, lm.Label)
+			merged, err := e.merge(pos, edges)
+			if err != nil {
+				return nil, err
+			}
+			e.cur = merged
+			continue
+		}
+		if e.cur.dead {
+			continue
+		}
+		if err := e.step(pos, in); err != nil {
+			return nil, err
+		}
+	}
+	if len(e.pending) != 0 {
+		return nil, fmt.Errorf("encode: a jump targets a label that is not in the program")
+	}
+	return e.finish(extraKeys, extraMoves), nil
+}
+
+func (e *encoder) text(pos int) string {
+	if pos < 0 {
+		return ""
+	}
+	return fmt.Sprint(e.instrs[pos])
+}
+
+func (e *encoder) unsupported(pos int, reason string) error {
+	return UnsupportedError{Index: pos, Text: e.text(pos), Reason: reason}
+}
+
+// prescan rejects what v1 does not model, naming the first offending
+// instruction whether or not it is reachable, and collects every (account,
+// asset) pair a funds operand can name. Constants are followed in text order
+// with jumps ignored, so an account on a path the model folds away (a run that
+// always fails first) is still known to properties.
+func (e *encoder) prescan() error {
+	consts := map[ir.Reg]string{}
+	asset, assetKnown := "", false
+	touchPair := func(account ir.Reg, assetName string, known bool) {
+		if a, ok := consts[account]; ok && known {
+			e.touch(Key{a, assetName})
+		}
+	}
+	for pos, in := range e.instrs {
+		reason := ""
+		switch in := in.(type) {
+		case ir.LoadStr:
+			consts[in.Dest] = in.Value
+		case ir.UnaryOp:
+			if _, ok := in.Op.(ir.OpStrCopy); ok {
+				if v, ok := consts[in.Arg]; ok {
+					consts[in.Dest] = v
+				} else {
+					delete(consts, in.Dest)
+				}
+			}
+		case ir.BinaryOp:
+			if _, ok := in.Op.(ir.OpAddString); ok {
+				l, lok := consts[in.Left]
+				r, rok := consts[in.Right]
+				if lok && rok {
+					consts[in.Dest] = l + r
+				} else {
+					delete(consts, in.Dest)
+				}
+			}
+		case ir.SetCurrentAsset:
+			asset, assetKnown = consts[in.Asset]
+		case ir.LoadVar:
+			reason = "script variables are not supported"
+		case ir.MetaVar, ir.MetaMonetary:
+			reason = "metadata reads are not supported"
+		case ir.AssertValidColor:
+			reason = "asset colors are not supported"
+		case ir.AssertValidScope, ir.AssertUnscoped:
+			reason = "scoped accounts are not supported"
+		case ir.PullAccount:
+			if in.Color != nil {
+				reason = "asset colors are not supported"
+			} else if in.Scope != nil {
+				reason = "scoped accounts are not supported"
+			}
+			touchPair(in.Account, asset, assetKnown)
+		case ir.SendToAccount:
+			if in.Scope != nil {
+				reason = "scoped accounts are not supported"
+			}
+			if in.Account != nil {
+				touchPair(*in.Account, asset, assetKnown)
+			}
+		case ir.Save:
+			if in.Scope != nil {
+				reason = "scoped accounts are not supported"
+			}
+			a, ok := consts[in.Asset]
+			touchPair(in.Account, a, ok)
+		case ir.FetchBalance:
+			if in.Scope != nil {
+				reason = "scoped accounts are not supported"
+			}
+			a, ok := consts[in.Asset]
+			touchPair(in.Account, a, ok)
+		}
+		if reason != "" {
+			return e.unsupported(pos, reason)
+		}
+	}
+	return nil
+}
+
+func (e *encoder) def(name string, t smt.Term) smt.Term {
+	return e.sc.Define(name, t)
+}
+
+func (e *encoder) comment(pos int) {
+	e.sc.Comment("%d: %s", pos, e.text(pos))
+}
+
+func (e *encoder) touch(k Key) {
+	e.keys[k] = struct{}{}
+	e.accounts[k.Account] = struct{}{}
+	e.assets[k.Asset] = struct{}{}
+}
+
+// balanceOf is the running balance of k in s: the before input until the
+// program writes it.
+func (e *encoder) balanceOf(s *state, k Key) smt.Term {
+	if t, ok := s.bal[k]; ok {
+		return t
+	}
+	e.touch(k)
+	return smt.Symbol(BeforeName(k), smt.SortInt)
+}
+
+func (e *encoder) reg(pos int, r ir.Reg) (regVal, error) {
+	v, ok := e.cur.regs[r]
+	if !ok {
+		return regVal{}, fmt.Errorf("encode: instruction %d: register $r%d is read before being written", pos, r)
+	}
+	return v, nil
+}
+
+func (e *encoder) term(pos int, r ir.Reg) (smt.Term, error) {
+	v, err := e.reg(pos, r)
+	if err != nil {
+		return nil, err
+	}
+	if v.t == nil {
+		return nil, fmt.Errorf("encode: instruction %d: register $r%d is not an int or bool", pos, r)
+	}
+	return v.t, nil
+}
+
+func (e *encoder) optTerm(pos int, r *ir.Reg) (smt.Term, error) {
+	if r == nil {
+		return nil, nil
+	}
+	return e.term(pos, *r)
+}
+
+func (e *encoder) str(pos int, r ir.Reg) (string, error) {
+	v, err := e.reg(pos, r)
+	if err != nil {
+		return "", err
+	}
+	if !v.s.known {
+		return "", e.unsupported(pos, fmt.Sprintf("the value of string register $r%d is not a constant", r))
+	}
+	return v.s.s, nil
+}
+
+func (e *encoder) portion(pos int, r ir.Reg) (*linForm, error) {
+	v, err := e.reg(pos, r)
+	if err != nil {
+		return nil, err
+	}
+	if v.p == nil {
+		return nil, fmt.Errorf("encode: instruction %d: register $r%d is not a portion", pos, r)
+	}
+	return v.p, nil
+}
+
+func (e *encoder) currentAsset(pos int) (string, error) {
+	if !e.cur.asset.known {
+		return "", e.unsupported(pos, "the current asset is not a constant")
+	}
+	return e.cur.asset.s, nil
+}
+
+func (e *encoder) setInt(pos int, dest ir.Reg, t smt.Term) {
+	e.cur.regs[dest] = regVal{t: e.def(fmt.Sprintf("$r%d@%d", dest, pos), t)}
+}
+
+func (e *encoder) setStr(dest ir.Reg, s string, known bool) {
+	e.cur.regs[dest] = regVal{s: strVal{known: known, s: s}}
+}
+
+// fail records a site that aborts the run when cond holds. A path on which
+// the abort is certain is dead from here on: nothing it would compute is
+// applied, and the outputs are masked by fails.
+func (e *encoder) fail(pos int, kind FailKind, cond smt.Term) {
+	flagTerm := smt.And(e.cur.alive, cond)
+	if smt.IsFalse(flagTerm) {
+		return
+	}
+	flag := e.sc.DefineAlways(fmt.Sprintf("fail@%d", pos), flagTerm)
+	e.fails = append(e.fails, FailSite{Index: pos, Text: e.text(pos), Kind: kind, Flag: flag})
+	alive := smt.And(e.cur.alive, smt.Not(cond))
+	if smt.IsFalse(alive) {
+		e.cur = deadState()
+		return
+	}
+	e.cur.alive = e.def(fmt.Sprintf("alive@%d", pos), alive)
+}
+
+func (e *encoder) branch(pos int, cond smt.Term, target ir.Label) {
+	switch {
+	case smt.IsTrue(cond):
+		e.pending[target] = append(e.pending[target], e.cur)
+		e.cur = deadState()
+	case smt.IsFalse(cond):
+	default:
+		taken := e.cur.clone()
+		taken.reach = e.def(fmt.Sprintf("reach@%d.t", pos), smt.And(e.cur.reach, cond))
+		taken.alive = e.def(fmt.Sprintf("alive@%d.t", pos), smt.And(e.cur.alive, cond))
+		e.pending[target] = append(e.pending[target], taken)
+		e.cur.reach = e.def(fmt.Sprintf("reach@%d.f", pos), smt.And(e.cur.reach, smt.Not(cond)))
+		e.cur.alive = e.def(fmt.Sprintf("alive@%d.f", pos), smt.And(e.cur.alive, smt.Not(cond)))
+	}
+}
+
+func (e *encoder) step(pos int, in ir.Instr) error {
+	switch in := in.(type) {
+	case ir.LoadInt:
+		e.cur.regs[in.Dest] = regVal{t: smt.Int(&in.Value)}
+	case ir.LoadStr:
+		e.setStr(in.Dest, in.Value, true)
+	case ir.ConstBool:
+		e.cur.regs[in.Dest] = regVal{t: smt.Bool(in.Value)}
+	case ir.BinaryOp:
+		return e.binary(pos, in)
+	case ir.UnaryOp:
+		return e.unary(pos, in)
+	case ir.JmpIfTrue:
+		c, err := e.term(pos, in.Cond)
+		if err != nil {
+			return err
+		}
+		e.branch(pos, c, in.Target)
+	case ir.JmpIfFalse:
+		c, err := e.term(pos, in.Cond)
+		if err != nil {
+			return err
+		}
+		e.branch(pos, smt.Not(c), in.Target)
+	case ir.Jmp:
+		e.branch(pos, smt.Bool(true), in.Target)
+	case ir.SetCurrentAsset:
+		v, err := e.reg(pos, in.Asset)
+		if err != nil {
+			return err
+		}
+		e.cur.asset = v.s
+	case ir.PullAccount:
+		return e.pull(pos, in)
+	case ir.SendToAccount:
+		return e.send(pos, in)
+	case ir.Save:
+		return e.save(pos, in)
+	case ir.FetchBalance:
+		return e.fetchBalance(pos, in)
+	case ir.MarkPush:
+		e.cur.marks = append(e.cur.marks, frame{pos: smt.Bool(true)})
+	case ir.MarkEnd:
+		return e.markEnd(pos, in)
+	case ir.CheckEnoughFunds:
+		got, err := e.term(pos, in.Got)
+		if err != nil {
+			return err
+		}
+		needed, err := e.term(pos, in.Needed)
+		if err != nil {
+			return err
+		}
+		e.fail(pos, MissingFunds, smt.Ne(got, needed))
+	case ir.AssertNonNegativeAmount:
+		t, err := e.term(pos, in.Amount)
+		if err != nil {
+			return err
+		}
+		e.fail(pos, NegativeAmount, smt.Lt(t, smt.Int64(0)))
+	case ir.AssertNonNegativeBalance:
+		t, err := e.term(pos, in.Balance)
+		if err != nil {
+			return err
+		}
+		e.fail(pos, NegativeBalance, smt.Lt(t, smt.Int64(0)))
+	case ir.AssertNonNegativePortion:
+		p, err := e.portion(pos, in.Portion)
+		if err != nil {
+			return err
+		}
+		e.fail(pos, NegativePortion, smt.Lt(p.sign(), smt.Int64(0)))
+	case ir.AssertLeftover:
+		p, err := e.portion(pos, in.Portion)
+		if err != nil {
+			return err
+		}
+		if in.Exact {
+			e.fail(pos, AllotmentSum, smt.Ne(p.sign(), smt.Int64(0)))
+		} else {
+			e.fail(pos, AllotmentSum, smt.Lt(p.sign(), smt.Int64(0)))
+		}
+	case ir.AssertSameAsset:
+		l, err := e.str(pos, in.Left)
+		if err != nil {
+			return err
+		}
+		r, err := e.str(pos, in.Right)
+		if err != nil {
+			return err
+		}
+		if l != r {
+			e.fail(pos, AssetMismatch, smt.Bool(true))
+		}
+	case ir.AssertValidAccount:
+		a, err := e.str(pos, in.Account)
+		if err != nil {
+			return err
+		}
+		if !funds.ValidateAccount(a) {
+			e.fail(pos, InvalidAccount, smt.Bool(true))
+		}
+	case ir.SetTxMeta, ir.SetAccountMeta:
+	default:
+		return e.unsupported(pos, "not modeled")
+	}
+	return nil
+}
+
+func (e *encoder) binary(pos int, in ir.BinaryOp) error {
+	switch in.Op.(type) {
+	case ir.OpAddInt, ir.OpSubInt, ir.OpLtInt, ir.OpEqInt:
+		l, err := e.term(pos, in.Left)
+		if err != nil {
+			return err
+		}
+		r, err := e.term(pos, in.Right)
+		if err != nil {
+			return err
+		}
+		var t smt.Term
+		switch in.Op.(type) {
+		case ir.OpAddInt:
+			t = smt.Add(l, r)
+		case ir.OpSubInt:
+			t = smt.Sub(l, r)
+		case ir.OpLtInt:
+			t = smt.Lt(l, r)
+		case ir.OpEqInt:
+			t = smt.Eq(l, r)
+		}
+		e.setInt(pos, in.Dest, t)
+
+	case ir.OpAddPortion, ir.OpSubPortion, ir.OpMulPortion, ir.OpLtPortion, ir.OpEqPortion:
+		l, err := e.portion(pos, in.Left)
+		if err != nil {
+			return err
+		}
+		r, err := e.portion(pos, in.Right)
+		if err != nil {
+			return err
+		}
+		switch in.Op.(type) {
+		case ir.OpAddPortion:
+			e.cur.regs[in.Dest] = regVal{p: l.add(r)}
+		case ir.OpSubPortion:
+			e.cur.regs[in.Dest] = regVal{p: l.sub(r)}
+		case ir.OpMulPortion:
+			p, ok := l.mul(r)
+			if !ok {
+				return e.unsupported(pos, "nonlinear portion arithmetic")
+			}
+			e.cur.regs[in.Dest] = regVal{p: p}
+		case ir.OpLtPortion:
+			e.setInt(pos, in.Dest, l.lt(r))
+		case ir.OpEqPortion:
+			e.setInt(pos, in.Dest, l.eq(r))
+		}
+
+	case ir.OpMakePortion:
+		num, err := e.term(pos, in.Left)
+		if err != nil {
+			return err
+		}
+		den, err := e.term(pos, in.Right)
+		if err != nil {
+			return err
+		}
+		d, ok := smt.AsInt(den)
+		if !ok {
+			return e.unsupported(pos, "nonlinear portion arithmetic: the denominator is not a constant")
+		}
+		if d.Sign() == 0 {
+			e.fail(pos, DivideByZero, smt.Bool(true))
+			return nil
+		}
+		e.cur.regs[in.Dest] = regVal{p: linOfInt(num).scale(new(big.Rat).SetFrac(big.NewInt(1), d))}
+
+	case ir.OpAddString:
+		l, lerr := e.reg(pos, in.Left)
+		r, rerr := e.reg(pos, in.Right)
+		if lerr != nil {
+			return lerr
+		}
+		if rerr != nil {
+			return rerr
+		}
+		e.setStr(in.Dest, l.s.s+r.s.s, l.s.known && r.s.known)
+
+	case ir.OpStrEq:
+		l, err := e.str(pos, in.Left)
+		if err != nil {
+			return err
+		}
+		r, err := e.str(pos, in.Right)
+		if err != nil {
+			return err
+		}
+		e.cur.regs[in.Dest] = regVal{t: smt.Bool(l == r)}
+
+	case ir.OpMonetaryToString:
+		asset, err := e.reg(pos, in.Left)
+		if err != nil {
+			return err
+		}
+		amount, err := e.term(pos, in.Right)
+		if err != nil {
+			return err
+		}
+		n, ok := smt.AsInt(amount)
+		e.setStr(in.Dest, asset.s.s+" "+n.String(), asset.s.known && ok)
+
+	default:
+		return e.unsupported(pos, "not modeled")
+	}
+	return nil
+}
+
+func (e *encoder) unary(pos int, in ir.UnaryOp) error {
+	switch in.Op.(type) {
+	case ir.OpIntCopy, ir.OpBoolCopy, ir.OpNegInt, ir.OpIsZero, ir.OpNot:
+		t, err := e.term(pos, in.Arg)
+		if err != nil {
+			return err
+		}
+		switch in.Op.(type) {
+		case ir.OpNegInt:
+			t = smt.Neg(t)
+		case ir.OpIsZero:
+			t = smt.Eq(t, smt.Int64(0))
+		case ir.OpNot:
+			t = smt.Not(t)
+		}
+		e.setInt(pos, in.Dest, t)
+
+	case ir.OpStrCopy:
+		v, err := e.reg(pos, in.Arg)
+		if err != nil {
+			return err
+		}
+		e.cur.regs[in.Dest] = regVal{s: v.s}
+
+	case ir.OpPortionCopy:
+		p, err := e.portion(pos, in.Arg)
+		if err != nil {
+			return err
+		}
+		e.cur.regs[in.Dest] = regVal{p: p}
+
+	case ir.OpIntToPortion:
+		t, err := e.term(pos, in.Arg)
+		if err != nil {
+			return err
+		}
+		e.cur.regs[in.Dest] = regVal{p: linOfInt(t)}
+
+	case ir.OpPortionToInt:
+		p, err := e.portion(pos, in.Arg)
+		if err != nil {
+			return err
+		}
+		e.setInt(pos, in.Dest, p.toInt())
+
+	case ir.OpIntToString:
+		t, err := e.term(pos, in.Arg)
+		if err != nil {
+			return err
+		}
+		n, ok := smt.AsInt(t)
+		if ok {
+			e.setStr(in.Dest, n.String(), true)
+		} else {
+			e.setStr(in.Dest, "", false)
+		}
+
+	case ir.OpPortionToString:
+		p, err := e.portion(pos, in.Arg)
+		if err != nil {
+			return err
+		}
+		if p.isConst() {
+			e.setStr(in.Dest, p.konst.String(), true)
+		} else {
+			e.setStr(in.Dest, "", false)
+		}
+
+	default:
+		return e.unsupported(pos, "not modeled")
+	}
+	return nil
+}
+
+func (e *encoder) finish(extraKeys []Key, extraMoves []MoveKey) *Problem {
+	fin := e.cur
+	for _, k := range extraKeys {
+		e.keys[k] = struct{}{}
+	}
+	for _, m := range extraMoves {
+		e.moves[m] = struct{}{}
+	}
+
+	e.sc.Blank()
+	e.sc.Comment("outputs: the ledger applies nothing on failure")
+	flags := make([]smt.Term, len(e.fails))
+	for i, s := range e.fails {
+		flags[i] = s.Flag
+	}
+	p := &Problem{
+		body:      e.sc,
+		Keys:      sortedKeys(e.keys),
+		MoveKeys:  sortedMoveKeys(e.moves),
+		Accounts:  sortedStrings(e.accounts),
+		Assets:    sortedStrings(e.assets),
+		Before:    map[Key]smt.Term{},
+		After:     map[Key]smt.Term{},
+		Sent:      map[Key]smt.Term{},
+		Received:  map[Key]smt.Term{},
+		Moved:     map[MoveKey]smt.Term{},
+		FailSites: e.fails,
+	}
+	p.Fails = e.sc.DefineAlways("fails", smt.Or(flags...))
+	p.Success = e.sc.DefineAlways("success", smt.Not(p.Fails))
+	for _, k := range p.Keys {
+		before := smt.Symbol(BeforeName(k), smt.SortInt)
+		p.Before[k] = before
+		sent := e.sc.DefineAlways(SentName(k), smt.Ite(p.Fails, smt.Int64(0), orZero(fin.sent[k])))
+		recv := e.sc.DefineAlways(ReceivedName(k), smt.Ite(p.Fails, smt.Int64(0), orZero(fin.recv[k])))
+		p.Sent[k] = sent
+		p.Received[k] = recv
+		p.After[k] = e.sc.DefineAlways(AfterName(k), smt.Add(before, smt.Sub(recv, sent)))
+	}
+	for _, m := range p.MoveKeys {
+		p.Moved[m] = e.sc.DefineAlways(MovedName(m), smt.Ite(p.Fails, smt.Int64(0), orZero(fin.moved[m])))
+	}
+	return p
+}
diff --git a/internal/prove/encode/encode_test.go b/internal/prove/encode/encode_test.go
new file mode 100644
index 00000000..648e7978
--- /dev/null
+++ b/internal/prove/encode/encode_test.go
@@ -0,0 +1,123 @@
+package encode
+
+import (
+	"context"
+	"math/big"
+	"os"
+	"testing"
+	"time"
+
+	"github.com/formancehq/numscript/internal/compiler"
+	"github.com/formancehq/numscript/internal/ir"
+	"github.com/formancehq/numscript/internal/parser"
+	"github.com/formancehq/numscript/internal/prove/smt"
+	"github.com/gkampitakis/go-snaps/snaps"
+	"github.com/stretchr/testify/require"
+)
+
+func compileIR(t *testing.T, src string) []ir.Instr {
+	t.Helper()
+	parsed := parser.Parse(src)
+	require.Empty(t, parsed.Errors)
+	instrs, _, err := compiler.CompileToIR(parsed.Value, nil)
+	require.NoError(t, err)
+	return instrs
+}
+
+func parseIR(t *testing.T, src string) []ir.Instr {
+	t.Helper()
+	instrs, errs := ir.Parse(src)
+	require.Empty(t, errs)
+	return instrs
+}
+
+func requireZ3(t *testing.T) {
+	t.Helper()
+	if err := (smt.Solver{}).Available(); err != nil {
+		if os.Getenv("NUMSCRIPT_REQUIRE_Z3") != "" {
+			t.Fatal(err)
+		}
+		t.Skip(err)
+	}
+}
+
+const simpleSend = `send [USD/2 10] (
+  source = @src
+  destination = @dest
+)`
+
+func TestSimpleSendText(t *testing.T) {
+	p, err := Encode(compileIR(t, simpleSend), nil, nil)
+	require.NoError(t, err)
+	require.Equal(t, []Key{{"dest", "USD/2"}, {"src", "USD/2"}}, p.Keys)
+	require.Equal(t, []MoveKey{{"src", "dest", "USD/2"}}, p.MoveKeys)
+	require.Equal(t, []string{"dest", "src"}, p.Accounts)
+	require.Equal(t, []string{"USD/2"}, p.Assets)
+	require.Len(t, p.FailSites, 1)
+	require.Equal(t, MissingFunds, p.FailSites[0].Kind)
+	snaps.MatchSnapshot(t, p.Text())
+}
+
+// checkFixed evaluates the model under concrete balances and requires the
+// real VM to agree on everything.
+func checkFixed(t *testing.T, instrs []ir.Instr, before map[Key]*big.Int) Outcome {
+	t.Helper()
+	p, err := Encode(instrs, nil, nil)
+	require.NoError(t, err)
+	model := p.OutcomeFromBalances(before)
+	replay, err := Replay(context.Background(), instrs, before, p.Keys, p.MoveKeys)
+	require.NoError(t, err)
+	require.Empty(t, Compare(model, replay), "model vs vm")
+	return model
+}
+
+func bal(pairs ...any) map[Key]*big.Int {
+	out := map[Key]*big.Int{}
+	for i := 0; i < len(pairs); i += 3 {
+		out[Key{pairs[i].(string), pairs[i+1].(string)}] = big.NewInt(int64(pairs[i+2].(int)))
+	}
+	return out
+}
+
+func TestSimpleSendFixedInputs(t *testing.T) {
+	instrs := compileIR(t, simpleSend)
+	out := checkFixed(t, instrs, bal("src", "USD/2", 25))
+	require.True(t, out.Success)
+	require.Equal(t, "10", out.Sent[Key{"src", "USD/2"}].String())
+	require.Equal(t, "15", out.After[Key{"src", "USD/2"}].String())
+	require.Equal(t, "10", out.After[Key{"dest", "USD/2"}].String())
+
+	out = checkFixed(t, instrs, bal("src", "USD/2", 3))
+	require.False(t, out.Success)
+	require.Equal(t, MissingFunds, out.FailKind)
+	require.Equal(t, "3", out.After[Key{"src", "USD/2"}].String())
+
+	checkFixed(t, instrs, bal("src", "USD/2", -3))
+	checkFixed(t, instrs, bal("src", "USD/2", 10))
+}
+
+func TestSimpleSendWithZ3(t *testing.T) {
+	requireZ3(t)
+	p, err := Encode(compileIR(t, simpleSend), nil, nil)
+	require.NoError(t, err)
+	solver := smt.Solver{Timeout: 5 * time.Second}
+	src, dest := Key{"src", "USD/2"}, Key{"dest", "USD/2"}
+
+	// success => after(src) = before(src) - 10
+	prop := smt.Implies(p.Success, smt.Eq(p.After[src], smt.Sub(p.Before[src], smt.Int64(10))))
+	res, err := solver.CheckSat(context.Background(), p.Text()+"(assert "+smt.Print(smt.Not(prop))+")\n", nil)
+	require.NoError(t, err)
+	require.Equal(t, smt.Unsat, res.Status)
+
+	// after(dest) = before(dest) + 10 has a counterexample: the run fails
+	prop = smt.Eq(p.After[dest], smt.Add(p.Before[dest], smt.Int64(10)))
+	res, err = solver.CheckSat(context.Background(), p.Text()+"(assert "+smt.Print(smt.Not(prop))+")\n", append(p.InputNames(), p.OutputNames()...))
+	require.NoError(t, err)
+	require.Equal(t, smt.Sat, res.Status)
+	before, model, err := p.OutcomeFromValues(res.Values)
+	require.NoError(t, err)
+	require.False(t, model.Success)
+	replay, err := Replay(context.Background(), compileIR(t, simpleSend), before, p.Keys, p.MoveKeys)
+	require.NoError(t, err)
+	require.Empty(t, Compare(model, replay))
+}
diff --git a/internal/prove/encode/funds.go b/internal/prove/encode/funds.go
new file mode 100644
index 00000000..877dbdc4
--- /dev/null
+++ b/internal/prove/encode/funds.go
@@ -0,0 +1,217 @@
+package encode
+
+import (
+	"fmt"
+	"sort"
+
+	"github.com/formancehq/numscript/internal/ir"
+	"github.com/formancehq/numscript/internal/prove/smt"
+)
+
+func (e *encoder) pull(pos int, in ir.PullAccount) error {
+	account, err := e.str(pos, in.Account)
+	if err != nil {
+		return err
+	}
+	asset, err := e.currentAsset(pos)
+	if err != nil {
+		return err
+	}
+	cap, err := e.optTerm(pos, in.Cap)
+	if err != nil {
+		return err
+	}
+	overdraft, err := e.optTerm(pos, in.Overdraft)
+	if err != nil {
+		return err
+	}
+	if cap == nil && overdraft == nil {
+		e.comment(pos)
+		e.fail(pos, UncappedSource, smt.Bool(true))
+		return nil
+	}
+
+	k := Key{account, asset}
+	e.comment(pos)
+	var out smt.Term
+	switch overdraft {
+	case nil:
+		// unbounded: the balance is never read
+		out = smt.Max0(cap)
+	default:
+		bal := e.balanceOf(e.cur, k)
+		available := e.def(fmt.Sprintf("available@%d", pos), smt.Max0(smt.Add(bal, smt.Max0(overdraft))))
+		if cap == nil {
+			out = available
+		} else {
+			out = smt.Ite(smt.Lt(cap, available), smt.Max0(cap), available)
+		}
+	}
+	e.touch(k)
+	e.setInt(pos, in.Dest, out)
+	out = e.cur.regs[in.Dest].t
+	e.cur.slots[pos] = &slot{pos: pos, account: account, amount: out}
+	e.cur.bal[k] = e.def(fmt.Sprintf("bal(%s)@%d", k, pos), smt.Sub(e.balanceOf(e.cur, k), out))
+	return nil
+}
+
+func (e *encoder) send(pos int, in ir.SendToAccount) error {
+	asset, err := e.currentAsset(pos)
+	if err != nil {
+		return err
+	}
+	var dest *string
+	if in.Account != nil {
+		d, err := e.str(pos, *in.Account)
+		if err != nil {
+			return err
+		}
+		dest = &d
+		e.touch(Key{d, asset})
+	}
+	rem, err := e.optTerm(pos, in.Cap)
+	if err != nil {
+		return err
+	}
+
+	e.comment(pos)
+	zero := smt.Int64(0)
+	sentAdd := map[Key]smt.Term{}
+	refundAdd := map[Key]smt.Term{}
+	movedAdd := map[MoveKey]smt.Term{}
+	var received = zero
+	for _, sl := range e.cur.sortedSlots() {
+		if n, ok := smt.AsInt(sl.amount); ok && n.Sign() == 0 {
+			continue
+		}
+		var take smt.Term
+		if rem == nil {
+			take = sl.amount
+			sl.amount = zero
+		} else {
+			take = e.def(fmt.Sprintf("take#%d@%d", sl.pos, pos), smt.Ite(smt.Lt(zero, rem), smt.Min(sl.amount, rem), zero))
+			rem = e.def(fmt.Sprintf("rem#%d@%d", sl.pos, pos), smt.Sub(rem, take))
+			sl.amount = e.def(fmt.Sprintf("slot#%d@%d", sl.pos, pos), smt.Sub(sl.amount, take))
+		}
+		src := Key{sl.account, asset}
+		if dest == nil {
+			refundAdd[src] = smt.Add(orZero(refundAdd[src]), take)
+			continue
+		}
+		e.touch(src)
+		sentAdd[src] = smt.Add(orZero(sentAdd[src]), take)
+		m := MoveKey{sl.account, *dest, asset}
+		e.moves[m] = struct{}{}
+		movedAdd[m] = smt.Add(orZero(movedAdd[m]), take)
+		received = smt.Add(received, take)
+	}
+
+	rset := map[Key]struct{}{}
+	for k := range refundAdd {
+		rset[k] = struct{}{}
+	}
+	for _, k := range sortedKeys(rset) {
+		e.cur.bal[k] = e.def(fmt.Sprintf("bal(%s)@%d", k, pos), smt.Add(e.balanceOf(e.cur, k), refundAdd[k]))
+	}
+	set := map[Key]struct{}{}
+	for k := range sentAdd {
+		set[k] = struct{}{}
+	}
+	for _, k := range sortedKeys(set) {
+		e.cur.sent[k] = e.def(fmt.Sprintf("sent(%s)@%d", k, pos), smt.Add(orZero(e.cur.sent[k]), sentAdd[k]))
+	}
+	mset := map[MoveKey]struct{}{}
+	for m := range movedAdd {
+		mset[m] = struct{}{}
+	}
+	for _, m := range sortedMoveKeys(mset) {
+		e.cur.moved[m] = e.def(fmt.Sprintf("moved(%s)@%d", m, pos), smt.Add(orZero(e.cur.moved[m]), movedAdd[m]))
+	}
+	if dest != nil {
+		dk := Key{*dest, asset}
+		e.cur.recv[dk] = e.def(fmt.Sprintf("received(%s)@%d", dk, pos), smt.Add(orZero(e.cur.recv[dk]), received))
+		e.cur.bal[dk] = e.def(fmt.Sprintf("bal(%s)@%d", dk, pos), smt.Add(e.balanceOf(e.cur, dk), received))
+	}
+	return nil
+}
+
+func (e *encoder) save(pos int, in ir.Save) error {
+	account, err := e.str(pos, in.Account)
+	if err != nil {
+		return err
+	}
+	asset, err := e.str(pos, in.Asset)
+	if err != nil {
+		return err
+	}
+	amount, err := e.optTerm(pos, in.Amount)
+	if err != nil {
+		return err
+	}
+	k := Key{account, asset}
+	e.comment(pos)
+	bal := e.balanceOf(e.cur, k)
+	e.touch(k)
+	if amount == nil {
+		e.cur.bal[k] = e.def(fmt.Sprintf("bal(%s)@%d", k, pos), smt.Min(bal, smt.Int64(0)))
+	} else {
+		e.cur.bal[k] = e.def(fmt.Sprintf("bal(%s)@%d", k, pos), smt.Max0(smt.Sub(bal, amount)))
+	}
+	return nil
+}
+
+func (e *encoder) fetchBalance(pos int, in ir.FetchBalance) error {
+	account, err := e.str(pos, in.Account)
+	if err != nil {
+		return err
+	}
+	asset, err := e.str(pos, in.Asset)
+	if err != nil {
+		return err
+	}
+	k := Key{account, asset}
+	e.touch(k)
+	e.setInt(pos, in.Dest, e.balanceOf(e.cur, k))
+	return nil
+}
+
+func (e *encoder) markEnd(pos int, in ir.MarkEnd) error {
+	if len(e.cur.marks) == 0 {
+		return fmt.Errorf("encode: instruction %d: mark end with no open mark", pos)
+	}
+	f := e.cur.marks[len(e.cur.marks)-1]
+	e.cur.marks = e.cur.marks[:len(e.cur.marks)-1]
+	if !in.Rewind {
+		return nil
+	}
+	asset, err := e.currentAsset(pos)
+	if err != nil {
+		return err
+	}
+	e.comment(pos)
+	for _, sl := range e.cur.sortedSlots() {
+		if n, ok := smt.AsInt(sl.amount); ok && n.Sign() == 0 {
+			continue
+		}
+		// the slot is repaid when the region was opened before its pull
+		cands := make([]int, 0, len(f))
+		for c := range f {
+			if c < sl.pos {
+				cands = append(cands, c)
+			}
+		}
+		sort.Ints(cands)
+		guards := make([]smt.Term, len(cands))
+		for i, c := range cands {
+			guards[i] = f[c]
+		}
+		repay := smt.Or(guards...)
+		if smt.IsFalse(repay) {
+			continue
+		}
+		k := Key{sl.account, asset}
+		e.cur.bal[k] = e.def(fmt.Sprintf("bal(%s)@%d", k, pos), smt.Add(e.balanceOf(e.cur, k), smt.Ite(repay, sl.amount, smt.Int64(0))))
+		sl.amount = e.def(fmt.Sprintf("slot#%d@%d", sl.pos, pos), smt.Ite(repay, smt.Int64(0), sl.amount))
+	}
+	return nil
+}
diff --git a/internal/prove/encode/funds_ir_test.go b/internal/prove/encode/funds_ir_test.go
new file mode 100644
index 00000000..7116a78b
--- /dev/null
+++ b/internal/prove/encode/funds_ir_test.go
@@ -0,0 +1,222 @@
+package encode
+
+import (
+	"fmt"
+	"math/big"
+	"testing"
+
+	"github.com/stretchr/testify/require"
+)
+
+const irPrologue = `
+  $asset = "USD/2"
+  set_current_asset($asset)
+  $zero = 0
+  $src = "src"
+  $dest = "dest"
+  $a = "a"
+  $b = "b"
+  $c = "c"
+`
+
+// Shapes the compiler never emits, as hand-written IR.
+var handIR = map[string]string{
+	"capped send then drain": irPrologue + `
+  $cap = 100
+  $pulled = pull_account(account: $src, cap: $cap, overdraft: $zero)
+  $thirty = 30
+  send_to_account(account: $dest, cap: $thirty)
+  send_to_account(account: $a)
+`,
+	"negative cap": irPrologue + `
+  $cap = -5
+  $pulled = pull_account(account: $src, cap: $cap, overdraft: $zero)
+  send_to_account(account: $dest)
+`,
+	"uncapped overdraft pull": irPrologue + `
+  $od = 20
+  $pulled = pull_account(account: $src, overdraft: $od)
+  send_to_account(account: $dest)
+`,
+	"unbounded pull": irPrologue + `
+  $cap = 100
+  $pulled = pull_account(account: $src, cap: $cap)
+  send_to_account(account: $dest)
+`,
+	"asset switch between pull and send": irPrologue + `
+  $cap = 100
+  $pulled = pull_account(account: $src, cap: $cap, overdraft: $zero)
+  $eur = "EUR/2"
+  set_current_asset($eur)
+  send_to_account(account: $dest)
+`,
+	"undrained queue": irPrologue + `
+  $cap = 100
+  $pulled = pull_account(account: $src, cap: $cap, overdraft: $zero)
+`,
+	"kept then send": irPrologue + `
+  $cap = 100
+  $pulled = pull_account(account: $src, cap: $cap, overdraft: $zero)
+  check_enough_funds($pulled, $cap)
+  $forty = 40
+  send_to_account(cap: $forty)
+  send_to_account(account: $dest)
+`,
+	"save then pull": irPrologue + `
+  $fifty = 50
+  save(account: $src, asset: $asset, amount: $fifty)
+  $cap = 100
+  $pulled = pull_account(account: $src, cap: $cap, overdraft: $zero)
+  check_enough_funds($pulled, $cap)
+  send_to_account(account: $dest)
+`,
+	"save all then pull": irPrologue + `
+  save(account: $src, asset: $asset)
+  $cap = 100
+  $od = 30
+  $pulled = pull_account(account: $src, cap: $cap, overdraft: $od)
+  send_to_account(account: $dest)
+`,
+	"balance read mid script": irPrologue + `
+  $cap = 100
+  $pulled = pull_account(account: $src, cap: $cap, overdraft: $zero)
+  $bal = balance($src, $asset)
+  assert_non_negative_balance($bal, $src)
+  send_to_account(account: $dest, cap: $bal)
+  send_to_account(account: $a)
+`,
+	"portion split": irPrologue + `
+  $cap = 100
+  $pulled = pull_account(account: $src, cap: $cap, overdraft: $zero)
+  $one = 1
+  $three = 3
+  $third = mk_portion($one, $three)
+  $whole = mk_portion($one, $one)
+  $rest = sub_portion($whole, $third)
+  assert_leftover($rest)
+  $pp = int_to_portion($pulled)
+  $prod1 = mul_portion($third, $pp)
+  $share1 = portion_to_int($prod1)
+  $prod2 = mul_portion($rest, $pp)
+  $share2 = portion_to_int($prod2)
+  $total = $share1 + $share2
+  $short = lt_int($total, $pulled)
+  jmp_if_false($short, #allot_end)
+  $share1 += $one
+#allot_end
+  send_to_account(account: $a, cap: $share1)
+  send_to_account(account: $b, cap: $share2)
+`,
+	"division by zero": irPrologue + `
+  $one = 1
+  $p = mk_portion($one, $zero)
+  $cap = 100
+  $pulled = pull_account(account: $src, cap: $cap, overdraft: $zero)
+  send_to_account(account: $dest)
+`,
+	"asset mismatch": irPrologue + `
+  $eur = "EUR/2"
+  assert_same_asset($asset, $eur)
+  $cap = 100
+  $pulled = pull_account(account: $src, cap: $cap, overdraft: $zero)
+  send_to_account(account: $dest)
+`,
+	"oneof": irPrologue + `
+  $cap = 10
+  mark_push()
+  $pa = pull_account(account: $a, cap: $cap, overdraft: $zero)
+  $res = int_copy($pa)
+  $missing = $cap - $pa
+  $done = is_zero($missing)
+  jmp_if_true($done, #end)
+  mark_rewind()
+  mark_push()
+  $pb = pull_account(account: $b, cap: $cap, overdraft: $zero)
+  $res = int_copy($pb)
+#end
+  mark_commit()
+  check_enough_funds($res, $cap)
+  send_to_account(account: $dest)
+`,
+	"rewind after a join": irPrologue + `
+  $cap = 10
+  $five = 5
+  mark_push()
+  $pa = pull_account(account: $a, cap: $cap, overdraft: $zero)
+  $small = lt_int($pa, $five)
+  jmp_if_true($small, #join)
+  mark_rewind()
+  mark_push()
+  $pb = pull_account(account: $b, cap: $cap, overdraft: $zero)
+#join
+  mark_rewind()
+  mark_push()
+  $pc = pull_account(account: $c, cap: $cap, overdraft: $zero)
+  mark_commit()
+  send_to_account(account: $dest)
+`,
+	"two statements": irPrologue + `
+  $cap = 100
+  $pulled = pull_account(account: $src, cap: $cap, overdraft: $zero)
+  check_enough_funds($pulled, $cap)
+  send_to_account(account: $dest)
+  $cap2 = 30
+  $pulled2 = pull_account(account: $dest, cap: $cap2, overdraft: $zero)
+  check_enough_funds($pulled2, $cap2)
+  send_to_account(account: $a)
+`,
+}
+
+var assignments = []map[Key]*big.Int{
+	{},
+	bal("src", "USD/2", 100, "a", "USD/2", 100, "b", "USD/2", 100, "c", "USD/2", 100),
+	bal("src", "USD/2", 3, "a", "USD/2", 4, "b", "USD/2", 12, "c", "USD/2", 1),
+	bal("src", "USD/2", -3, "a", "USD/2", -4, "b", "USD/2", 10, "dest", "USD/2", -7),
+	bal("src", "USD/2", 25, "a", "USD/2", 10, "b", "USD/2", 7, "c", "USD/2", 10, "dest", "USD/2", 5),
+	bal("src", "USD/2", 150, "a", "USD/2", 0, "b", "USD/2", 2),
+	bal("src", "USD/2", 70, "src", "EUR/2", 9, "dest", "EUR/2", 1),
+}
+
+func TestHandIRAgreesWithVM(t *testing.T) {
+	for name, src := range handIR {
+		t.Run(name, func(t *testing.T) {
+			instrs := parseIR(t, src)
+			for i, before := range assignments {
+				t.Run(fmt.Sprint(i), func(t *testing.T) {
+					checkFixed(t, instrs, before)
+				})
+			}
+		})
+	}
+}
+
+func TestHandIRExpectedOutcomes(t *testing.T) {
+	out := checkFixed(t, parseIR(t, handIR["capped send then drain"]), bal("src", "USD/2", 100))
+	require.True(t, out.Success)
+	require.Equal(t, "30", out.Received[Key{"dest", "USD/2"}].String())
+	require.Equal(t, "70", out.Received[Key{"a", "USD/2"}].String())
+
+	out = checkFixed(t, parseIR(t, handIR["kept then send"]), bal("src", "USD/2", 100))
+	require.True(t, out.Success)
+	require.Equal(t, "60", out.Sent[Key{"src", "USD/2"}].String())
+	require.Equal(t, "40", out.After[Key{"src", "USD/2"}].String())
+
+	out = checkFixed(t, parseIR(t, handIR["save then pull"]), bal("src", "USD/2", 120))
+	require.False(t, out.Success)
+	require.Equal(t, MissingFunds, out.FailKind)
+
+	out = checkFixed(t, parseIR(t, handIR["oneof"]), bal("a", "USD/2", 4, "b", "USD/2", 12))
+	require.True(t, out.Success)
+	require.Equal(t, "0", out.Sent[Key{"a", "USD/2"}].String())
+	require.Equal(t, "10", out.Sent[Key{"b", "USD/2"}].String())
+	require.Equal(t, "4", out.After[Key{"a", "USD/2"}].String())
+
+	out = checkFixed(t, parseIR(t, handIR["division by zero"]), bal("src", "USD/2", 100))
+	require.False(t, out.Success)
+	require.Equal(t, DivideByZero, out.FailKind)
+
+	out = checkFixed(t, parseIR(t, handIR["asset switch between pull and send"]), bal("src", "USD/2", 100))
+	require.True(t, out.Success)
+	require.Equal(t, "100", out.After[Key{"src", "USD/2"}].String(), "no USD posting exists, so the ledger never debits USD")
+	require.Equal(t, "100", out.Received[Key{"dest", "EUR/2"}].String())
+}
diff --git a/internal/prove/encode/problem.go b/internal/prove/encode/problem.go
new file mode 100644
index 00000000..38ffdee4
--- /dev/null
+++ b/internal/prove/encode/problem.go
@@ -0,0 +1,245 @@
+// Package encode turns an IR program into an SMT model of its run over every
+// initial balance: free Int inputs for the balances the program can read, one
+// define-fun per state write, and named outputs for the run outcome and the
+// amounts moved per (account, asset) pair.
+package encode
+
+import (
+	"fmt"
+	"math/big"
+	"sort"
+	"strings"
+
+	"github.com/formancehq/numscript/internal/prove/smt"
+)
+
+// Key is a balance slot. Scope and color are "" in v1.
+type Key struct{ Account, Asset string }
+
+// MoveKey is a (source, destination, asset) posting aggregate.
+type MoveKey struct{ From, To, Asset string }
+
+func (k Key) String() string     { return "@" + k.Account + "," + k.Asset }
+func (m MoveKey) String() string { return "@" + m.From + ",@" + m.To + "," + m.Asset }
+
+func BeforeName(k Key) string    { return "before(" + k.String() + ")" }
+func AfterName(k Key) string     { return "after(" + k.String() + ")" }
+func SentName(k Key) string      { return "sent(" + k.String() + ")" }
+func ReceivedName(k Key) string  { return "received(" + k.String() + ")" }
+func MovedName(m MoveKey) string { return "moved(" + m.String() + ")" }
+
+type FailKind int
+
+const (
+	MissingFunds FailKind = iota
+	NegativeAmount
+	NegativeBalance
+	NegativePortion
+	AllotmentSum
+	AssetMismatch
+	InvalidAccount
+	DivideByZero
+	UncappedSource
+)
+
+func (k FailKind) String() string {
+	switch k {
+	case MissingFunds:
+		return "missing funds"
+	case NegativeAmount:
+		return "negative amount"
+	case NegativeBalance:
+		return "negative balance"
+	case NegativePortion:
+		return "negative portion"
+	case AllotmentSum:
+		return "invalid allotment sum"
+	case AssetMismatch:
+		return "asset mismatch"
+	case InvalidAccount:
+		return "invalid account name"
+	case DivideByZero:
+		return "division by zero"
+	case UncappedSource:
+		return "uncapped source"
+	}
+	return "?"
+}
+
+// FailSite is one instruction that can abort the run. Flags of different
+// sites are never true together: each is guarded by the absence of every
+// earlier failure on its path.
+type FailSite struct {
+	Index int
+	Text  string
+	Kind  FailKind
+	Flag  smt.Term
+}
+
+type Problem struct {
+	body     *smt.Script
+	Keys     []Key
+	MoveKeys []MoveKey
+	// Accounts and Assets are the names the program can touch, sorted.
+	Accounts []string
+	Assets   []string
+
+	Before   map[Key]smt.Term
+	After    map[Key]smt.Term
+	Sent     map[Key]smt.Term
+	Received map[Key]smt.Term
+	Moved    map[MoveKey]smt.Term
+	Success  smt.Term
+	Fails    smt.Term
+
+	FailSites []FailSite
+}
+
+// Text is the complete SMT-LIB2 model: header, the before inputs, the body.
+func (p *Problem) Text() string {
+	var sb strings.Builder
+	sb.WriteString(smt.Header)
+	for _, k := range p.Keys {
+		fmt.Fprintf(&sb, "(declare-const %s Int)\n", smt.Quote(BeforeName(k)))
+	}
+	for _, line := range p.body.Lines() {
+		sb.WriteString(line)
+		sb.WriteString("\n")
+	}
+	return sb.String()
+}
+
+// InputNames lists the before symbols, in Keys order.
+func (p *Problem) InputNames() []string {
+	out := make([]string, len(p.Keys))
+	for i, k := range p.Keys {
+		out[i] = BeforeName(k)
+	}
+	return out
+}
+
+// OutputNames lists every named output: outcome flags, fail sites, and the
+// after/sent/received/moved aggregates.
+func (p *Problem) OutputNames() []string {
+	names := []string{"success", "fails"}
+	for _, s := range p.FailSites {
+		if n, ok := smt.SymbolName(s.Flag); ok {
+			names = append(names, n)
+		}
+	}
+	for _, k := range p.Keys {
+		names = append(names, AfterName(k), SentName(k), ReceivedName(k))
+	}
+	for _, m := range p.MoveKeys {
+		names = append(names, MovedName(m))
+	}
+	return names
+}
+
+// Evaluator evaluates the model's terms under concrete initial balances
+// (missing keys are 0).
+func (p *Problem) Evaluator(before map[Key]*big.Int) *smt.Evaluator {
+	inputs := make(map[string]smt.Value, len(p.Keys))
+	for _, k := range p.Keys {
+		v := before[k]
+		if v == nil {
+			v = new(big.Int)
+		}
+		inputs[BeforeName(k)] = smt.IntValue(v)
+	}
+	return smt.NewEvaluator(p.body, inputs)
+}
+
+// UnsupportedError reports an instruction the encoder does not model.
+type UnsupportedError struct {
+	Index  int
+	Text   string
+	Reason string
+}
+
+func (e UnsupportedError) Error() string {
+	return fmt.Sprintf("unsupported instruction %d `%s`: %s", e.Index, e.Text, e.Reason)
+}
+
+func sortedKeys(set map[Key]struct{}) []Key {
+	out := make([]Key, 0, len(set))
+	for k := range set {
+		out = append(out, k)
+	}
+	sort.Slice(out, func(i, j int) bool {
+		if out[i].Account != out[j].Account {
+			return out[i].Account < out[j].Account
+		}
+		return out[i].Asset < out[j].Asset
+	})
+	return out
+}
+
+func sortedMoveKeys(set map[MoveKey]struct{}) []MoveKey {
+	out := make([]MoveKey, 0, len(set))
+	for m := range set {
+		out = append(out, m)
+	}
+	sort.Slice(out, func(i, j int) bool {
+		a, b := out[i], out[j]
+		if a.From != b.From {
+			return a.From < b.From
+		}
+		if a.To != b.To {
+			return a.To < b.To
+		}
+		return a.Asset < b.Asset
+	})
+	return out
+}
+
+func sortedStrings(set map[string]struct{}) []string {
+	out := make([]string, 0, len(set))
+	for s := range set {
+		out = append(out, s)
+	}
+	sort.Strings(out)
+	return out
+}
+
+// AddKeys declares pairs the program never touches, so a property may name
+// them: a free before, after equal to it, and zero movements.
+func (p *Problem) AddKeys(keys []Key, moves []MoveKey) {
+	set := map[Key]struct{}{}
+	for _, k := range p.Keys {
+		set[k] = struct{}{}
+	}
+	added := false
+	for _, k := range keys {
+		if _, ok := set[k]; ok {
+			continue
+		}
+		set[k] = struct{}{}
+		added = true
+		before := smt.Symbol(BeforeName(k), smt.SortInt)
+		p.Before[k] = before
+		p.Sent[k] = p.body.DefineAlways(SentName(k), smt.Int64(0))
+		p.Received[k] = p.body.DefineAlways(ReceivedName(k), smt.Int64(0))
+		p.After[k] = p.body.DefineAlways(AfterName(k), before)
+	}
+	if added {
+		p.Keys = sortedKeys(set)
+	}
+
+	mset := map[MoveKey]struct{}{}
+	for _, m := range p.MoveKeys {
+		mset[m] = struct{}{}
+	}
+	added = false
+	for _, m := range moves {
+		if _, ok := mset[m]; ok {
+			continue
+		}
+		mset[m] = struct{}{}
+		added = true
+		p.Moved[m] = p.body.DefineAlways(MovedName(m), smt.Int64(0))
+	}
+	if added {
+		p.MoveKeys = sortedMoveKeys(mset)
+	}
+}
diff --git a/internal/prove/encode/replay.go b/internal/prove/encode/replay.go
new file mode 100644
index 00000000..8c16c735
--- /dev/null
+++ b/internal/prove/encode/replay.go
@@ -0,0 +1,282 @@
+package encode
+
+import (
+	"context"
+	"errors"
+	"fmt"
+	"math/big"
+	"sort"
+
+	"github.com/formancehq/numscript/internal/funds"
+	"github.com/formancehq/numscript/internal/ir"
+	"github.com/formancehq/numscript/internal/prove/smt"
+	"github.com/formancehq/numscript/internal/vm"
+)
+
+// Outcome is what a run did: the outcome flag and the aggregates, either
+// read off a solver model or computed from a real VM run.
+type Outcome struct {
+	Success bool
+	// FailKind and FailIndex describe the abort. FailIndex is -1 when the
+	// outcome comes from the VM, which does not report positions.
+	FailKind  FailKind
+	FailIndex int
+
+	Sent     map[Key]*big.Int
+	Received map[Key]*big.Int
+	After    map[Key]*big.Int
+	Moved    map[MoveKey]*big.Int
+}
+
+func newOutcome() Outcome {
+	return Outcome{
+		FailIndex: -1,
+		Sent:      map[Key]*big.Int{},
+		Received:  map[Key]*big.Int{},
+		After:     map[Key]*big.Int{},
+		Moved:     map[MoveKey]*big.Int{},
+	}
+}
+
+// OutcomeFromValues reads a solver model: the before inputs and the outcome.
+func (p *Problem) OutcomeFromValues(vals map[string]smt.Value) (map[Key]*big.Int, Outcome, error) {
+	get := func(name string) (smt.Value, error) {
+		v, ok := vals[name]
+		if !ok {
+			return smt.Value{}, fmt.Errorf("encode: the model has no value for %s", name)
+		}
+		return v, nil
+	}
+	before := map[Key]*big.Int{}
+	for _, k := range p.Keys {
+		v, err := get(BeforeName(k))
+		if err != nil {
+			return nil, Outcome{}, err
+		}
+		before[k] = v.Int
+	}
+	return before, p.outcome(func(t smt.Term) (smt.Value, error) {
+		if n, ok := smt.SymbolName(t); ok {
+			return get(n)
+		}
+		if b, ok := smt.AsBool(t); ok {
+			return smt.BoolValue(b), nil
+		}
+		if n, ok := smt.AsInt(t); ok {
+			return smt.IntValue(n), nil
+		}
+		return smt.Value{}, fmt.Errorf("encode: output %s is not a named symbol", smt.Print(t))
+	}), nil
+}
+
+// OutcomeFromBalances evaluates the model under concrete initial balances,
+// without a solver.
+func (p *Problem) OutcomeFromBalances(before map[Key]*big.Int) Outcome {
+	ev := p.Evaluator(before)
+	return p.outcome(ev.Eval)
+}
+
+func (p *Problem) outcome(eval func(smt.Term) (smt.Value, error)) Outcome {
+	must := func(t smt.Term) smt.Value {
+		v, err := eval(t)
+		if err != nil {
+			panic(err)
+		}
+		return v
+	}
+	out := newOutcome()
+	out.Success = must(p.Success).Bool
+	if !out.Success {
+		for _, s := range p.FailSites {
+			if must(s.Flag).Bool {
+				out.FailKind = s.Kind
+				out.FailIndex = s.Index
+				break
+			}
+		}
+	}
+	for _, k := range p.Keys {
+		out.Sent[k] = must(p.Sent[k]).Int
+		out.Received[k] = must(p.Received[k]).Int
+		out.After[k] = must(p.After[k]).Int
+	}
+	for _, m := range p.MoveKeys {
+		out.Moved[m] = must(p.Moved[m]).Int
+	}
+	return out
+}
+
+type staticStore map[funds.PairKey]*big.Int
+
+func (s staticStore) GetBalance(_ context.Context, account, scope, asset, color string) (*big.Int, error) {
+	if v, ok := s[funds.PairKey{Account: account, Scope: scope, Asset: asset, Color: color}]; ok {
+		return new(big.Int).Set(v), nil
+	}
+	return new(big.Int), nil
+}
+
+func (s staticStore) GetMetadata(context.Context, string, string, string) (string, bool, error) {
+	return "", false, nil
+}
+
+// Replay runs instrs on the real VM from the given initial balances and
+// aggregates its postings over keys and moves (plus any pair a posting
+// touches).
+func Replay(ctx context.Context, instrs []ir.Instr, before map[Key]*big.Int, keys []Key, moves []MoveKey) (Outcome, error) {
+	prog, err := ir.Assemble(instrs)
+	if err != nil {
+		return Outcome{}, err
+	}
+	store := staticStore{}
+	for k, v := range before {
+		store[funds.PairKey{Account: k.Account, Asset: k.Asset}] = v
+	}
+
+	out := newOutcome()
+	for _, k := range keys {
+		out.Sent[k] = new(big.Int)
+		out.Received[k] = new(big.Int)
+	}
+	for _, m := range moves {
+		out.Moved[m] = new(big.Int)
+	}
+
+	result, execErr := vm.Exec(ctx, vm.NewVm(prog), nil, store)
+	if execErr != nil {
+		kind, ok := failKindOf(execErr)
+		if !ok {
+			return Outcome{}, fmt.Errorf("encode: replay: %w", execErr)
+		}
+		out.FailKind = kind
+	} else {
+		out.Success = true
+		for _, p := range result.Postings {
+			src, dst := Key{p.Source, p.Asset}, Key{p.Destination, p.Asset}
+			addTo(out.Sent, src, p.Amount)
+			addTo(out.Received, dst, p.Amount)
+			m := MoveKey{p.Source, p.Destination, p.Asset}
+			if out.Moved[m] == nil {
+				out.Moved[m] = new(big.Int)
+			}
+			out.Moved[m].Add(out.Moved[m], p.Amount)
+		}
+	}
+	for k := range out.Sent {
+		if out.Received[k] == nil {
+			out.Received[k] = new(big.Int)
+		}
+	}
+	for k := range out.Received {
+		if out.Sent[k] == nil {
+			out.Sent[k] = new(big.Int)
+		}
+		b := before[k]
+		if b == nil {
+			b = new(big.Int)
+		}
+		out.After[k] = new(big.Int).Add(b, new(big.Int).Sub(out.Received[k], out.Sent[k]))
+	}
+	return out, nil
+}
+
+func addTo(m map[Key]*big.Int, k Key, v *big.Int) {
+	if m[k] == nil {
+		m[k] = new(big.Int)
+	}
+	m[k].Add(m[k], v)
+}
+
+func failKindOf(err error) (FailKind, bool) {
+	var (
+		missing   vm.MissingFundsError
+		negAmount vm.NegativeAmountError
+		negBal    vm.NegativeBalanceError
+		negPor    vm.NegativePortionError
+		allot     vm.InvalidAllotmentSum
+		mismatch  vm.AssetMismatchError
+		account   vm.InvalidAccountName
+		divZero   vm.DivideByZeroError
+		uncapped  vm.InvalidUncappedSource
+	)
+	switch {
+	case errors.As(err, &missing):
+		return MissingFunds, true
+	case errors.As(err, &negAmount):
+		return NegativeAmount, true
+	case errors.As(err, &negBal):
+		return NegativeBalance, true
+	case errors.As(err, &negPor):
+		return NegativePortion, true
+	case errors.As(err, &allot):
+		return AllotmentSum, true
+	case errors.As(err, &mismatch):
+		return AssetMismatch, true
+	case errors.As(err, &account):
+		return InvalidAccount, true
+	case errors.As(err, &divZero):
+		return DivideByZero, true
+	case errors.As(err, &uncapped):
+		return UncappedSource, true
+	}
+	return 0, false
+}
+
+// Compare lists every way model and replay disagree. Pairs missing on one
+// side count as zero.
+func Compare(model, replay Outcome) []string {
+	var diffs []string
+	if model.Success != replay.Success {
+		diffs = append(diffs, fmt.Sprintf("outcome: model %s, vm %s", outcomeWord(model), outcomeWord(replay)))
+		return diffs
+	}
+	if !model.Success && model.FailKind != replay.FailKind {
+		diffs = append(diffs, fmt.Sprintf("failure: model %s, vm %s", model.FailKind, replay.FailKind))
+	}
+	cmpKeyed := func(name string, a, b map[Key]*big.Int) {
+		set := map[Key]struct{}{}
+		for k := range a {
+			set[k] = struct{}{}
+		}
+		for k := range b {
+			set[k] = struct{}{}
+		}
+		for _, k := range sortedKeys(set) {
+			x, y := orZeroInt(a[k]), orZeroInt(b[k])
+			if x.Cmp(y) != 0 {
+				diffs = append(diffs, fmt.Sprintf("%s(%s): model %s, vm %s", name, k, x, y))
+			}
+		}
+	}
+	cmpKeyed("sent", model.Sent, replay.Sent)
+	cmpKeyed("received", model.Received, replay.Received)
+	cmpKeyed("after", model.After, replay.After)
+	mset := map[MoveKey]struct{}{}
+	for m := range model.Moved {
+		mset[m] = struct{}{}
+	}
+	for m := range replay.Moved {
+		mset[m] = struct{}{}
+	}
+	for _, m := range sortedMoveKeys(mset) {
+		x, y := orZeroInt(model.Moved[m]), orZeroInt(replay.Moved[m])
+		if x.Cmp(y) != 0 {
+			diffs = append(diffs, fmt.Sprintf("moved(%s): model %s, vm %s", m, x, y))
+		}
+	}
+	sort.Strings(diffs)
+	return diffs
+}
+
+func outcomeWord(o Outcome) string {
+	if o.Success {
+		return "success"
+	}
+	return "fails (" + o.FailKind.String() + ")"
+}
+
+func orZeroInt(v *big.Int) *big.Int {
+	if v == nil {
+		return new(big.Int)
+	}
+	return v
+}
diff --git a/internal/prove/encode/state.go b/internal/prove/encode/state.go
new file mode 100644
index 00000000..24180390
--- /dev/null
+++ b/internal/prove/encode/state.go
@@ -0,0 +1,318 @@
+package encode
+
+import (
+	"fmt"
+	"sort"
+
+	"github.com/formancehq/numscript/internal/ir"
+	"github.com/formancehq/numscript/internal/prove/smt"
+)
+
+// slot is a queued funding source: the pull that created it, its account, and
+// what is still queued (0 once consumed, rewound, or never pulled on this path).
+type slot struct {
+	pos     int
+	account string
+	amount  smt.Term
+}
+
+// frame is an open mark region: the guard under which each candidate
+// mark_push position is the one this region was opened at. A path through no
+// join has a single candidate guarded by true.
+type frame map[int]smt.Term
+
+type state struct {
+	reach smt.Term
+	alive smt.Term
+	dead  bool
+
+	regs  map[ir.Reg]regVal
+	bal   map[Key]smt.Term
+	slots map[int]*slot
+	sent  map[Key]smt.Term
+	recv  map[Key]smt.Term
+	moved map[MoveKey]smt.Term
+	asset strVal
+	marks []frame
+}
+
+func newState() *state {
+	return &state{
+		reach: smt.Bool(true),
+		alive: smt.Bool(true),
+		regs:  map[ir.Reg]regVal{},
+		bal:   map[Key]smt.Term{},
+		slots: map[int]*slot{},
+		sent:  map[Key]smt.Term{},
+		recv:  map[Key]smt.Term{},
+		moved: map[MoveKey]smt.Term{},
+	}
+}
+
+func deadState() *state {
+	s := newState()
+	s.reach = smt.Bool(false)
+	s.alive = smt.Bool(false)
+	s.dead = true
+	return s
+}
+
+func (s *state) clone() *state {
+	out := &state{
+		reach: s.reach,
+		alive: s.alive,
+		dead:  s.dead,
+		regs:  make(map[ir.Reg]regVal, len(s.regs)),
+		bal:   make(map[Key]smt.Term, len(s.bal)),
+		slots: make(map[int]*slot, len(s.slots)),
+		sent:  make(map[Key]smt.Term, len(s.sent)),
+		recv:  make(map[Key]smt.Term, len(s.recv)),
+		moved: make(map[MoveKey]smt.Term, len(s.moved)),
+		asset: s.asset,
+	}
+	for k, v := range s.regs {
+		out.regs[k] = v
+	}
+	for k, v := range s.bal {
+		out.bal[k] = v
+	}
+	for k, v := range s.slots {
+		c := *v
+		out.slots[k] = &c
+	}
+	for k, v := range s.sent {
+		out.sent[k] = v
+	}
+	for k, v := range s.recv {
+		out.recv[k] = v
+	}
+	for k, v := range s.moved {
+		out.moved[k] = v
+	}
+	for _, f := range s.marks {
+		c := make(frame, len(f))
+		for k, v := range f {
+			c[k] = v
+		}
+		out.marks = append(out.marks, c)
+	}
+	return out
+}
+
+func (s *state) sortedSlots() []*slot {
+	out := make([]*slot, 0, len(s.slots))
+	for _, sl := range s.slots {
+		out = append(out, sl)
+	}
+	sort.Slice(out, func(i, j int) bool { return out[i].pos < out[j].pos })
+	return out
+}
+
+// merge joins the live edges reaching a label into one state. Every value is
+// an ite chain over the edges' reach conditions, named by a define-fun.
+func (e *encoder) merge(pos int, edges []*state) (*state, error) {
+	live := edges[:0]
+	for _, s := range edges {
+		if !s.dead {
+			live = append(live, s)
+		}
+	}
+	switch len(live) {
+	case 0:
+		return deadState(), nil
+	case 1:
+		return live[0], nil
+	}
+
+	out := newState()
+	reach := make([]smt.Term, len(live))
+	alive := make([]smt.Term, len(live))
+	for i, s := range live {
+		reach[i] = s.reach
+		alive[i] = s.alive
+	}
+	out.reach = e.def(fmt.Sprintf("reach@%d", pos), smt.Or(reach...))
+	out.alive = e.def(fmt.Sprintf("alive@%d", pos), smt.Or(alive...))
+
+	// chain builds ite(reach_1, v_1, ite(reach_2, v_2, ... v_n)) over the
+	// edges that have a value; the last one is the default
+	chain := func(vals []smt.Term, guards []smt.Term) smt.Term {
+		t := vals[len(vals)-1]
+		for i := len(vals) - 2; i >= 0; i-- {
+			t = smt.Ite(guards[i], vals[i], t)
+		}
+		return t
+	}
+
+	regSet := map[ir.Reg]struct{}{}
+	for _, s := range live {
+		for r := range s.regs {
+			regSet[r] = struct{}{}
+		}
+	}
+	regs := make([]ir.Reg, 0, len(regSet))
+	for r := range regSet {
+		regs = append(regs, r)
+	}
+	sort.Slice(regs, func(i, j int) bool { return regs[i] < regs[j] })
+	for _, r := range regs {
+		var vals []regVal
+		var guards []smt.Term
+		for i, s := range live {
+			if v, ok := s.regs[r]; ok {
+				vals = append(vals, v)
+				guards = append(guards, reach[i])
+			}
+		}
+		first := vals[0]
+		switch {
+		case first.p != nil:
+			for _, v := range vals[1:] {
+				if v.p.String() != first.p.String() {
+					return nil, e.unsupported(pos, fmt.Sprintf("portion register $r%d takes different values on joining paths", r))
+				}
+			}
+			out.regs[r] = first
+		case first.t == nil:
+			merged := first.s
+			for _, v := range vals[1:] {
+				if !v.s.known || !merged.known || v.s.s != merged.s {
+					if !v.s.known || !merged.known {
+						merged = strVal{}
+						continue
+					}
+					return nil, e.unsupported(pos, fmt.Sprintf("string register $r%d takes different values on joining paths", r))
+				}
+			}
+			out.regs[r] = regVal{s: merged}
+		default:
+			ts := make([]smt.Term, len(vals))
+			for i, v := range vals {
+				ts[i] = v.t
+			}
+			out.regs[r] = regVal{t: e.def(fmt.Sprintf("$r%d@%d", r, pos), chain(ts, guards))}
+		}
+	}
+
+	keySet := map[Key]struct{}{}
+	for _, s := range live {
+		for k := range s.bal {
+			keySet[k] = struct{}{}
+		}
+	}
+	for _, k := range sortedKeys(keySet) {
+		vals := make([]smt.Term, len(live))
+		for i, s := range live {
+			vals[i] = e.balanceOf(s, k)
+		}
+		out.bal[k] = e.def(fmt.Sprintf("bal(%s)@%d", k, pos), chain(vals, reach))
+	}
+
+	slotSet := map[int]struct{}{}
+	for _, s := range live {
+		for p := range s.slots {
+			slotSet[p] = struct{}{}
+		}
+	}
+	slotPos := make([]int, 0, len(slotSet))
+	for p := range slotSet {
+		slotPos = append(slotPos, p)
+	}
+	sort.Ints(slotPos)
+	for _, p := range slotPos {
+		vals := make([]smt.Term, len(live))
+		var account string
+		for i, s := range live {
+			if sl, ok := s.slots[p]; ok {
+				vals[i] = sl.amount
+				account = sl.account
+			} else {
+				vals[i] = smt.Int64(0)
+			}
+		}
+		out.slots[p] = &slot{pos: p, account: account, amount: e.def(fmt.Sprintf("slot#%d@%d", p, pos), chain(vals, reach))}
+	}
+
+	mergeKeyed := func(name string, get func(*state) map[Key]smt.Term, dst map[Key]smt.Term) {
+		set := map[Key]struct{}{}
+		for _, s := range live {
+			for k := range get(s) {
+				set[k] = struct{}{}
+			}
+		}
+		for _, k := range sortedKeys(set) {
+			vals := make([]smt.Term, len(live))
+			for i, s := range live {
+				vals[i] = orZero(get(s)[k])
+			}
+			dst[k] = e.def(fmt.Sprintf("%s(%s)@%d", name, k, pos), chain(vals, reach))
+		}
+	}
+	mergeKeyed("sent", func(s *state) map[Key]smt.Term { return s.sent }, out.sent)
+	mergeKeyed("received", func(s *state) map[Key]smt.Term { return s.recv }, out.recv)
+
+	moveSet := map[MoveKey]struct{}{}
+	for _, s := range live {
+		for m := range s.moved {
+			moveSet[m] = struct{}{}
+		}
+	}
+	for _, m := range sortedMoveKeys(moveSet) {
+		vals := make([]smt.Term, len(live))
+		for i, s := range live {
+			vals[i] = orZero(s.moved[m])
+		}
+		out.moved[m] = e.def(fmt.Sprintf("moved(%s)@%d", m, pos), chain(vals, reach))
+	}
+
+	out.asset = live[0].asset
+	for _, s := range live[1:] {
+		if s.asset != out.asset {
+			if !s.asset.known || !out.asset.known {
+				out.asset = strVal{}
+				continue
+			}
+			return nil, e.unsupported(pos, "the current asset differs on joining paths")
+		}
+	}
+
+	depth := len(live[0].marks)
+	for _, s := range live[1:] {
+		if len(s.marks) != depth {
+			return nil, fmt.Errorf("encode: instruction %d: paths join with different numbers of open marks", pos)
+		}
+	}
+	for d := 0; d < depth; d++ {
+		merged := frame{}
+		cands := map[int]struct{}{}
+		for _, s := range live {
+			for c := range s.marks[d] {
+				cands[c] = struct{}{}
+			}
+		}
+		candList := make([]int, 0, len(cands))
+		for c := range cands {
+			candList = append(candList, c)
+		}
+		sort.Ints(candList)
+		for _, c := range candList {
+			var guards []smt.Term
+			for i, s := range live {
+				if g, ok := s.marks[d][c]; ok {
+					guards = append(guards, smt.And(reach[i], g))
+				}
+			}
+			merged[c] = e.def(fmt.Sprintf("mark#%d@%d", c, pos), smt.Or(guards...))
+		}
+		out.marks = append(out.marks, merged)
+	}
+
+	return out, nil
+}
+
+func orZero(t smt.Term) smt.Term {
+	if t == nil {
+		return smt.Int64(0)
+	}
+	return t
+}
diff --git a/internal/prove/encode/sweep_test.go b/internal/prove/encode/sweep_test.go
new file mode 100644
index 00000000..980c6a28
--- /dev/null
+++ b/internal/prove/encode/sweep_test.go
@@ -0,0 +1,157 @@
+package encode
+
+import (
+	"context"
+	"encoding/json"
+	"errors"
+	"math/big"
+	"math/rand"
+	"path/filepath"
+	"sort"
+	"testing"
+
+	"github.com/formancehq/numscript/internal/compiler"
+	"github.com/formancehq/numscript/internal/gen"
+	"github.com/formancehq/numscript/internal/interpreter"
+	"github.com/formancehq/numscript/internal/parser"
+	"github.com/formancehq/numscript/internal/specs_format"
+	"github.com/stretchr/testify/require"
+)
+
+const scriptsFolder = "../../interpreter/testdata/script-tests"
+
+type coverage struct {
+	encoded int
+	cases   int
+	skipped map[string]int
+}
+
+func (c *coverage) skip(reason string) {
+	if c.skipped == nil {
+		c.skipped = map[string]int{}
+	}
+	c.skipped[reason]++
+}
+
+func (c *coverage) log(t *testing.T, what string) {
+	t.Helper()
+	reasons := make([]string, 0, len(c.skipped))
+	for r := range c.skipped {
+		reasons = append(reasons, r)
+	}
+	sort.Strings(reasons)
+	t.Logf("%s: %d encoded, %d cases checked", what, c.encoded, c.cases)
+	for _, r := range reasons {
+		t.Logf("  skipped %d: %s", c.skipped[r], r)
+	}
+}
+
+func beforeOf(rows interpreter.Balances) (map[Key]*big.Int, bool) {
+	out := map[Key]*big.Int{}
+	for _, row := range rows {
+		if row.Color != "" || row.Scope != "" {
+			return nil, false
+		}
+		amount := row.Amount
+		if amount == nil {
+			amount = new(big.Int)
+		}
+		out[Key{row.Account, row.Asset}] = amount
+	}
+	return out, true
+}
+
+// Every spec script the encoder accepts must agree with the VM on every test
+// case's balances.
+func TestSpecCorpusAgreesWithVM(t *testing.T) {
+	rawSpecs, err := specs_format.ReadSpecsFiles([]string{scriptsFolder})
+	require.NoError(t, err)
+
+	var cov coverage
+	for _, rawSpec := range rawSpecs {
+		rel, err := filepath.Rel(scriptsFolder, rawSpec.NumscriptPath)
+		require.NoError(t, err)
+
+		var specs specs_format.Specs
+		require.NoError(t, json.Unmarshal(rawSpec.SpecsFileContent, &specs))
+
+		parsed := parser.Parse(rawSpec.NumscriptContent)
+		require.Empty(t, parsed.Errors, rel)
+		flags := map[string]struct{}{}
+		for _, f := range specs.FeatureFlags {
+			flags[f] = struct{}{}
+		}
+		instrs, _, err := compiler.CompileToIR(parsed.Value, flags)
+		if err != nil {
+			cov.skip("compile: " + err.Error())
+			continue
+		}
+		p, err := Encode(instrs, nil, nil)
+		var unsupported UnsupportedError
+		if errors.As(err, &unsupported) {
+			cov.skip(unsupported.Reason)
+			continue
+		}
+		require.NoError(t, err, rel)
+		cov.encoded++
+
+		for _, tc := range specs.TestCases {
+			before, ok := beforeOf(specs_format.MergeBalances(specs.Balances, tc.Balances))
+			if !ok {
+				cov.skip("colored or scoped balances")
+				continue
+			}
+			t.Run(rel+"/"+tc.It, func(t *testing.T) {
+				model := p.OutcomeFromBalances(before)
+				replay, err := Replay(context.Background(), instrs, before, p.Keys, p.MoveKeys)
+				require.NoError(t, err)
+				require.Empty(t, Compare(model, replay))
+			})
+			cov.cases++
+		}
+	}
+	cov.log(t, "spec corpus")
+	require.Greater(t, cov.encoded, 40)
+}
+
+// Generated scripts lean on vars and metadata, which v1 rejects; the ones
+// that encode must still agree with the VM.
+func TestGeneratedScriptsAgreeWithVM(t *testing.T) {
+	var cov coverage
+	for seed := int64(0); seed < 200; seed++ {
+		g := gen.Generate(rand.New(rand.NewSource(seed)))
+		parsed := parser.Parse(g.Script)
+		if len(parsed.Errors) != 0 {
+			cov.skip("parse error")
+			continue
+		}
+		flags := map[string]struct{}{}
+		for _, f := range g.Flags {
+			flags[f] = struct{}{}
+		}
+		instrs, _, err := compiler.CompileToIR(parsed.Value, flags)
+		if err != nil {
+			cov.skip("compile error")
+			continue
+		}
+		p, err := Encode(instrs, nil, nil)
+		var unsupported UnsupportedError
+		if errors.As(err, &unsupported) {
+			cov.skip(unsupported.Reason)
+			continue
+		}
+		require.NoError(t, err, "seed %d", seed)
+		cov.encoded++
+
+		before := map[Key]*big.Int{}
+		for k, v := range g.Balances {
+			before[Key{k.Account, k.Asset}] = v
+		}
+		model := p.OutcomeFromBalances(before)
+		replay, err := Replay(context.Background(), instrs, before, p.Keys, p.MoveKeys)
+		require.NoError(t, err, "seed %d", seed)
+		require.Empty(t, Compare(model, replay), "seed %d:\n%s", seed, g.Script)
+		cov.cases++
+	}
+	cov.log(t, "generated scripts")
+}
diff --git a/internal/prove/encode/values.go b/internal/prove/encode/values.go
new file mode 100644
index 00000000..226e2a9c
--- /dev/null
+++ b/internal/prove/encode/values.go
@@ -0,0 +1,159 @@
+package encode
+
+import (
+	"math/big"
+	"sort"
+
+	"github.com/formancehq/numscript/internal/prove/smt"
+)
+
+// strVal is a str register: a constant known at encode time, or not.
+type strVal struct {
+	known bool
+	s     string
+}
+
+// linForm is a portion register as an exact rational linear form over Int
+// terms: sum of coef*term plus konst. It is what keeps portions in QF_LIA.
+type linTerm struct {
+	key string
+	t   smt.Term
+	c   *big.Rat
+}
+
+type linForm struct {
+	terms []linTerm
+	konst *big.Rat
+}
+
+func linConst(r *big.Rat) *linForm {
+	return &linForm{konst: new(big.Rat).Set(r)}
+}
+
+func linOfInt(t smt.Term) *linForm {
+	if n, ok := smt.AsInt(t); ok {
+		return linConst(new(big.Rat).SetInt(n))
+	}
+	return &linForm{
+		terms: []linTerm{{key: smt.Print(t), t: t, c: big.NewRat(1, 1)}},
+		konst: new(big.Rat),
+	}
+}
+
+func (f *linForm) isConst() bool { return len(f.terms) == 0 }
+
+func (f *linForm) clone() *linForm {
+	out := &linForm{konst: new(big.Rat).Set(f.konst)}
+	for _, t := range f.terms {
+		out.terms = append(out.terms, linTerm{t.key, t.t, new(big.Rat).Set(t.c)})
+	}
+	return out
+}
+
+func (f *linForm) scale(r *big.Rat) *linForm {
+	out := &linForm{konst: new(big.Rat).Mul(f.konst, r)}
+	if r.Sign() == 0 {
+		return out
+	}
+	for _, t := range f.terms {
+		out.terms = append(out.terms, linTerm{t.key, t.t, new(big.Rat).Mul(t.c, r)})
+	}
+	return out
+}
+
+func (f *linForm) add(g *linForm) *linForm {
+	out := f.clone()
+	out.konst.Add(out.konst, g.konst)
+	for _, gt := range g.terms {
+		found := false
+		for i := range out.terms {
+			if out.terms[i].key == gt.key {
+				out.terms[i].c.Add(out.terms[i].c, gt.c)
+				found = true
+				break
+			}
+		}
+		if !found {
+			out.terms = append(out.terms, linTerm{gt.key, gt.t, new(big.Rat).Set(gt.c)})
+		}
+	}
+	// drop cancelled terms, keep a deterministic order
+	kept := out.terms[:0]
+	for _, t := range out.terms {
+		if t.c.Sign() != 0 {
+			kept = append(kept, t)
+		}
+	}
+	out.terms = kept
+	sort.Slice(out.terms, func(i, j int) bool { return out.terms[i].key < out.terms[j].key })
+	return out
+}
+
+func (f *linForm) sub(g *linForm) *linForm {
+	return f.add(g.scale(big.NewRat(-1, 1)))
+}
+
+// mul is defined when at least one side is constant.
+func (f *linForm) mul(g *linForm) (*linForm, bool) {
+	switch {
+	case f.isConst():
+		return g.scale(f.konst), true
+	case g.isConst():
+		return f.scale(g.konst), true
+	}
+	return nil, false
+}
+
+// numerator returns the integer-coefficient form D*f and D > 0, the common
+// denominator of every coefficient.
+func (f *linForm) numerator() (smt.Term, *big.Int) {
+	d := new(big.Int).Set(f.konst.Denom())
+	for _, t := range f.terms {
+		d.Mul(d, new(big.Int).Div(t.c.Denom(), new(big.Int).GCD(nil, nil, d, t.c.Denom())))
+	}
+	scale := func(r *big.Rat) *big.Int {
+		n := new(big.Int).Mul(r.Num(), d)
+		return n.Div(n, r.Denom())
+	}
+	sum := smt.Int(scale(f.konst))
+	for _, t := range f.terms {
+		sum = smt.Add(sum, smt.MulConst(scale(t.c), t.t))
+	}
+	return sum, d
+}
+
+// toInt floors the form, like portion_to_int.
+func (f *linForm) toInt() smt.Term {
+	num, d := f.numerator()
+	return smt.DivConst(num, d)
+}
+
+func (f *linForm) sign() smt.Term {
+	num, _ := f.numerator()
+	return num
+}
+
+func (f *linForm) lt(g *linForm) smt.Term {
+	return smt.Lt(f.sub(g).sign(), smt.Int64(0))
+}
+
+func (f *linForm) eq(g *linForm) smt.Term {
+	return smt.Eq(f.sub(g).sign(), smt.Int64(0))
+}
+
+func (f *linForm) String() string {
+	return smt.Print(f.sign()) + "/" + f.denomString()
+}
+
+func (f *linForm) denomString() string {
+	_, d := f.numerator()
+	return d.String()
+}
+
+// regVal is the value of a logical register, in the representation of its
+// bank.
+type regVal struct {
+	t smt.Term // int or bool
+	s strVal
+	p *linForm
+}
diff --git a/internal/prove/prop/ast.go b/internal/prove/prop/ast.go
new file mode 100644
index 00000000..27bed697
--- /dev/null
+++ b/internal/prove/prop/ast.go
@@ -0,0 +1,140 @@
+// Package prop is the property DSL of the prover: a boolean formula over the
+// balances and flows of a script run. It parses, dumps, typechecks, lowers to
+// smt terms and evaluates formulas.
+package prop
+
+import (
+	"fmt"
+	"math/big"
+
+	"github.com/formancehq/numscript/internal/parser"
+)
+
+type Error struct {
+	Range parser.Range
+	Msg   string
+}
+
+func (e Error) Error() string {
+	return fmt.Sprintf("%d:%d: %s", e.Range.Start.Line+1, e.Range.Start.Character+1, e.Msg)
+}
+
+type AtomKind int
+
+const (
+	Before AtomKind = iota
+	After
+	Sent
+	Received
+	Moved
+)
+
+var atomKindNames = [...]string{"before", "after", "sent", "received", "moved"}
+
+func (k AtomKind) String() string { return atomKindNames[k] }
+
+// Atom is a quantity of the run. Accounts are bare names, without the '@';
+// Account2 is set for Moved only.
+type Atom struct {
+	Kind     AtomKind
+	Account  string
+	Account2 string
+	Asset    string
+}
+
+func (a Atom) String() string {
+	if a.Kind == Moved {
+		return fmt.Sprintf("moved(@%s, @%s, %s)", a.Account, a.Account2, a.Asset)
+	}
+	return fmt.Sprintf("%s(@%s, %s)", a.Kind, a.Account, a.Asset)
+}
+
+type Expr interface {
+	GetRange() parser.Range
+	expr()
+}
+
+type UnaryOp int
+
+const (
+	Neg UnaryOp = iota
+	Not
+)
+
+type BinaryOp int
+
+const (
+	Add BinaryOp = iota
+	Sub
+	Mul
+	Div
+	Mod
+	Eq
+	Ne
+	Lt
+	Le
+	Gt
+	Ge
+	And
+	Or
+	Implies
+	Iff
+)
+
+var binaryOpNames = [...]string{"+", "-", "*", "/", "%", "==", "!=", "<", "<=", ">", ">=", "and", "or", "=>", "<=>"}
+
+func (op BinaryOp) String() string { return binaryOpNames[op] }
+
+type (
+	IntLit struct {
+		parser.Range
+		Value *big.Int
+	}
+	BoolLit struct {
+		parser.Range
+		Value bool
+	}
+	Success  struct{ parser.Range }
+	Fails    struct{ parser.Range }
+	AtomExpr struct {
+		parser.Range
+		Atom Atom
+	}
+	Unary struct {
+		parser.Range
+		Op UnaryOp
+		X  Expr
+	}
+	Binary struct {
+		parser.Range
+		Op   BinaryOp
+		L, R Expr
+	}
+	MinMax struct {
+		parser.Range
+		IsMax bool
+		Args  []Expr
+	}
+	// Delta is after - before of the same account and asset.
+	Delta struct {
+		parser.Range
+		Account string
+		Asset   string
+	}
+)
+
+func (*IntLit) expr()   {}
+func (*BoolLit) expr()  {}
+func (*Success) expr()  {}
+func (*Fails) expr()    {}
+func (*AtomExpr) expr() {}
+func (*Unary) expr()    {}
+func (*Binary) expr()   {}
+func (*MinMax) expr()   {}
+func (*Delta) expr()    {}
+
+type Property struct {
+	Name    string
+	Formula Expr
+	Range   parser.Range
+}
diff --git a/internal/prove/prop/dump.go b/internal/prove/prop/dump.go
new file mode 100644
index 00000000..69335247
--- /dev/null
+++ b/internal/prove/prop/dump.go
@@ -0,0 +1,87 @@
+package prop
+
+import (
+	"fmt"
+	"strings"
+)
+
+// Dump renders a formula in the DSL with the fewest parentheses that keep its
+// structure. Parsing the output gives back the same tree.
+func Dump(e Expr) string {
+	var sb strings.Builder
+	dumpTo(&sb, e)
+	return sb.String()
+}
+
+func prec(e Expr) int {
+	switch e := e.(type) {
+	case *Unary:
+		if e.Op == Neg {
+			return precUnary
+		}
+		return precNot
+	case *Binary:
+		return binaryOps[e.Op].prec
+	}
+	return precAtom
+}
+
+func dumpChild(sb *strings.Builder, e Expr, parens bool) {
+	if parens {
+		sb.WriteString("(")
+		dumpTo(sb, e)
+		sb.WriteString(")")
+		return
+	}
+	dumpTo(sb, e)
+}
+
+func dumpTo(sb *strings.Builder, e Expr) {
+	switch e := e.(type) {
+	case *IntLit:
+		sb.WriteString(e.Value.String())
+	case *BoolLit:
+		if e.Value {
+			sb.WriteString("true")
+		} else {
+			sb.WriteString("false")
+		}
+	case *Success:
+		sb.WriteString("success")
+	case *Fails:
+		sb.WriteString("fails")
+	case *AtomExpr:
+		sb.WriteString(e.Atom.String())
+	case *Delta:
+		fmt.Fprintf(sb, "delta(@%s, %s)", e.Account, e.Asset)
+	case *MinMax:
+		if e.IsMax {
+			sb.WriteString("max(")
+		} else {
+			sb.WriteString("min(")
+		}
+		for i, a := range e.Args {
+			if i > 0 {
+				sb.WriteString(", ")
+			}
+			dumpChild(sb, a, prec(a) < precSum)
+		}
+		sb.WriteString(")")
+	case *Unary:
+		if e.Op == Neg {
+			sb.WriteString("-")
+			dumpChild(sb, e.X, prec(e.X) < precUnary)
+		} else {
+			sb.WriteString("not ")
+			dumpChild(sb, e.X, prec(e.X) < precNot)
+		}
+	case *Binary:
+		info := binaryOps[e.Op]
+		lp, rp := prec(e.L), prec(e.R)
+		dumpChild(sb, e.L, lp < info.prec || (lp == info.prec && info.assoc != assocLeft))
+		sb.WriteString(" " + e.Op.String() + " ")
+		dumpChild(sb, e.R, rp < info.prec || (rp == info.prec && info.assoc != assocRight))
+	default:
+		panic(fmt.Sprintf("prop.Dump: unknown node %T", e))
+	}
+}
diff --git a/internal/prove/prop/dump_test.go b/internal/prove/prop/dump_test.go
new file mode 100644
index 00000000..1a701428
--- /dev/null
+++ b/internal/prove/prop/dump_test.go
@@ -0,0 +1,93 @@
+package prop
+
+import (
+	"math/big"
+	"testing"
+
+	"github.com/stretchr/testify/require"
+)
+
+var roundTripFormulas = []string{
+	"success => after(@src, USD/2) == before(@src, USD/2) - 10",
+	"not sent(@a, USD/2) == 0",
+	"not (success and fails)",
+	"(success => fails) => true",
+	"success => fails => true",
+	"(success <=> fails) <=> true",
+	"before(@a, USD/2) - (before(@b, USD/2) - 1) < 3",
+	"before(@a, USD/2) * 2 + 1 % 2 >= -5",
+	"-(before(@a, USD/2) + 1) != --3",
+	"min(1, max(2, 3), delta(@a, EUR/2)) <= moved(@a, @b:001, COIN)",
+	"success and not fails or true and false",
+	"received(@users:001, USD/2) / 2 * 3 == 1000000",
+	"success or fails and (true or false)",
+	"1 - -1 == 2 and not not success",
+}
+
+func TestDumpRoundTrip(t *testing.T) {
+	for _, src := range roundTripFormulas {
+		t.Run(src, func(t *testing.T) {
+			e := mustParse(t, src)
+			require.Equal(t, src, Dump(e))
+			again := mustParse(t, Dump(e))
+			require.True(t, sameExpr(e, again), "reparse of %q differs: %s vs %s", src, tree(e), tree(again))
+		})
+	}
+}
+
+func TestDumpParenthesizes(t *testing.T) {
+	a, b, c := &Success{}, &Fails{}, &BoolLit{Value: true}
+	x := &AtomExpr{Atom: Atom{Kind: Sent, Account: "a", Asset: "USD/2"}}
+	one, two := &IntLit{Value: big.NewInt(1)}, &IntLit{Value: big.NewInt(2)}
+	cases := []struct {
+		e    Expr
+		want string
+	}{
+		{&Binary{Op: And, L: a, R: &Binary{Op: And, L: b, R: c}}, "success and (fails and true)"},
+		{&Binary{Op: And, L: &Binary{Op: And, L: a, R: b}, R: c}, "success and fails and true"},
+		{&Binary{Op: Implies, L: &Binary{Op: Implies, L: a, R: b}, R: c}, "(success => fails) => true"},
+		{&Binary{Op: Implies, L: a, R: &Binary{Op: Implies, L: b, R: c}}, "success => fails => true"},
+		{&Binary{Op: Sub, L: x, R: &Binary{Op: Sub, L: one, R: two}}, "sent(@a, USD/2) - (1 - 2)"},
+		{&Binary{Op: Sub, L: &Binary{Op: Sub, L: x, R: one}, R: two}, "sent(@a, USD/2) - 1 - 2"},
+		{&Unary{Op: Neg, X: &Binary{Op: Mul, L: x, R: two}}, "-(sent(@a, USD/2) * 2)"},
+		{&Binary{Op: Mul, L: &Unary{Op: Neg, X: x}, R: two}, "-sent(@a, USD/2) * 2"},
+		{&Unary{Op: Not, X: &Binary{Op: And, L: a, R: b}}, "not (success and fails)"},
+		{&Unary{Op: Not, X: &Binary{Op: Eq, L: x, R: one}}, "not sent(@a, USD/2) == 1"},
+		{&Binary{Op: And, L: &Unary{Op: Not, X: a}, R: b}, "not success and fails"},
+		{&Binary{Op: Lt, L: &Binary{Op: Add, L: x, R: one}, R: &Unary{Op: Neg, X: two}}, "sent(@a, USD/2) + 1 < -2"},
+		{&MinMax{IsMax: true, Args: []Expr{x, &Binary{Op: Add, L: one, R: two}}}, "max(sent(@a, USD/2), 1 + 2)"},
+		{&Binary{Op: Eq, L: &Delta{Account: "a", Asset: "USD/2"}, R: &IntLit{Value: big.NewInt(-3)}}, "delta(@a, USD/2) == -3"},
+	}
+	for _, c := range cases {
+		t.Run(c.want, func(t *testing.T) {
+			require.Equal(t, c.want, Dump(c.e))
+			require.Equal(t, c.want, Dump(mustParse(t, c.want)))
+		})
+	}
+}
+
+func FuzzParse(f *testing.F) {
+	for _, src := range roundTripFormulas {
+		f.Add(src)
+	}
+	f.Add("name: success")
+	f.Add("$x == [USD/2 100]")
+	f.Add("1 < 2 < 3")
+	f.Add("before(@a:, USD")
+	f.Add("/* unterminated")
+	f.Add("--1 - -1")
+	f.Fuzz(func(t *testing.T, src string) {
+		p, errs := ParseInline(src)
+		if len(errs) > 0 {
+			return
+		}
+		d := Dump(p.Formula)
+		again, errs := ParseInline(d)
+		if len(errs) > 0 {
+			t.Fatalf("Dump of %q gives %q, which does not parse: %v", src, d, errs)
+		}
+		if Dump(again.Formula) != d {
+			t.Fatalf("Dump of %q is %q, reparsed as %q", src, d, Dump(again.Formula))
+		}
+	})
+}
diff --git a/internal/prove/prop/eval.go b/internal/prove/prop/eval.go
new file mode 100644
index 00000000..7da80d75
--- /dev/null
+++ b/internal/prove/prop/eval.go
@@ -0,0 +1,97 @@
+package prop
+
+import (
+	"fmt"
+	"math/big"
+)
+
+// Eval evaluates a typechecked formula. lookup gives the value of an atom.
+// Division and modulo are Euclidean, like big.Int.Div and Mod.
+func Eval(e Expr, lookup func(Atom) *big.Int, success bool) bool {
+	ev := evaluator{lookup: lookup, success: success}
+	return ev.boolean(e)
+}
+
+type evaluator struct {
+	lookup  func(Atom) *big.Int
+	success bool
+}
+
+func (ev evaluator) boolean(e Expr) bool {
+	switch e := e.(type) {
+	case *BoolLit:
+		return e.Value
+	case *Success:
+		return ev.success
+	case *Fails:
+		return !ev.success
+	case *Unary:
+		return !ev.boolean(e.X)
+	case *Binary:
+		switch e.Op {
+		case And:
+			return ev.boolean(e.L) && ev.boolean(e.R)
+		case Or:
+			return ev.boolean(e.L) || ev.boolean(e.R)
+		case Implies:
+			return !ev.boolean(e.L) || ev.boolean(e.R)
+		case Iff:
+			return ev.boolean(e.L) == ev.boolean(e.R)
+		}
+		c := ev.integer(e.L).Cmp(ev.integer(e.R))
+		switch e.Op {
+		case Eq:
+			return c == 0
+		case Ne:
+			return c != 0
+		case Lt:
+			return c < 0
+		case Le:
+			return c <= 0
+		case Gt:
+			return c > 0
+		case Ge:
+			return c >= 0
+		}
+	}
+	panic(fmt.Sprintf("prop.Eval: %T is not a boolean", e))
+}
+
+func (ev evaluator) integer(e Expr) *big.Int {
+	switch e := e.(type) {
+	case *IntLit:
+		return e.Value
+	case *AtomExpr:
+		return ev.lookup(e.Atom)
+	case *Delta:
+		after := ev.lookup(Atom{Kind: After, Account: e.Account, Asset: e.Asset})
+		before := ev.lookup(Atom{Kind: Before, Account: e.Account, Asset: e.Asset})
+		return new(big.Int).Sub(after, before)
+	case *Unary:
+		return new(big.Int).Neg(ev.integer(e.X))
+	case *MinMax:
+		acc := ev.integer(e.Args[0])
+		for _, a := range e.Args[1:] {
+			v := ev.integer(a)
+			if (e.IsMax && v.Cmp(acc) > 0) || (!e.IsMax && v.Cmp(acc) < 0) {
+				acc = v
+			}
+		}
+		return acc
+	case *Binary:
+		l, r := ev.integer(e.L), ev.integer(e.R)
+		switch e.Op {
+		case Add:
+			return new(big.Int).Add(l, r)
+		case Sub:
+			return new(big.Int).Sub(l, r)
+		case Mul:
+			return new(big.Int).Mul(l, r)
+		case Div:
+			return new(big.Int).Div(l, r)
+		case Mod:
+			return new(big.Int).Mod(l, r)
+		}
+	}
+	panic(fmt.Sprintf("prop.Eval: %T is not an integer", e))
+}
diff --git a/internal/prove/prop/eval_test.go b/internal/prove/prop/eval_test.go
new file mode 100644
index 00000000..b534f508
--- /dev/null
+++ b/internal/prove/prop/eval_test.go
@@ -0,0 +1,79 @@
+package prop
+
+import (
+	"math/big"
+	"testing"
+
+	"github.com/stretchr/testify/require"
+)
+
+func TestEval(t *testing.T) {
+	big20, ok := new(big.Int).SetString("100000000000000000000", 10)
+	require.True(t, ok)
+	values := map[string]*big.Int{
+		"before(@a, USD/2)": big.NewInt(10),
+		"after(@a, USD/2)":  big.NewInt(25),
+		"sent(@a, USD/2)":   big.NewInt(5),
+		"big(@a, USD/2)":    big20,
+		"before(@b, USD/2)": big20,
+	}
+	lookup := func(a Atom) *big.Int {
+		v, ok := values[a.String()]
+		if !ok {
+			panic("no value for " + a.String())
+		}
+		return v
+	}
+	cases := []struct {
+		src     string
+		success bool
+		want    bool
+	}{
+		{"-5 / 2 == -3", true, true},
+		{"-5 % 2 == 1", true, true},
+		{"5 / 2 == 2", true, true},
+		{"5 % 2 == 1", true, true},
+		{"-7 / 3 == -3", true, true},
+		{"-7 % 3 == 2", true, true},
+		{"-6 / 3 == -2 and -6 % 3 == 0", true, true},
+		{"min(3, 1, 2) == 1", true, true},
+		{"max(3, 1, 2) == 3", true, true},
+		{"min(-1, 0) == -1 and max(-1, 0) == 0", true, true},
+		{"false => false", true, true},
+		{"false => true", true, true},
+		{"true => true", true, true},
+		{"true => false", true, false},
+		{"fails", true, false},
+		{"fails", false, true},
+		{"fails <=> not success", true, true},
+		{"fails <=> not success", false, true},
+		{"success <=> fails", true, false},
+		{"true and false or true", true, true},
+		{"not 1 == 2", true, true},
+		{"1 != 2 and 1 < 2 and 1 <= 1 and 2 > 1 and 2 >= 2", true, true},
+		{"delta(@a, USD/2) == 15", true, true},
+		{"not sent(@a, USD/2) == 0", true, true},
+		{"before(@b, USD/2) * 2 == 200000000000000000000", true, true},
+		{"before(@b, USD/2) > 9223372036854775807", true, true},
+		{"before(@b, USD/2) / 3 == 33333333333333333333", true, true},
+		{"before(@b, USD/2) % 7 == 100000000000000000000 % 7", true, true},
+		{"-before(@b, USD/2) < -9223372036854775808", true, true},
+		{"after(@a, USD/2) - before(@a, USD/2) == sent(@a, USD/2) * 3", true, true},
+		{"1_000 == 1000", true, true},
+	}
+	for _, c := range cases {
+		t.Run(c.src, func(t *testing.T) {
+			e := mustParse(t, c.src)
+			require.Empty(t, Typecheck(e, Known{}))
+			require.Equal(t, c.want, Eval(e, lookup, c.success))
+		})
+	}
+}
+
+func TestEvalDoesNotMutateLookupValues(t *testing.T) {
+	v := big.NewInt(10)
+	lookup := func(Atom) *big.Int { return v }
+	e := mustParse(t, "-sent(@a, USD/2) + sent(@a, USD/2) * 2 - sent(@a, USD/2) / 3 % 2 == 9")
+	require.True(t, Eval(e, lookup, true))
+	require.Equal(t, int64(10), v.Int64())
+}
diff --git a/internal/prove/prop/helpers_test.go b/internal/prove/prop/helpers_test.go
new file mode 100644
index 00000000..1e270f2f
--- /dev/null
+++ b/internal/prove/prop/helpers_test.go
@@ -0,0 +1,106 @@
+package prop
+
+import (
+	"fmt"
+	"strings"
+	"testing"
+
+	"github.com/stretchr/testify/require"
+)
+
+// tree is the fully parenthesized form of a formula, which exposes its
+// structure regardless of Dump's parenthesization.
+func tree(e Expr) string {
+	switch e := e.(type) {
+	case *IntLit:
+		return e.Value.String()
+	case *BoolLit:
+		return fmt.Sprint(e.Value)
+	case *Success:
+		return "success"
+	case *Fails:
+		return "fails"
+	case *AtomExpr:
+		return e.Atom.String()
+	case *Delta:
+		return fmt.Sprintf("delta(@%s, %s)", e.Account, e.Asset)
+	case *Unary:
+		if e.Op == Neg {
+			return "(- " + tree(e.X) + ")"
+		}
+		return "(not " + tree(e.X) + ")"
+	case *Binary:
+		return "(" + e.Op.String() + " " + tree(e.L) + " " + tree(e.R) + ")"
+	case *MinMax:
+		parts := make([]string, len(e.Args))
+		for i, a := range e.Args {
+			parts[i] = tree(a)
+		}
+		name := "min"
+		if e.IsMax {
+			name = "max"
+		}
+		return "(" + name + " " + strings.Join(parts, " ") + ")"
+	}
+	panic(fmt.Sprintf("tree: unknown node %T", e))
+}
+
+// sameExpr is structural equality ignoring ranges.
+func sameExpr(a, b Expr) bool {
+	switch a := a.(type) {
+	case *IntLit:
+		b, ok := b.(*IntLit)
+		return ok && a.Value.Cmp(b.Value) == 0
+	case *BoolLit:
+		b, ok := b.(*BoolLit)
+		return ok && a.Value == b.Value
+	case *Success:
+		_, ok := b.(*Success)
+		return ok
+	case *Fails:
+		_, ok := b.(*Fails)
+		return ok
+	case *AtomExpr:
+		b, ok := b.(*AtomExpr)
+		return ok && a.Atom == b.Atom
+	case *Delta:
+		b, ok := b.(*Delta)
+		return ok && a.Account == b.Account && a.Asset == b.Asset
+	case *Unary:
+		b, ok := b.(*Unary)
+		return ok && a.Op == b.Op && sameExpr(a.X, b.X)
+	case *Binary:
+		b, ok := b.(*Binary)
+		return ok && a.Op == b.Op && sameExpr(a.L, b.L) && sameExpr(a.R, b.R)
+	case *MinMax:
+		b, ok := b.(*MinMax)
+		if !ok || a.IsMax != b.IsMax || len(a.Args) != len(b.Args) {
+			return false
+		}
+		for i := range a.Args {
+			if !sameExpr(a.Args[i], b.Args[i]) {
+				return false
+			}
+		}
+		return true
+	}
+	return false
+}
+
+func mustParse(t *testing.T, src string) Expr {
+	t.Helper()
+	p, errs := ParseInline(src)
+	require.Empty(t, errs, "parsing %q", src)
+	return p.Formula
+}
+
+func errStrings(errs []Error) []string {
+	if len(errs) == 0 {
+		return nil
+	}
+	out := make([]string, len(errs))
+	for i, e := range errs {
+		out[i] = e.Error()
+	}
+	return out
+}
diff --git a/internal/prove/prop/lexer.go b/internal/prove/prop/lexer.go
new file mode 100644
index 00000000..39cbeb42
--- /dev/null
+++ b/internal/prove/prop/lexer.go
@@ -0,0 +1,265 @@
+package prop
+
+import (
+	"fmt"
+
+	"github.com/formancehq/numscript/internal/parser"
+)
+
+type tokKind int
+
+const (
+	tokEOF tokKind = iota
+	tokInt
+	tokName
+	tokAccount
+	tokAsset
+	tokVar
+	tokString
+	tokLBracket
+	tokLParen
+	tokRParen
+	tokComma
+	tokColon
+	tokPlus
+	tokMinus
+	tokStar
+	tokSlash
+	tokPercent
+	tokEq
+	tokNe
+	tokLt
+	tokLe
+	tokGt
+	tokGe
+	tokImplies
+	tokIff
+	// tokInvalid carries the lexical error in text and ends the token stream.
+	tokInvalid
+)
+
+type token struct {
+	kind tokKind
+	text string
+	rng  parser.Range
+}
+
+type lexer struct {
+	src  []rune
+	pos  int
+	line int
+	col  int
+}
+
+func lex(src string) []token {
+	l := &lexer{src: []rune(src)}
+	var toks []token
+	for {
+		t := l.next()
+		toks = append(toks, t)
+		if t.kind == tokEOF || t.kind == tokInvalid {
+			return toks
+		}
+	}
+}
+
+func (l *lexer) peek() rune { return l.peekAt(0) }
+
+func (l *lexer) peekAt(n int) rune {
+	if l.pos+n >= len(l.src) {
+		return -1
+	}
+	return l.src[l.pos+n]
+}
+
+func (l *lexer) advance() {
+	if l.src[l.pos] == '\n' {
+		l.line++
+		l.col = 0
+	} else {
+		l.col++
+	}
+	l.pos++
+}
+
+func (l *lexer) position() parser.Position {
+	return parser.Position{Line: l.line, Character: l.col}
+}
+
+func (l *lexer) tok(kind tokKind, start parser.Position, startPos int) token {
+	return token{
+		kind: kind,
+		text: string(l.src[startPos:l.pos]),
+		rng:  parser.Range{Start: start, End: l.position()},
+	}
+}
+
+func (l *lexer) invalid(start parser.Position, msg string) token {
+	return token{kind: tokInvalid, text: msg, rng: parser.Range{Start: start, End: l.position()}}
+}
+
+func isDigit(r rune) bool    { return r >= '0' && r <= '9' }
+func isLower(r rune) bool    { return r >= 'a' && r <= 'z' }
+func isUpper(r rune) bool    { return r >= 'A' && r <= 'Z' }
+func isNameChar(r rune) bool { return isLower(r) || isDigit(r) || r == '_' }
+func isAccountChar(r rune) bool {
+	return isLower(r) || isUpper(r) || isDigit(r) || r == '_' || r == '-'
+}
+
+func (l *lexer) skipSpaceAndComments() *token {
+	for {
+		switch {
+		case l.peek() == ' ', l.peek() == '\t', l.peek() == '\r', l.peek() == '\n':
+			l.advance()
+		case l.peek() == '/' && l.peekAt(1) == '/':
+			for l.peek() != -1 && l.peek() != '\n' {
+				l.advance()
+			}
+		case l.peek() == '/' && l.peekAt(1) == '*':
+			start := l.position()
+			l.advance()
+			l.advance()
+			for l.peek() != '*' || l.peekAt(1) != '/' {
+				if l.peek() == -1 {
+					t := l.invalid(start, "unterminated block comment")
+					return &t
+				}
+				l.advance()
+			}
+			l.advance()
+			l.advance()
+		default:
+			return nil
+		}
+	}
+}
+
+func (l *lexer) next() token {
+	if t := l.skipSpaceAndComments(); t != nil {
+		return *t
+	}
+	start := l.position()
+	startPos := l.pos
+	c := l.peek()
+	if c == -1 {
+		return token{kind: tokEOF, rng: parser.Range{Start: start, End: start}}
+	}
+	switch {
+	case c == '@':
+		l.advance()
+		if !isAccountChar(l.peek()) {
+			return l.invalid(start, "expected an account name after '@'")
+		}
+		for {
+			for isAccountChar(l.peek()) {
+				l.advance()
+			}
+			if l.peek() != ':' {
+				break
+			}
+			l.advance()
+			if !isAccountChar(l.peek()) {
+				return l.invalid(start, "expected an account segment after ':'")
+			}
+		}
+		return l.tok(tokAccount, start, startPos)
+	case c == '$':
+		l.advance()
+		for isNameChar(l.peek()) {
+			l.advance()
+		}
+		return l.tok(tokVar, start, startPos)
+	case c == '"':
+		l.advance()
+		for l.peek() != '"' {
+			if l.peek() == -1 {
+				return l.invalid(start, "unterminated string")
+			}
+			l.advance()
+		}
+		l.advance()
+		return l.tok(tokString, start, startPos)
+	case isDigit(c):
+		for isDigit(l.peek()) {
+			l.advance()
+		}
+		for l.peek() == '_' && isDigit(l.peekAt(1)) {
+			l.advance()
+			for isDigit(l.peek()) {
+				l.advance()
+			}
+		}
+		return l.tok(tokInt, start, startPos)
+	case isUpper(c):
+		for isUpper(l.peek()) || isDigit(l.peek()) {
+			l.advance()
+		}
+		if l.peek() == '/' && isDigit(l.peekAt(1)) {
+			l.advance()
+			for isDigit(l.peek()) {
+				l.advance()
+			}
+		}
+		return l.tok(tokAsset, start, startPos)
+	case isLower(c) || c == '_':
+		for isNameChar(l.peek()) {
+			l.advance()
+		}
+		return l.tok(tokName, start, startPos)
+	}
+
+	l.advance()
+	single := func(kind tokKind) token { return l.tok(kind, start, startPos) }
+	double := func(kind tokKind) token {
+		l.advance()
+		return l.tok(kind, start, startPos)
+	}
+	switch c {
+	case '[':
+		return single(tokLBracket)
+	case '(':
+		return single(tokLParen)
+	case ')':
+		return single(tokRParen)
+	case ',':
+		return single(tokComma)
+	case ':':
+		return single(tokColon)
+	case '+':
+		return single(tokPlus)
+	case '-':
+		return single(tokMinus)
+	case '*':
+		return single(tokStar)
+	case '/':
+		return single(tokSlash)
+	case '%':
+		return single(tokPercent)
+	case '<':
+		if l.peek() == '=' && l.peekAt(1) == '>' {
+			l.advance()
+			return double(tokIff)
+		}
+		if l.peek() == '=' {
+			return double(tokLe)
+		}
+		return single(tokLt)
+	case '>':
+		if l.peek() == '=' {
+			return double(tokGe)
+		}
+		return single(tokGt)
+	case '=':
+		if l.peek() == '>' {
+			return double(tokImplies)
+		}
+		if l.peek() == '=' {
+			return double(tokEq)
+		}
+	case '!':
+		if l.peek() == '=' {
+			return double(tokNe)
+		}
+	}
+	return l.invalid(start, fmt.Sprintf("unexpected character '%c'", c))
+}
diff --git a/internal/prove/prop/lower.go b/internal/prove/prop/lower.go
new file mode 100644
index 00000000..d478faa8
--- /dev/null
+++ b/internal/prove/prop/lower.go
@@ -0,0 +1,102 @@
+package prop
+
+import (
+	"fmt"
+
+	"github.com/formancehq/numscript/internal/prove/smt"
+)
+
+// Lower builds the Bool term of a typechecked formula. resolve gives the Int
+// term of an atom; success is the Bool term of the run outcome.
+func Lower(e Expr, resolve func(Atom) smt.Term, success smt.Term) smt.Term {
+	l := lowerer{resolve: resolve, success: success}
+	return l.lower(e)
+}
+
+type lowerer struct {
+	resolve func(Atom) smt.Term
+	success smt.Term
+}
+
+func (l lowerer) lower(e Expr) smt.Term {
+	switch e := e.(type) {
+	case *IntLit:
+		return smt.Int(e.Value)
+	case *BoolLit:
+		return smt.Bool(e.Value)
+	case *Success:
+		return l.success
+	case *Fails:
+		return smt.Not(l.success)
+	case *AtomExpr:
+		return l.resolve(e.Atom)
+	case *Delta:
+		after := l.resolve(Atom{Kind: After, Account: e.Account, Asset: e.Asset})
+		before := l.resolve(Atom{Kind: Before, Account: e.Account, Asset: e.Asset})
+		return smt.Sub(after, before)
+	case *Unary:
+		if e.Op == Neg {
+			return smt.Neg(l.lower(e.X))
+		}
+		return smt.Not(l.lower(e.X))
+	case *MinMax:
+		t := l.lower(e.Args[0])
+		for _, a := range e.Args[1:] {
+			if e.IsMax {
+				t = smt.Max(t, l.lower(a))
+			} else {
+				t = smt.Min(t, l.lower(a))
+			}
+		}
+		return t
+	case *Binary:
+		a, b := l.lower(e.L), l.lower(e.R)
+		switch e.Op {
+		case Add:
+			return smt.Add(a, b)
+		case Sub:
+			return smt.Sub(a, b)
+		case Mul:
+			if c, ok := smt.AsInt(a); ok {
+				return smt.MulConst(c, b)
+			}
+			if c, ok := smt.AsInt(b); ok {
+				return smt.MulConst(c, a)
+			}
+			panic("prop.Lower: multiplication without a literal operand")
+		case Div:
+			d, ok := smt.AsInt(b)
+			if !ok {
+				panic("prop.Lower: division by a non-literal")
+			}
+			return smt.DivConst(a, d)
+		case Mod:
+			d, ok := smt.AsInt(b)
+			if !ok {
+				panic("prop.Lower: modulo by a non-literal")
+			}
+			return smt.ModConst(a, d)
+		case Eq:
+			return smt.Eq(a, b)
+		case Ne:
+			return smt.Ne(a, b)
+		case Lt:
+			return smt.Lt(a, b)
+		case Le:
+			return smt.Le(a, b)
+		case Gt:
+			return smt.Gt(a, b)
+		case Ge:
+			return smt.Ge(a, b)
+		case And:
+			return smt.And(a, b)
+		case Or:
+			return smt.Or(a, b)
+		case Implies:
+			return smt.Implies(a, b)
+		case Iff:
+			return smt.Iff(a, b)
+		}
+	}
+	panic(fmt.Sprintf("prop.Lower: unknown node %T", e))
+}
diff --git a/internal/prove/prop/lower_test.go b/internal/prove/prop/lower_test.go
new file mode 100644
index 00000000..5db8b391
--- /dev/null
+++ b/internal/prove/prop/lower_test.go
@@ -0,0 +1,42 @@
+package prop
+
+import (
+	"fmt"
+	"testing"
+
+	"github.com/formancehq/numscript/internal/prove/smt"
+	"github.com/stretchr/testify/require"
+)
+
+func TestLower(t *testing.T) {
+	resolve := func(a Atom) smt.Term {
+		if a.Kind == Moved {
+			return smt.Symbol(fmt.Sprintf("moved(@%s,@%s,%s)", a.Account, a.Account2, a.Asset), smt.SortInt)
+		}
+		return smt.Symbol(fmt.Sprintf("%s(@%s,%s)", a.Kind, a.Account, a.Asset), smt.SortInt)
+	}
+	success := smt.Symbol("success", smt.SortBool)
+	cases := []struct{ src, want string }{
+		{"success => after(@src, USD/2) == before(@src, USD/2) - 10", "(=> success (= |after(@src,USD/2)| (- |before(@src,USD/2)| 10)))"},
+		{"fails", "(not success)"},
+		{"true", "true"},
+		{"delta(@a, USD/2) >= 0", "(<= 0 (- |after(@a,USD/2)| |before(@a,USD/2)|))"},
+		{"sent(@a, USD/2) * 2 <= 10", "(<= (* 2 |sent(@a,USD/2)|) 10)"},
+		{"2 * 3 * sent(@a, USD/2) == 6", "(= (* 6 |sent(@a,USD/2)|) 6)"},
+		{"before(@a, USD/2) / 2 % 3 == min(1, sent(@a, USD/2))", "(= (mod (div |before(@a,USD/2)| 2) 3) (ite (< 1 |sent(@a,USD/2)|) 1 |sent(@a,USD/2)|))"},
+		{"not success and true", "(not success)"},
+		{"-moved(@a, @b, USD/2) < 0 or fails", "(or (< (- |moved(@a,@b,USD/2)|) 0) (not success))"},
+		{"max(sent(@a, USD/2), 0) != 1", "(not (= (ite (< |sent(@a,USD/2)| 0) 0 |sent(@a,USD/2)|) 1))"},
+		{"received(@a, USD/2) > 1 <=> success", "(= (< 1 |received(@a,USD/2)|) success)"},
+		{"-5 / 2 == -3 and -5 % 2 == 1", "true"},
+		{"sent(@a, USD/2) - 0 == sent(@a, USD/2) * 1", "true"},
+		{"min(sent(@a, USD/2), received(@a, USD/2), 7) == 7", "(= (ite (< (ite (< |sent(@a,USD/2)| |received(@a,USD/2)|) |sent(@a,USD/2)| |received(@a,USD/2)|) 7) (ite (< |sent(@a,USD/2)| |received(@a,USD/2)|) |sent(@a,USD/2)| |received(@a,USD/2)|) 7) 7)"},
+	}
+	for _, c := range cases {
+		t.Run(c.src, func(t *testing.T) {
+			e := mustParse(t, c.src)
+			require.Empty(t, Typecheck(e, Known{}))
+			require.Equal(t, c.want, smt.Print(Lower(e, resolve, success)))
+		})
+	}
+}
diff --git a/internal/prove/prop/parser.go b/internal/prove/prop/parser.go
new file mode 100644
index 00000000..07d98eb7
--- /dev/null
+++ b/internal/prove/prop/parser.go
@@ -0,0 +1,402 @@
+package prop
+
+import (
+	"fmt"
+	"math/big"
+	"strings"
+
+	"github.com/formancehq/numscript/internal/parser"
+)
+
+const (
+	precLowest = iota
+	precIff
+	precImplies
+	precOr
+	precAnd
+	precNot
+	precCmp
+	precSum
+	precTerm
+	precUnary
+	precAtom
+)
+
+type assoc int
+
+const (
+	assocLeft assoc = iota
+	assocRight
+	assocNone
+)
+
+type opInfo struct {
+	op    BinaryOp
+	prec  int
+	assoc assoc
+}
+
+var binaryOps = map[BinaryOp]opInfo{
+	Iff:     {Iff, precIff, assocNone},
+	Implies: {Implies, precImplies, assocRight},
+	Or:      {Or, precOr, assocLeft},
+	And:     {And, precAnd, assocLeft},
+	Eq:      {Eq, precCmp, assocNone},
+	Ne:      {Ne, precCmp, assocNone},
+	Lt:      {Lt, precCmp, assocNone},
+	Le:      {Le, precCmp, assocNone},
+	Gt:      {Gt, precCmp, assocNone},
+	Ge:      {Ge, precCmp, assocNone},
+	Add:     {Add, precSum, assocLeft},
+	Sub:     {Sub, precSum, assocLeft},
+	Mul:     {Mul, precTerm, assocLeft},
+	Div:     {Div, precTerm, assocLeft},
+	Mod:     {Mod, precTerm, assocLeft},
+}
+
+func binaryOp(t token) (opInfo, bool) {
+	var op BinaryOp
+	switch t.kind {
+	case tokIff:
+		op = Iff
+	case tokImplies:
+		op = Implies
+	case tokEq:
+		op = Eq
+	case tokNe:
+		op = Ne
+	case tokLt:
+		op = Lt
+	case tokLe:
+		op = Le
+	case tokGt:
+		op = Gt
+	case tokGe:
+		op = Ge
+	case tokPlus:
+		op = Add
+	case tokMinus:
+		op = Sub
+	case tokStar:
+		op = Mul
+	case tokSlash:
+		op = Div
+	case tokPercent:
+		op = Mod
+	case tokName:
+		switch t.text {
+		case "and":
+			op = And
+		case "or":
+			op = Or
+		default:
+			return opInfo{}, false
+		}
+	default:
+		return opInfo{}, false
+	}
+	return binaryOps[op], true
+}
+
+var reservedNames = map[string]string{
+	"forall":   "quantifiers are not supported yet",
+	"exists":   "quantifiers are not supported yet",
+	"in":       "quantifiers are not supported yet",
+	"accounts": "quantifiers are not supported yet",
+	"assets":   "quantifiers are not supported yet",
+	"sum":      "sums are not supported yet",
+	"meta":     "metadata is not supported yet",
+}
+
+var keywords = map[string]bool{
+	"before": true, "after": true, "sent": true, "received": true, "moved": true, "delta": true,
+	"success": true, "fails": true, "and": true, "or": true, "not": true, "true": true, "false": true,
+	"prop": true, "min": true, "max": true,
+}
+
+type bailout struct{}
+
+type parserState struct {
+	toks []token
+	i    int
+	errs []Error
+}
+
+func newParser(src string) *parserState {
+	return &parserState{toks: lex(src)}
+}
+
+// run executes f, stopping at the first failure.
+func (p *parserState) run(f func()) {
+	defer func() {
+		if r := recover(); r != nil {
+			if _, ok := r.(bailout); !ok {
+				panic(r)
+			}
+		}
+	}()
+	f()
+}
+
+func (p *parserState) fail(rng parser.Range, msg string) {
+	p.errs = append(p.errs, Error{Range: rng, Msg: msg})
+	panic(bailout{})
+}
+
+// cur is the current token; reaching a lexical error reports it.
+func (p *parserState) cur() token {
+	t := p.toks[p.i]
+	if t.kind == tokInvalid {
+		p.fail(t.rng, t.text)
+	}
+	return t
+}
+
+func (p *parserState) peek() token {
+	if p.i+1 < len(p.toks) {
+		return p.toks[p.i+1]
+	}
+	return p.toks[len(p.toks)-1]
+}
+
+func (p *parserState) advance() token {
+	t := p.toks[p.i]
+	if p.i < len(p.toks)-1 {
+		p.i++
+	}
+	return t
+}
+
+func found(t token) string {
+	if t.kind == tokEOF {
+		return "end of input"
+	}
+	return "'" + t.text + "'"
+}
+
+func (p *parserState) expect(kind tokKind, what string) token {
+	t := p.cur()
+	if t.kind != kind {
+		p.fail(t.rng, fmt.Sprintf("expected %s but found %s", what, found(t)))
+	}
+	return p.advance()
+}
+
+func (p *parserState) isName(text string) bool {
+	t := p.cur()
+	return t.kind == tokName && t.text == text
+}
+
+func span(a, b parser.Range) parser.Range {
+	return parser.Range{Start: a.Start, End: b.End}
+}
+
+func ParseFile(src string) ([]Property, []Error) {
+	p := newParser(src)
+	var props []Property
+	seen := map[string]bool{}
+	p.run(func() {
+		for p.cur().kind != tokEOF {
+			kw := p.cur()
+			if !p.isName("prop") {
+				p.fail(kw.rng, "expected 'prop' but found "+found(kw))
+			}
+			p.advance()
+			name := p.expect(tokName, "a property name")
+			p.expect(tokColon, "':'")
+			f := p.parseBinary(precLowest)
+			if seen[name.text] {
+				p.errs = append(p.errs, Error{Range: name.rng, Msg: fmt.Sprintf("property %q is defined twice", name.text)})
+			}
+			seen[name.text] = true
+			props = append(props, Property{Name: name.text, Formula: f, Range: span(kw.rng, f.GetRange())})
+		}
+	})
+	if len(p.errs) == 0 && len(props) == 0 {
+		p.errs = append(p.errs, Error{Msg: "no properties found"})
+	}
+	if len(p.errs) > 0 {
+		return nil, p.errs
+	}
+	return props, nil
+}
+
+func ParseInline(src string) (Property, []Error) {
+	p := newParser(src)
+	var prop Property
+	p.run(func() {
+		var start parser.Range
+		named := false
+		if t := p.cur(); t.kind == tokName && p.peek().kind == tokColon {
+			p.advance()
+			p.advance()
+			prop.Name = t.text
+			start = t.rng
+			named = true
+		}
+		f := p.parseBinary(precLowest)
+		if t := p.cur(); t.kind != tokEOF {
+			p.fail(t.rng, "expected end of input but found "+found(t))
+		}
+		if !named {
+			start = f.GetRange()
+		}
+		prop.Formula = f
+		prop.Range = span(start, f.GetRange())
+	})
+	if len(p.errs) > 0 {
+		return Property{}, p.errs
+	}
+	return prop, nil
+}
+
+func (p *parserState) parseBinary(minPrec int) Expr {
+	l := p.parsePrefix()
+	for {
+		info, ok := binaryOp(p.cur())
+		if !ok || info.prec < minPrec {
+			return l
+		}
+		p.advance()
+		next := info.prec + 1
+		if info.assoc == assocRight {
+			next = info.prec
+		}
+		r := p.parseBinary(next)
+		l = &Binary{Range: span(l.GetRange(), r.GetRange()), Op: info.op, L: l, R: r}
+		if info.assoc == assocNone {
+			if again, ok := binaryOp(p.cur()); ok && again.prec == info.prec {
+				if info.prec == precIff {
+					p.fail(p.cur().rng, "'<=>' does not chain: write (a <=> b) <=> c")
+				}
+				p.fail(p.cur().rng, "comparisons do not chain: write (a < b) and (b < c)")
+			}
+		}
+	}
+}
+
+func (p *parserState) parsePrefix() Expr {
+	t := p.cur()
+	switch {
+	case t.kind == tokMinus:
+		p.advance()
+		x := p.parsePrefix()
+		return &Unary{Range: span(t.rng, x.GetRange()), Op: Neg, X: x}
+	case t.kind == tokName && t.text == "not":
+		p.advance()
+		x := p.parseBinary(precCmp)
+		return &Unary{Range: span(t.rng, x.GetRange()), Op: Not, X: x}
+	}
+	return p.parsePrimary()
+}
+
+func (p *parserState) parsePrimary() Expr {
+	t := p.cur()
+	switch t.kind {
+	case tokInt:
+		p.advance()
+		v, ok := new(big.Int).SetString(strings.ReplaceAll(t.text, "_", ""), 10)
+		if !ok {
+			p.fail(t.rng, "invalid integer "+t.text)
+		}
+		return &IntLit{Range: t.rng, Value: v}
+	case tokLParen:
+		p.advance()
+		e := p.parseBinary(precLowest)
+		p.expect(tokRParen, "')'")
+		return e
+	case tokName:
+		return p.parseName(t)
+	case tokVar:
+		p.fail(t.rng, "script variables are not supported in properties yet")
+	case tokString:
+		p.fail(t.rng, "strings are not supported in properties")
+	case tokLBracket:
+		p.fail(t.rng, "monetary literals are not allowed in properties; amounts are plain integers in the asset's minor unit: write 100")
+	case tokEOF:
+		p.fail(t.rng, "unexpected end of input")
+	}
+	p.fail(t.rng, "expected an expression but found "+found(t))
+	return nil
+}
+
+func (p *parserState) parseName(t token) Expr {
+	switch t.text {
+	case "true", "false":
+		p.advance()
+		return &BoolLit{Range: t.rng, Value: t.text == "true"}
+	case "success":
+		p.advance()
+		return &Success{Range: t.rng}
+	case "fails":
+		p.advance()
+		return &Fails{Range: t.rng}
+	case "before":
+		return p.parseAtomCall(Before)
+	case "after":
+		return p.parseAtomCall(After)
+	case "sent":
+		return p.parseAtomCall(Sent)
+	case "received":
+		return p.parseAtomCall(Received)
+	case "moved":
+		return p.parseAtomCall(Moved)
+	case "delta":
+		p.advance()
+		p.expect(tokLParen, "'('")
+		acc := p.expect(tokAccount, "an account")
+		p.expect(tokComma, "','")
+		asset := p.expect(tokAsset, "an asset")
+		end := p.expect(tokRParen, "')'")
+		return &Delta{Range: span(t.rng, end.rng), Account: acc.text[1:], Asset: asset.text}
+	case "min", "max":
+		return p.parseMinMax(t)
+	}
+	if msg, ok := reservedNames[t.text]; ok {
+		p.fail(t.rng, msg)
+	}
+	if keywords[t.text] {
+		p.fail(t.rng, "expected an expression but found "+found(t))
+	}
+	p.fail(t.rng, fmt.Sprintf("unknown name '%s'", t.text))
+	return nil
+}
+
+func (p *parserState) parseAtomCall(kind AtomKind) Expr {
+	name := p.advance()
+	p.expect(tokLParen, "'('")
+	atom := Atom{Kind: kind}
+	atom.Account = p.expect(tokAccount, "an account").text[1:]
+	p.expect(tokComma, "','")
+	if kind == Moved {
+		atom.Account2 = p.expect(tokAccount, "an account").text[1:]
+		p.expect(tokComma, "','")
+	}
+	atom.Asset = p.expect(tokAsset, "an asset").text
+	end := p.expect(tokRParen, "')'")
+	return &AtomExpr{Range: span(name.rng, end.rng), Atom: atom}
+}
+
+func (p *parserState) parseMinMax(name token) Expr {
+	p.advance()
+	p.expect(tokLParen, "'('")
+	var args []Expr
+	for {
+		args = append(args, p.parseBinary(precSum))
+		t := p.cur()
+		if t.kind == tokComma {
+			p.advance()
+			continue
+		}
+		if t.kind == tokRParen {
+			break
+		}
+		p.fail(t.rng, "expected ',' or ')' but found "+found(t))
+	}
+	end := p.advance()
+	rng := span(name.rng, end.rng)
+	if len(args) < 2 {
+		p.fail(rng, name.text+" takes at least two arguments")
+	}
+	return &MinMax{Range: rng, IsMax: name.text == "max", Args: args}
+}
diff --git a/internal/prove/prop/parser_test.go b/internal/prove/prop/parser_test.go
new file mode 100644
index 00000000..128dd6d5
--- /dev/null
+++ b/internal/prove/prop/parser_test.go
@@ -0,0 +1,144 @@
+package prop
+
+import (
+	"testing"
+
+	"github.com/formancehq/numscript/internal/parser"
+	"github.com/stretchr/testify/require"
+)
+
+func TestParsePrecedence(t *testing.T) {
+	cases := []struct{ src, want string }{
+		{"success or true and false", "(or success (and true false))"},
+		{"not sent(@a, USD/2) == 0", "(not (== sent(@a, USD/2) 0))"},
+		{"success => true => false", "(=> success (=> true false))"},
+		{"(success <=> true) <=> false", "(<=> (<=> success true) false)"},
+		{"success => true <=> false", "(<=> (=> success true) false)"},
+		{"1 + 2 * 3", "(+ 1 (* 2 3))"},
+		{"1 - 2 - 3", "(- (- 1 2) 3)"},
+		{"-1 * 2", "(* (- 1) 2)"},
+		{"success and not fails or true", "(or (and success (not fails)) true)"},
+		{"not not success", "(not (not success))"},
+		{"--1 == 1", "(== (- (- 1)) 1)"},
+		{"1_000_000 == 1000000", "(== 1000000 1000000)"},
+		{"before(@a, USD/2) / 2 % 3 == 0", "(== (% (/ before(@a, USD/2) 2) 3) 0)"},
+		{"min(1, 2, 3) == max(1, 2)", "(== (min 1 2 3) (max 1 2))"},
+		{"not 1 + 2 < 3 and fails", "(and (not (< (+ 1 2) 3)) fails)"},
+		{"1 < 2 and 2 < 3 => success", "(=> (and (< 1 2) (< 2 3)) success)"},
+		{"moved(@a, @b:001, USD/2) == delta(@users:x_1, COIN)", "(== moved(@a, @b:001, USD/2) delta(@users:x_1, COIN))"},
+		{"after(@a-b, USD) != received(@A1, USD/2)", "(!= after(@a-b, USD) received(@A1, USD/2))"},
+		{"1 >= 2 or 3 <= 4 or 5 > 6", "(or (or (>= 1 2) (<= 3 4)) (> 5 6))"},
+		{"before(@a, USD/2) / 2 == 1", "(== (/ before(@a, USD/2) 2) 1)"},
+		{"/* c */ success // trailing\n and fails", "(and success fails)"},
+	}
+	for _, c := range cases {
+		t.Run(c.src, func(t *testing.T) {
+			require.Equal(t, c.want, tree(mustParse(t, c.src)))
+		})
+	}
+}
+
+func TestParseErrors(t *testing.T) {
+	cases := []struct{ src, want string }{
+		{"$x == 0", "1:1: script variables are not supported in properties yet"},
+		{`"a" == 0`, "1:1: strings are not supported in properties"},
+		{"[USD/2 100] == 0", "1:1: monetary literals are not allowed in properties; amounts are plain integers in the asset's minor unit: write 100"},
+		{"forall a in accounts", "1:1: quantifiers are not supported yet"},
+		{"success and exists a", "1:13: quantifiers are not supported yet"},
+		{"sum(1, 2) == 0", "1:1: sums are not supported yet"},
+		{`meta(@a, "k") == 0`, "1:1: metadata is not supported yet"},
+		{"before(@a, USD/2) = 0", "1:19: unexpected character '='"},
+		{"before(@a, USD/2) == 0 and", "1:27: unexpected end of input"},
+		{"(1 + 2", "1:7: expected ')' but found end of input"},
+		{"before(@a USD/2)", "1:11: expected ',' but found 'USD/2'"},
+		{"before(a, USD/2)", "1:8: expected an account but found 'a'"},
+		{"before(@a, usd)", "1:12: expected an asset but found 'usd'"},
+		{"1 2", "1:3: expected end of input but found '2'"},
+		{"/* x", "1:1: unterminated block comment"},
+		{`"abc`, "1:1: unterminated string"},
+		{"@", "1:1: expected an account name after '@'"},
+		{"before(@a:, USD/2)", "1:8: expected an account segment after ':'"},
+		{"min(1)", "1:1: min takes at least two arguments"},
+		{"max(1 < 2, 3)", "1:7: expected ',' or ')' but found '<'"},
+		{"foo", "1:1: unknown name 'foo'"},
+		{"and", "1:1: expected an expression but found 'and'"},
+		{"prop a: success", "1:1: expected an expression but found 'prop'"},
+		{"success\n  and $x", "2:7: script variables are not supported in properties yet"},
+		{"success <=> fails <=> true", "1:19: '<=>' does not chain: write (a <=> b) <=> c"},
+		{"1 < 2 < 3", "1:7: comparisons do not chain: write (a < b) and (b < c)"},
+		{"1 == 2 != 3", "1:8: comparisons do not chain: write (a < b) and (b < c)"},
+		{"success ?", "1:9: unexpected character '?'"},
+		{"x:", "1:3: unexpected end of input"},
+		{"1 +", "1:4: unexpected end of input"},
+		{"", "1:1: unexpected end of input"},
+		{"(success))", "1:10: expected end of input but found ')'"},
+	}
+	for _, c := range cases {
+		t.Run(c.src, func(t *testing.T) {
+			_, errs := ParseInline(c.src)
+			require.Equal(t, []string{c.want}, errStrings(errs))
+		})
+	}
+}
+
+func TestParseInlineName(t *testing.T) {
+	p, errs := ParseInline("safe: success")
+	require.Empty(t, errs)
+	require.Equal(t, "safe", p.Name)
+	require.Equal(t, "success", Dump(p.Formula))
+	require.Equal(t, parser.Range{Start: parser.Position{}, End: parser.Position{Character: 13}}, p.Range)
+
+	p, errs = ParseInline("success => fails")
+	require.Empty(t, errs)
+	require.Equal(t, "", p.Name)
+	require.Equal(t, parser.Range{Start: parser.Position{}, End: parser.Position{Character: 16}}, p.Range)
+	require.Equal(t, p.Range, p.Formula.GetRange())
+}
+
+func TestParseFile(t *testing.T) {
+	src := `// safety
+prop conserve: // trailing
+  success => after(@src, USD/2) == before(@src, USD/2) - 10
+/* block
+   comment */
+prop fee_bound: sent(@src, USD/2) <= 100 and received(@fees, USD/2) >= 0`
+	props, errs := ParseFile(src)
+	require.Empty(t, errs)
+	require.Len(t, props, 2)
+	require.Equal(t, "conserve", props[0].Name)
+	require.Equal(t, "success => after(@src, USD/2) == before(@src, USD/2) - 10", Dump(props[0].Formula))
+	require.Equal(t, parser.Position{Line: 1}, props[0].Range.Start)
+	require.Equal(t, parser.Position{Line: 2, Character: 59}, props[0].Range.End)
+	require.Equal(t, "fee_bound", props[1].Name)
+	require.Equal(t, "sent(@src, USD/2) <= 100 and received(@fees, USD/2) >= 0", Dump(props[1].Formula))
+	require.Equal(t, parser.Position{Line: 5}, props[1].Range.Start)
+}
+
+func TestParseFileErrors(t *testing.T) {
+	cases := []struct {
+		src  string
+		want []string
+	}{
+		{"", []string{"1:1: no properties found"}},
+		{"// just a comment\n", []string{"1:1: no properties found"}},
+		{"prop a: success\nprop a: fails", []string{`2:6: property "a" is defined twice`}},
+		{"prop a: success\nprop b: fails\nprop a: true\nprop b: false", []string{`3:6: property "a" is defined twice`, `4:6: property "b" is defined twice`}},
+		{"success", []string{"1:1: expected 'prop' but found 'success'"}},
+		{"prop a: success fails", []string{"1:17: expected 'prop' but found 'fails'"}},
+		{"prop : success", []string{"1:6: expected a property name but found ':'"}},
+		{"prop a success", []string{"1:8: expected ':' but found 'success'"}},
+		{"prop a:", []string{"1:8: unexpected end of input"}},
+	}
+	for _, c := range cases {
+		t.Run(c.src, func(t *testing.T) {
+			props, errs := ParseFile(c.src)
+			require.Nil(t, props)
+			require.Equal(t, c.want, errStrings(errs))
+		})
+	}
+}
+
+func TestErrorFormat(t *testing.T) {
+	e := Error{Range: parser.Range{Start: parser.Position{Line: 2, Character: 4}}, Msg: "boom"}
+	require.Equal(t, "3:5: boom", e.Error())
+}
diff --git a/internal/prove/prop/typecheck.go b/internal/prove/prop/typecheck.go
new file mode 100644
index 00000000..30acbf4d
--- /dev/null
+++ b/internal/prove/prop/typecheck.go
@@ -0,0 +1,244 @@
+package prop
+
+import (
+	"fmt"
+	"math/big"
+	"sort"
+	"strings"
+)
+
+// Known is the set of accounts (bare names) and assets a script references.
+// A nil map disables that check.
+type Known struct {
+	Accounts map[string]struct{}
+	Assets   map[string]struct{}
+}
+
+type sort_ int
+
+const (
+	sortInt sort_ = iota
+	sortBool
+)
+
+type checker struct {
+	known Known
+	errs  []Error
+}
+
+// Typecheck reports every type error of a formula, which must be boolean.
+func Typecheck(e Expr, known Known) []Error {
+	c := &checker{known: known}
+	c.want(e, sortBool)
+	return c.errs
+}
+
+func (c *checker) err(e Expr, msg string) {
+	c.errs = append(c.errs, Error{Range: e.GetRange(), Msg: msg})
+}
+
+func (c *checker) want(e Expr, s sort_) {
+	if c.infer(e) == s {
+		return
+	}
+	if s == sortInt {
+		c.err(e, "expected an integer expression, found a boolean")
+	} else {
+		c.err(e, "expected a boolean expression, found an integer")
+	}
+}
+
+func (c *checker) infer(e Expr) sort_ {
+	switch e := e.(type) {
+	case *IntLit:
+		return sortInt
+	case *BoolLit, *Success, *Fails:
+		return sortBool
+	case *AtomExpr:
+		c.checkAccount(e, e.Atom.Account)
+		if e.Atom.Kind == Moved {
+			c.checkAccount(e, e.Atom.Account2)
+		}
+		c.checkAsset(e, e.Atom.Asset)
+		return sortInt
+	case *Delta:
+		c.checkAccount(e, e.Account)
+		c.checkAsset(e, e.Asset)
+		return sortInt
+	case *Unary:
+		if e.Op == Neg {
+			c.want(e.X, sortInt)
+			return sortInt
+		}
+		c.want(e.X, sortBool)
+		return sortBool
+	case *Binary:
+		switch e.Op {
+		case Add, Sub:
+			c.want(e.L, sortInt)
+			c.want(e.R, sortInt)
+			return sortInt
+		case Mul:
+			c.want(e.L, sortInt)
+			c.want(e.R, sortInt)
+			_, lok := constInt(e.L)
+			_, rok := constInt(e.R)
+			if !lok && !rok {
+				c.err(e, "multiplication must have a literal operand (linear arithmetic only)")
+			}
+			return sortInt
+		case Div, Mod:
+			c.want(e.L, sortInt)
+			c.want(e.R, sortInt)
+			if d, ok := constInt(e.R); !ok || d.Sign() <= 0 {
+				if e.Op == Div {
+					c.err(e.R, "division must be by a positive literal")
+				} else {
+					c.err(e.R, "modulo must be by a positive literal")
+				}
+			}
+			return sortInt
+		case Eq, Ne, Lt, Le, Gt, Ge:
+			c.want(e.L, sortInt)
+			c.want(e.R, sortInt)
+			return sortBool
+		default:
+			c.want(e.L, sortBool)
+			c.want(e.R, sortBool)
+			return sortBool
+		}
+	case *MinMax:
+		for _, a := range e.Args {
+			c.want(a, sortInt)
+		}
+		return sortInt
+	}
+	panic(fmt.Sprintf("prop.Typecheck: unknown node %T", e))
+}
+
+func (c *checker) checkAccount(e Expr, account string) {
+	if c.known.Accounts == nil {
+		return
+	}
+	if _, ok := c.known.Accounts[account]; ok {
+		return
+	}
+	names := make([]string, 0, len(c.known.Accounts))
+	for a := range c.known.Accounts {
+		names = append(names, "@"+a)
+	}
+	c.err(e, fmt.Sprintf("account @%s is not referenced by the script (known: %s)", account, knownList(names)))
+}
+
+func (c *checker) checkAsset(e Expr, asset string) {
+	if c.known.Assets == nil {
+		return
+	}
+	if _, ok := c.known.Assets[asset]; ok {
+		return
+	}
+	names := make([]string, 0, len(c.known.Assets))
+	for a := range c.known.Assets {
+		names = append(names, a)
+	}
+	c.err(e, fmt.Sprintf("asset %s is not referenced by the script (known: %s)", asset, knownList(names)))
+}
+
+func knownList(names []string) string {
+	if len(names) == 0 {
+		return "none"
+	}
+	sort.Strings(names)
+	return strings.Join(names, ", ")
+}
+
+// constInt is the value of an atom-free integer expression. A division by a
+// non-positive constant has no value.
+func constInt(e Expr) (*big.Int, bool) {
+	switch e := e.(type) {
+	case *IntLit:
+		return e.Value, true
+	case *Unary:
+		if e.Op != Neg {
+			return nil, false
+		}
+		x, ok := constInt(e.X)
+		if !ok {
+			return nil, false
+		}
+		return new(big.Int).Neg(x), true
+	case *Binary:
+		l, ok := constInt(e.L)
+		if !ok {
+			return nil, false
+		}
+		r, ok := constInt(e.R)
+		if !ok {
+			return nil, false
+		}
+		switch e.Op {
+		case Add:
+			return new(big.Int).Add(l, r), true
+		case Sub:
+			return new(big.Int).Sub(l, r), true
+		case Mul:
+			return new(big.Int).Mul(l, r), true
+		case Div:
+			if r.Sign() <= 0 {
+				return nil, false
+			}
+			return new(big.Int).Div(l, r), true
+		case Mod:
+			if r.Sign() <= 0 {
+				return nil, false
+			}
+			return new(big.Int).Mod(l, r), true
+		}
+		return nil, false
+	case *MinMax:
+		var acc *big.Int
+		for _, a := range e.Args {
+			v, ok := constInt(a)
+			if !ok {
+				return nil, false
+			}
+			if acc == nil || (e.IsMax && v.Cmp(acc) > 0) || (!e.IsMax && v.Cmp(acc) < 0) {
+				acc = v
+			}
+		}
+		return acc, true
+	}
+	return nil, false
+}
+
+// Atoms lists the distinct atoms of a formula, sorted by their text. A delta
+// contributes its Before and After atoms.
+func Atoms(e Expr) []Atom {
+	set := map[Atom]struct{}{}
+	var walk func(Expr)
+	walk = func(e Expr) {
+		switch e := e.(type) {
+		case *AtomExpr:
+			set[e.Atom] = struct{}{}
+		case *Delta:
+			set[Atom{Kind: Before, Account: e.Account, Asset: e.Asset}] = struct{}{}
+			set[Atom{Kind: After, Account: e.Account, Asset: e.Asset}] = struct{}{}
+		case *Unary:
+			walk(e.X)
+		case *Binary:
+			walk(e.L)
+			walk(e.R)
+		case *MinMax:
+			for _, a := range e.Args {
+				walk(a)
+			}
+		}
+	}
+	walk(e)
+	out := make([]Atom, 0, len(set))
+	for a := range set {
+		out = append(out, a)
+	}
+	sort.Slice(out, func(i, j int) bool { return out[i].String() < out[j].String() })
+	return out
+}
diff --git a/internal/prove/prop/typecheck_test.go b/internal/prove/prop/typecheck_test.go
new file mode 100644
index 00000000..0d9f5ea0
--- /dev/null
+++ b/internal/prove/prop/typecheck_test.go
@@ -0,0 +1,105 @@
+package prop
+
+import (
+	"testing"
+
+	"github.com/stretchr/testify/require"
+)
+
+func TestTypecheckErrors(t *testing.T) {
+	cases := []struct {
+		src  string
+		want []string
+	}{
+		{"success", nil},
+		{"sent(@a, USD/2) * 2 + 1 % 2 >= -5", nil},
+		{"2 * 3 * sent(@a, USD/2) == 0", nil},
+		{"sent(@a, USD/2) * (10 - 3) == 0", nil},
+		{"sent(@a, USD/2) % (1 + 1) == 0", nil},
+		{"sent(@a, USD/2) / min(2, 3) == 0", nil},
+		{"success + 1", []string{
+			"1:1: expected an integer expression, found a boolean",
+			"1:1: expected a boolean expression, found an integer",
+		}},
+		{"1 and success", []string{"1:1: expected a boolean expression, found an integer"}},
+		{"not 1", []string{"1:5: expected a boolean expression, found an integer"}},
+		{"min(1, success) == 1", []string{"1:8: expected an integer expression, found a boolean"}},
+		{"-success == 1", []string{"1:2: expected an integer expression, found a boolean"}},
+		{"success == true", []string{
+			"1:1: expected an integer expression, found a boolean",
+			"1:12: expected an integer expression, found a boolean",
+		}},
+		{"1", []string{"1:1: expected a boolean expression, found an integer"}},
+		{"before(@a, USD/2) * sent(@a, USD/2) == 0", []string{"1:1: multiplication must have a literal operand (linear arithmetic only)"}},
+		{"sent(@a, USD/2) / 0 == 0", []string{"1:19: division must be by a positive literal"}},
+		{"sent(@a, USD/2) / -2 == 0", []string{"1:19: division must be by a positive literal"}},
+		{"sent(@a, USD/2) / sent(@b, USD/2) == 0", []string{"1:19: division must be by a positive literal"}},
+		{"sent(@a, USD/2) % 0 == 0", []string{"1:19: modulo must be by a positive literal"}},
+		{"(1 / 0) * sent(@a, USD/2) == 0", []string{
+			"1:6: division must be by a positive literal",
+			"1:2: multiplication must have a literal operand (linear arithmetic only)",
+		}},
+		{"success and 1 or 2", []string{
+			"1:13: expected a boolean expression, found an integer",
+			"1:18: expected a boolean expression, found an integer",
+		}},
+	}
+	for _, c := range cases {
+		t.Run(c.src, func(t *testing.T) {
+			errs := Typecheck(mustParse(t, c.src), Known{})
+			require.Equal(t, c.want, errStrings(errs))
+		})
+	}
+}
+
+func TestTypecheckKnown(t *testing.T) {
+	known := Known{
+		Accounts: map[string]struct{}{"src": {}, "dest": {}, "world": {}},
+		Assets:   map[string]struct{}{"USD/2": {}},
+	}
+	cases := []struct {
+		src  string
+		want []string
+	}{
+		{"before(@src, USD/2) == 0", nil},
+		{"moved(@src, @dest, USD/2) == delta(@world, USD/2)", nil},
+		{"before(@dset, USD/2) == 0", []string{"1:1: account @dset is not referenced by the script (known: @dest, @src, @world)"}},
+		{"before(@src, EUR/2) == 0", []string{"1:1: asset EUR/2 is not referenced by the script (known: USD/2)"}},
+		{"moved(@src, @nope, USD/2) == 0", []string{"1:1: account @nope is not referenced by the script (known: @dest, @src, @world)"}},
+		{"0 == delta(@x, EUR/2)", []string{
+			"1:6: account @x is not referenced by the script (known: @dest, @src, @world)",
+			"1:6: asset EUR/2 is not referenced by the script (known: USD/2)",
+		}},
+	}
+	for _, c := range cases {
+		t.Run(c.src, func(t *testing.T) {
+			errs := Typecheck(mustParse(t, c.src), known)
+			require.Equal(t, c.want, errStrings(errs))
+		})
+	}
+
+	e := mustParse(t, "before(@nobody, XYZ) == 0")
+	require.Empty(t, Typecheck(e, Known{}))
+	require.Equal(t, []string{
+		"1:1: account @nobody is not referenced by the script (known: none)",
+		"1:1: asset XYZ is not referenced by the script (known: none)",
+	}, errStrings(Typecheck(e, Known{Accounts: map[string]struct{}{}, Assets: map[string]struct{}{}})))
+}
+
+func TestAtoms(t *testing.T) {
+	e := mustParse(t, "delta(@b, USD/2) + sent(@a, USD/2) == moved(@a, @b, USD/2) + sent(@a, USD/2) - min(received(@a, EUR/2), 1)")
+	require.Equal(t, []Atom{
+		{Kind: After, Account: "b", Asset: "USD/2"},
+		{Kind: Before, Account: "b", Asset: "USD/2"},
+		{Kind: Moved, Account: "a", Account2: "b", Asset: "USD/2"},
+		{Kind: Received, Account: "a", Asset: "EUR/2"},
+		{Kind: Sent, Account: "a", Asset: "USD/2"},
+	}, Atoms(e))
+	require.Empty(t, Atoms(mustParse(t, "success")))
+}
+
+func TestAtomString(t *testing.T) {
+	require.Equal(t, "before(@src, USD/2)", Atom{Kind: Before, Account: "src", Asset: "USD/2"}.String())
+	require.Equal(t, "moved(@a, @b, USD/2)", Atom{Kind: Moved, Account: "a", Account2: "b", Asset: "USD/2"}.String())
+	require.Equal(t, "received", Received.String())
+}
diff --git a/internal/prove/prove.go b/internal/prove/prove.go
new file mode 100644
index 00000000..17e2be67
--- /dev/null
+++ b/internal/prove/prove.go
@@ -0,0 +1,207 @@
+// Package prove checks properties of an IR program for every initial balance:
+// the program is encoded into SMT, each property's negation is asserted, and
+// a model (if any) is replayed on the real VM before being reported as a
+// counterexample.
+package prove
+
+import (
+	"context"
+	"fmt"
+	"math/big"
+	"sort"
+	"strings"
+	"time"
+
+	"github.com/formancehq/numscript/internal/ir"
+	"github.com/formancehq/numscript/internal/prove/encode"
+	"github.com/formancehq/numscript/internal/prove/prop"
+	"github.com/formancehq/numscript/internal/prove/smt"
+)
+
+type Options struct {
+	Solver smt.Solver
+}
+
+// PropertyError is a property that does not parse or typecheck.
+type PropertyError struct {
+	Property prop.Property
+	Errors   []prop.Error
+}
+
+func (e PropertyError) Error() string {
+	msgs := make([]string, len(e.Errors))
+	for i, err := range e.Errors {
+		msgs[i] = err.Error()
+	}
+	return fmt.Sprintf("property %q: %s", e.Property.Name, strings.Join(msgs, "; "))
+}
+
+// Check encodes instrs once and checks every property against it.
+func Check(ctx context.Context, instrs []ir.Instr, props []prop.Property, opts Options) (*Report, error) {
+	p, err := encode.Encode(instrs, nil, nil)
+	if err != nil {
+		return nil, err
+	}
+	known := prop.Known{Accounts: map[string]struct{}{}, Assets: map[string]struct{}{}}
+	for _, a := range p.Accounts {
+		known.Accounts[a] = struct{}{}
+	}
+	for _, a := range p.Assets {
+		known.Assets[a] = struct{}{}
+	}
+
+	var extraKeys []encode.Key
+	var extraMoves []encode.MoveKey
+	for _, pr := range props {
+		if errs := prop.Typecheck(pr.Formula, known); len(errs) != 0 {
+			return nil, PropertyError{Property: pr, Errors: errs}
+		}
+		for _, a := range prop.Atoms(pr.Formula) {
+			if a.Kind == prop.Moved {
+				extraMoves = append(extraMoves, encode.MoveKey{From: a.Account, To: a.Account2, Asset: a.Asset})
+			} else {
+				extraKeys = append(extraKeys, encode.Key{Account: a.Account, Asset: a.Asset})
+			}
+		}
+	}
+	p.AddKeys(extraKeys, extraMoves)
+
+	report := &Report{Problem: p}
+	report.SuccessReachable = reachable(ctx, p, p.Success, opts.Solver)
+	report.FailureReachable = reachable(ctx, p, p.Fails, opts.Solver)
+	for _, pr := range props {
+		report.Results = append(report.Results, checkOne(ctx, instrs, p, pr, opts.Solver))
+	}
+	return report, nil
+}
+
+func reachable(ctx context.Context, p *encode.Problem, flag smt.Term, solver smt.Solver) *bool {
+	res, err := solver.CheckSat(ctx, p.Text()+"(assert "+smt.Print(flag)+")\n", nil)
+	if err != nil || res.Status == smt.Unknown {
+		return nil
+	}
+	v := res.Status == smt.Sat
+	return &v
+}
+
+func resolver(p *encode.Problem) func(prop.Atom) smt.Term {
+	return func(a prop.Atom) smt.Term {
+		k := encode.Key{Account: a.Account, Asset: a.Asset}
+		switch a.Kind {
+		case prop.Before:
+			return p.Before[k]
+		case prop.After:
+			return p.After[k]
+		case prop.Sent:
+			return p.Sent[k]
+		case prop.Received:
+			return p.Received[k]
+		case prop.Moved:
+			return p.Moved[encode.MoveKey{From: a.Account, To: a.Account2, Asset: a.Asset}]
+		}
+		panic("unknown atom kind")
+	}
+}
+
+// Problem returns the SMT-LIB2 text of a property's problem: the model, the
+// property, and the assertion of its negation.
+func Problem(p *encode.Problem, pr prop.Property) string {
+	property := prop.Lower(pr.Formula, resolver(p), p.Success)
+	var sb strings.Builder
+	sb.WriteString(p.Text())
+	sb.WriteString("\n; property ")
+	sb.WriteString(pr.Name)
+	sb.WriteString(": ")
+	sb.WriteString(prop.Dump(pr.Formula))
+	sb.WriteString("\n(define-fun property () Bool ")
+	sb.WriteString(smt.Print(property))
+	sb.WriteString(")\n(assert (not property))\n")
+	return sb.String()
+}
+
+func checkOne(ctx context.Context, instrs []ir.Instr, p *encode.Problem, pr prop.Property, solver smt.Solver) (result Result) {
+	start := time.Now()
+	result = Result{Property: pr, SMT: Problem(p, pr)}
+	defer func() { result.Duration = time.Since(start) }()
+
+	res, err := solver.CheckSat(ctx, result.SMT, append(p.InputNames(), p.OutputNames()...))
+	if err != nil {
+		result.Status, result.Err = SolverError, err
+		return result
+	}
+	switch res.Status {
+	case smt.Unsat:
+		result.Status = Valid
+		return result
+	case smt.Unknown:
+		result.Status = Unknown
+		return result
+	}
+
+	before, model, err := p.OutcomeFromValues(res.Values)
+	if err != nil {
+		result.Status, result.Err = SolverError, err
+		return result
+	}
+	result.Before, result.Model = before, model
+	replay, err := encode.Replay(ctx, instrs, before, p.Keys, p.MoveKeys)
+	if err != nil {
+		result.Status, result.Err = ToolBug, err
+		return result
+	}
+	result.Replay = replay
+	result.Diffs = encode.Compare(model, replay)
+	result.Replayed = prop.Eval(pr.Formula, lookup(before, replay), replay.Success)
+	if len(result.Diffs) != 0 || result.Replayed {
+		result.Status = ToolBug
+		return result
+	}
+	result.Status = Counterexample
+	return result
+}
+
+func lookup(before map[encode.Key]*big.Int, out encode.Outcome) func(prop.Atom) *big.Int {
+	orZero := func(v *big.Int) *big.Int {
+		if v == nil {
+			return new(big.Int)
+		}
+		return v
+	}
+	return func(a prop.Atom) *big.Int {
+		k := encode.Key{Account: a.Account, Asset: a.Asset}
+		switch a.Kind {
+		case prop.Before:
+			return orZero(before[k])
+		case prop.After:
+			if v, ok := out.After[k]; ok {
+				return v
+			}
+			return orZero(before[k])
+		case prop.Sent:
+			return orZero(out.Sent[k])
+		case prop.Received:
+			return orZero(out.Received[k])
+		case prop.Moved:
+			return orZero(out.Moved[encode.MoveKey{From: a.Account, To: a.Account2, Asset: a.Asset}])
+		}
+		panic("unknown atom kind")
+	}
+}
+
+// AtomValues lists every atom of the property with its value on the
+// counterexample, in source order of first appearance.
+func (r Result) AtomValues() []AtomValue {
+	look := lookup(r.Before, r.Replay)
+	atoms := prop.Atoms(r.Property.Formula)
+	out := make([]AtomValue, len(atoms))
+	for i, a := range atoms {
+		out[i] = AtomValue{Atom: a, Value: look(a)}
+	}
+	sort.SliceStable(out, func(i, j int) bool { return out[i].Atom.String() < out[j].Atom.String() })
+	return out
+}
+
+type AtomValue struct {
+	Atom  prop.Atom
+	Value *big.Int
+}
diff --git a/internal/prove/prove_test.go b/internal/prove/prove_test.go
new file mode 100644
index 00000000..7f39a817
--- /dev/null
+++ b/internal/prove/prove_test.go
@@ -0,0 +1,159 @@
+package prove
+
+import (
+	"context"
+	"math/big"
+	"math/rand"
+	"os"
+	"path/filepath"
+	"strings"
+	"testing"
+	"time"
+
+	"github.com/formancehq/numscript/internal/compiler"
+	"github.com/formancehq/numscript/internal/ir"
+	"github.com/formancehq/numscript/internal/parser"
+	"github.com/formancehq/numscript/internal/prove/encode"
+	"github.com/formancehq/numscript/internal/prove/prop"
+	"github.com/formancehq/numscript/internal/prove/smt"
+	"github.com/stretchr/testify/require"
+)
+
+func requireZ3(t *testing.T) {
+	t.Helper()
+	if err := (smt.Solver{}).Available(); err != nil {
+		if os.Getenv("NUMSCRIPT_REQUIRE_Z3") != "" {
+			t.Fatal(err)
+		}
+		t.Skip(err)
+	}
+}
+
+func loadScript(t *testing.T, path string) []ir.Instr {
+	t.Helper()
+	content, err := os.ReadFile(path)
+	require.NoError(t, err)
+	if strings.HasSuffix(path, ".ir") {
+		instrs, errs := ir.Parse(string(content))
+		require.Empty(t, errs)
+		return instrs
+	}
+	parsed := parser.Parse(string(content))
+	require.Empty(t, parsed.Errors)
+	instrs, _, err := compiler.CompileToIR(parsed.Value, nil)
+	require.NoError(t, err)
+	return instrs
+}
+
+// crossCheck runs the script on random initial balances and requires the
+// property to hold on each: the only guard against an unsound "valid".
+func crossCheck(t *testing.T, instrs []ir.Instr, p *encode.Problem, pr prop.Property, seed int64) {
+	t.Helper()
+	rng := rand.New(rand.NewSource(seed))
+	for trial := 0; trial < 64; trial++ {
+		before := map[encode.Key]*big.Int{}
+		for _, k := range p.Keys {
+			var v int64
+			if rng.Intn(4) == 0 {
+				v = []int64{0, 50, 100, 150}[rng.Intn(4)]
+			} else {
+				v = int64(rng.Intn(601)) - 200
+			}
+			before[k] = big.NewInt(v)
+		}
+		replay, err := encode.Replay(context.Background(), instrs, before, p.Keys, p.MoveKeys)
+		require.NoError(t, err)
+		require.True(t, prop.Eval(pr.Formula, lookup(before, replay), replay.Success),
+			"property %q is false on the vm for balances %v", pr.Name, before)
+	}
+}
+
+func TestCases(t *testing.T) {
+	requireZ3(t)
+	propsFiles, err := filepath.Glob("testdata/cases/*.props")
+	require.NoError(t, err)
+	require.NotEmpty(t, propsFiles)
+
+	for _, propsPath := range propsFiles {
+		scriptPath := strings.TrimSuffix(propsPath, ".props")
+		t.Run(filepath.Base(scriptPath), func(t *testing.T) {
+			instrs := loadScript(t, scriptPath)
+
+			propsSrc, err := os.ReadFile(propsPath)
+			require.NoError(t, err)
+			props, errs := prop.ParseFile(string(propsSrc))
+			require.Empty(t, errs)
+
+			expectedSrc, err := os.ReadFile(scriptPath + ".expected")
+			require.NoError(t, err)
+			expected := map[string]string{}
+			var unsupported string
+			for _, line := range strings.Split(strings.TrimSpace(string(expectedSrc)), "\n") {
+				name, status, ok := strings.Cut(line, ": ")
+				require.True(t, ok, "malformed expected line %q", line)
+				if name == "unsupported" {
+					unsupported = status
+					continue
+				}
+				expected[name] = status
+			}
+
+			report, err := Check(context.Background(), instrs, props, Options{Solver: smt.Solver{Timeout: 10 * time.Second}})
+			if unsupported != "" {
+				var unsupportedErr encode.UnsupportedError
+				require.ErrorAs(t, err, &unsupportedErr)
+				require.Equal(t, unsupported, unsupportedErr.Reason)
+				return
+			}
+			require.NoError(t, err)
+			require.Len(t, report.Results, len(expected))
+
+			for i, res := range report.Results {
+				want, ok := expected[res.Property.Name]
+				require.True(t, ok, "no expectation for property %q", res.Property.Name)
+				require.Equal(t, want, res.Status.String(), "property %q: %v %v", res.Property.Name, res.Err, res.Diffs)
+				if res.Status == Valid {
+					crossCheck(t, instrs, report.Problem, res.Property, int64(i))
+				}
+			}
+		})
+	}
+}
+
+func TestPropertyErrors(t *testing.T) {
+	requireZ3(t)
+	instrs := loadScript(t, "testdata/cases/simple-send.num")
+	pr, errs := prop.ParseInline("after(@nobody, USD/2) == 0")
+	require.Empty(t, errs)
+	_, err := Check(context.Background(), instrs, []prop.Property{pr}, Options{})
+	var propErr PropertyError
+	require.ErrorAs(t, err, &propErr)
+	require.Len(t, propErr.Errors, 1)
+	require.Equal(t, "account @nobody is not referenced by the script (known: @dest, @src)", propErr.Errors[0].Msg)
+}
+
+func TestReportOutput(t *testing.T) {
+	requireZ3(t)
+	instrs := loadScript(t, "testdata/cases/simple-send.num")
+	src, err := os.ReadFile("testdata/cases/simple-send.num.props")
+	require.NoError(t, err)
+	props, errs := prop.ParseFile(string(src))
+	require.Empty(t, errs)
+	report, err := Check(context.Background(), instrs, props, Options{Solver: smt.Solver{Timeout: 10 * time.Second}})
+	require.NoError(t, err)
+	require.Equal(t, 1, report.ExitCode())
+	require.True(t, *report.SuccessReachable)
+	require.True(t, *report.FailureReachable)
+
+	out := report.Pretty("simple-send.num")
+	require.Contains(t, out, "success reachable: yes; failure reachable: yes")
+	require.Contains(t, out, "src_never_negative: after(@src, USD/2) >= 0")
+	require.Contains(t, out, "initial balances:")
+	require.Contains(t, out, "missing funds")
+	require.Contains(t, out, "6 valid, 1 counterexample")
+
+	js, err := report.JSON("simple-send.num")
+	require.NoError(t, err)
+	require.Contains(t, string(js), `"status": "counterexample"`)
+	require.Contains(t, string(js), `"outcome": "fails"`)
+}
diff --git a/internal/prove/report.go b/internal/prove/report.go
new file mode 100644
index 00000000..86fe1488
--- /dev/null
+++ b/internal/prove/report.go
@@ -0,0 +1,226 @@
+package prove
+
+import (
+	"bytes"
+	"encoding/json"
+	"fmt"
+	"math/big"
+	"strings"
+
+	"github.com/formancehq/numscript/internal/ansi"
+	"github.com/formancehq/numscript/internal/interpreter"
+	"github.com/formancehq/numscript/internal/prove/encode"
+	"github.com/formancehq/numscript/internal/prove/prop"
+)
+
+func yesNo(b *bool) string {
+	switch {
+	case b == nil:
+		return "unknown"
+	case *b:
+		return "yes"
+	}
+	return "no"
+}
+
+func (r *Report) touched() string {
+	accounts := make([]string, len(r.Problem.Accounts))
+	for i, a := range r.Problem.Accounts {
+		accounts[i] = "@" + a
+	}
+	return strings.Join(accounts, ", ") + " in " + strings.Join(r.Problem.Assets, ", ")
+}
+
+func statusIcon(s Status) string {
+	switch s {
+	case Valid:
+		return ansi.ColorGreen("✓")
+	case Counterexample:
+		return ansi.ColorRed("×")
+	case Unknown:
+		return ansi.ColorYellow("?")
+	}
+	return ansi.ColorRed("!")
+}
+
+// Pretty renders the human report.
+func (r *Report) Pretty(title string) string {
+	w := &strings.Builder{}
+	fmt.Fprintf(w, "%s: touches %s; success reachable: %s; failure reachable: %s\n\n",
+		title, r.touched(), yesNo(r.SuccessReachable), yesNo(r.FailureReachable))
+
+	width := 0
+	for _, res := range r.Results {
+		width = max(width, len(res.Property.Name))
+	}
+	for _, res := range r.Results {
+		fmt.Fprintf(w, "  %s %-*s  %-14s %s\n", statusIcon(res.Status), width, res.Property.Name, res.Status, res.Duration.Round(1e6))
+	}
+
+	counts := map[Status]int{}
+	for _, res := range r.Results {
+		counts[res.Status]++
+		if res.Status == Valid || res.Status == Unknown {
+			continue
+		}
+		fmt.Fprintf(w, "\n%s %s: %s\n", statusIcon(res.Status), res.Property.Name, prop.Dump(res.Property.Formula))
+		switch res.Status {
+		case Counterexample, ToolBug:
+			if res.Before != nil {
+				fmt.Fprintln(w, "  initial balances:")
+				fmt.Fprint(w, indent(balanceRows(res.Before).PrettyPrint(), "    "))
+				fmt.Fprintf(w, "  outcome: %s\n", r.outcomeLine(res.Model))
+				fmt.Fprintln(w, "  atoms:")
+				for _, av := range res.AtomValues() {
+					fmt.Fprintf(w, "    %s = %s\n", av.Atom, av.Value)
+				}
+			}
+			if res.Status == ToolBug {
+				fmt.Fprintln(w, "  the prover's model does not match the vm; this is a bug in the prover, not in the script:")
+				for _, d := range res.Diffs {
+					fmt.Fprintf(w, "    %s\n", d)
+				}
+				if res.Replayed {
+					fmt.Fprintln(w, "    the property holds on the vm run")
+				}
+				if res.Err != nil {
+					fmt.Fprintf(w, "    %s\n", res.Err)
+				}
+			}
+		case SolverError:
+			fmt.Fprintf(w, "  %s\n", res.Err)
+		}
+	}
+
+	var parts []string
+	for _, s := range []Status{Valid, Counterexample, Unknown, ToolBug, SolverError} {
+		if counts[s] != 0 {
+			parts = append(parts, fmt.Sprintf("%d %s", counts[s], s))
+		}
+	}
+	fmt.Fprintf(w, "\n%s\n", strings.Join(parts, ", "))
+	return w.String()
+}
+
+func (r *Report) outcomeLine(o encode.Outcome) string {
+	if o.Success {
+		return "success"
+	}
+	for _, s := range r.Problem.FailSites {
+		if s.Index == o.FailIndex {
+			return fmt.Sprintf("fails at instruction %d `%s`: %s", o.FailIndex, s.Text, o.FailKind)
+		}
+	}
+	return fmt.Sprintf("fails: %s", o.FailKind)
+}
+
+func indent(s, prefix string) string {
+	lines := strings.Split(strings.TrimRight(s, "\n"), "\n")
+	for i, l := range lines {
+		lines[i] = prefix + l
+	}
+	return strings.Join(lines, "\n") + "\n"
+}
+
+func balanceRows(before map[encode.Key]*big.Int) interpreter.Balances {
+	keys := make([]encode.Key, 0, len(before))
+	for k := range before {
+		keys = append(keys, k)
+	}
+	rows := make(interpreter.Balances, 0, len(keys))
+	for _, k := range sortKeys(keys) {
+		rows = append(rows, interpreter.BalanceRow{Account: k.Account, Asset: k.Asset, Amount: before[k]})
+	}
+	return rows
+}
+
+func sortKeys(keys []encode.Key) []encode.Key {
+	for i := 1; i < len(keys); i++ {
+		for j := i; j > 0 && less(keys[j], keys[j-1]); j-- {
+			keys[j], keys[j-1] = keys[j-1], keys[j]
+		}
+	}
+	return keys
+}
+
+func less(a, b encode.Key) bool {
+	if a.Account != b.Account {
+		return a.Account < b.Account
+	}
+	return a.Asset < b.Asset
+}
+
+type jsonReport struct {
+	Script           string       `json:"script"`
+	Accounts         []string     `json:"accounts"`
+	Assets           []string     `json:"assets"`
+	SuccessReachable *bool        `json:"successReachable"`
+	FailureReachable *bool        `json:"failureReachable"`
+	Results          []jsonResult `json:"results"`
+}
+
+type jsonResult struct {
+	Name           string              `json:"name"`
+	Formula        string              `json:"formula"`
+	Status         Status              `json:"status"`
+	DurationMs     int64               `json:"durationMs"`
+	Error          string              `json:"error,omitempty"`
+	Counterexample *jsonCounterexample `json:"counterexample,omitempty"`
+}
+
+type jsonCounterexample struct {
+	Balances interpreter.Balances `json:"balances"`
+	Outcome  string               `json:"outcome"`
+	Failure  *jsonFailure         `json:"failure,omitempty"`
+	Atoms    map[string]string    `json:"atoms"`
+	Diffs    []string             `json:"modelVmDiffs,omitempty"`
+}
+
+type jsonFailure struct {
+	Kind        string `json:"kind"`
+	Instruction int    `json:"instruction"`
+}
+
+// JSON renders the report for machines. Balance amounts are numbers, atom
+// values are strings.
+func (r *Report) JSON(title string) ([]byte, error) {
+	out := jsonReport{
+		Script:           title,
+		Accounts:         r.Problem.Accounts,
+		Assets:           r.Problem.Assets,
+		SuccessReachable: r.SuccessReachable,
+		FailureReachable: r.FailureReachable,
+		Results:          []jsonResult{},
+	}
+	for _, res := range r.Results {
+		jr := jsonResult{
+			Name:       res.Property.Name,
+			Formula:    prop.Dump(res.Property.Formula),
+			Status:     res.Status,
+			DurationMs: res.Duration.Milliseconds(),
+		}
+		if res.Err != nil {
+			jr.Error = res.Err.Error()
+		}
+		if res.Before != nil {
+			ce := &jsonCounterexample{Balances: balanceRows(res.Before), Outcome: "success", Atoms: map[string]string{}, Diffs: res.Diffs}
+			if !res.Model.Success {
+				ce.Outcome = "fails"
+				ce.Failure = &jsonFailure{Kind: res.Model.FailKind.String(), Instruction: res.Model.FailIndex}
+			}
+			for _, av := range res.AtomValues() {
+				ce.Atoms[av.Atom.String()] = av.Value.String()
+			}
+			jr.Counterexample = ce
+		}
+		out.Results = append(out.Results, jr)
+	}
+	var buf bytes.Buffer
+	enc := json.NewEncoder(&buf)
+	enc.SetEscapeHTML(false)
+	enc.SetIndent("", "  ")
+	if err := enc.Encode(out); err != nil {
+		return nil, err
+	}
+	return buf.Bytes(), nil
+}
diff --git a/internal/prove/result.go b/internal/prove/result.go
new file mode 100644
index 00000000..8faa1447
--- /dev/null
+++ b/internal/prove/result.go
@@ -0,0 +1,93 @@
+package prove
+
+import (
+	"math/big"
+	"time"
+
+	"github.com/formancehq/numscript/internal/prove/encode"
+	"github.com/formancehq/numscript/internal/prove/prop"
+)
+
+type Status int
+
+const (
+	// Valid: the property holds for every initial balance.
+	Valid Status = iota
+	// Counterexample: the solver found initial balances on which the property
+	// is false, and the VM confirmed them.
+	Counterexample
+	// Unknown: the solver gave up (timeout).
+	Unknown
+	// ToolBug: the solver's model does not reproduce on the VM, or the
+	// property does not evaluate to false on it. A bug in the prover.
+	ToolBug
+	// SolverError: the solver could not be run or rejected the problem.
+	SolverError
+)
+
+func (s Status) String() string {
+	switch s {
+	case Valid:
+		return "valid"
+	case Counterexample:
+		return "counterexample"
+	case Unknown:
+		return "unknown"
+	case ToolBug:
+		return "tool-bug"
+	case SolverError:
+		return "solver-error"
+	}
+	return "?"
+}
+
+func (s Status) MarshalText() ([]byte, error) { return []byte(s.String()), nil }
+
+type Result struct {
+	Property prop.Property
+	Status   Status
+	Duration time.Duration
+	// SMT is the complete problem the solver was given.
+	SMT string
+	Err error
+
+	// Set on Counterexample and ToolBug.
+	Before map[encode.Key]*big.Int
+	Model  encode.Outcome
+	Replay encode.Outcome
+	// Diffs lists model/VM disagreements (ToolBug).
+	Diffs []string
+	// Replayed is the property's value on the VM run: false on a
+	// counterexample, true means ToolBug.
+	Replayed bool
+}
+
+type Report struct {
+	Problem *encode.Problem
+	// SuccessReachable and FailureReachable say whether some initial balance
+	// makes the run succeed / fail; nil when the solver could not tell.
+	SuccessReachable *bool
+	FailureReachable *bool
+	Results          []Result
+}
+
+// ExitCode maps a report to the CLI's contract: 0 all valid, 1 a
+// counterexample, 2 only unknowns otherwise, 3 a tool or solver problem.
+func (r *Report) ExitCode() int {
+	code := 0
+	for _, res := range r.Results {
+		switch res.Status {
+		case Counterexample:
+			if code < 1 {
+				code = 1
+			}
+		case Unknown:
+			if code < 2 {
+				code = 2
+			}
+		case ToolBug, SolverError:
+			code = 3
+		}
+	}
+	return code
+}
diff --git a/internal/prove/smt/eval.go b/internal/prove/smt/eval.go
new file mode 100644
index 00000000..5b85a76a
--- /dev/null
+++ b/internal/prove/smt/eval.go
@@ -0,0 +1,172 @@
+package smt
+
+import (
+	"fmt"
+	"math/big"
+)
+
+// Value is a concrete Int or Bool.
+type Value struct {
+	Sort Sort
+	Int  *big.Int
+	Bool bool
+}
+
+func IntValue(v *big.Int) Value { return Value{Sort: SortInt, Int: new(big.Int).Set(v)} }
+func BoolValue(b bool) Value    { return Value{Sort: SortBool, Bool: b} }
+
+func (v Value) String() string {
+	if v.Sort == SortBool {
+		if v.Bool {
+			return "true"
+		}
+		return "false"
+	}
+	return v.Int.String()
+}
+
+// Evaluator evaluates terms under an assignment of the script's free symbols,
+// resolving defined names through the script and memoizing them.
+type Evaluator struct {
+	script *Script
+	inputs map[string]Value
+	memo   map[string]Value
+}
+
+func NewEvaluator(script *Script, inputs map[string]Value) *Evaluator {
+	return &Evaluator{script: script, inputs: inputs, memo: map[string]Value{}}
+}
+
+func (e *Evaluator) Eval(t Term) (Value, error) {
+	switch t := t.(type) {
+	case intLit:
+		return IntValue(t.v), nil
+	case boolLit:
+		return BoolValue(t.v), nil
+	case symbol:
+		if v, ok := e.memo[t.name]; ok {
+			return v, nil
+		}
+		if v, ok := e.inputs[t.name]; ok {
+			return v, nil
+		}
+		def, ok := e.script.Definition(t.name)
+		if !ok {
+			return Value{}, fmt.Errorf("smt: symbol %s has no value", t.name)
+		}
+		v, err := e.Eval(def)
+		if err != nil {
+			return Value{}, err
+		}
+		e.memo[t.name] = v
+		return v, nil
+	case app:
+		return e.evalApp(t)
+	}
+	return Value{}, fmt.Errorf("smt: unknown term")
+}
+
+func (e *Evaluator) ints(args []Term) ([]*big.Int, error) {
+	out := make([]*big.Int, len(args))
+	for i, a := range args {
+		v, err := e.Eval(a)
+		if err != nil {
+			return nil, err
+		}
+		if v.Sort != SortInt {
+			return nil, fmt.Errorf("smt: expected an Int")
+		}
+		out[i] = v.Int
+	}
+	return out, nil
+}
+
+func (e *Evaluator) evalApp(t app) (Value, error) {
+	switch t.op {
+	case "+", "-", "*", "div", "mod":
+		xs, err := e.ints(t.args)
+		if err != nil {
+			return Value{}, err
+		}
+		r := new(big.Int)
+		switch t.op {
+		case "+":
+			r.Add(xs[0], xs[1])
+		case "-":
+			if len(xs) == 1 {
+				r.Neg(xs[0])
+			} else {
+				r.Sub(xs[0], xs[1])
+			}
+		case "*":
+			r.Mul(xs[0], xs[1])
+		case "div":
+			r.Div(xs[0], xs[1])
+		case "mod":
+			r.Mod(xs[0], xs[1])
+		}
+		return IntValue(r), nil
+	case "<", "<=":
+		xs, err := e.ints(t.args)
+		if err != nil {
+			return Value{}, err
+		}
+		c := xs[0].Cmp(xs[1])
+		if t.op == "<" {
+			return BoolValue(c < 0), nil
+		}
+		return BoolValue(c <= 0), nil
+	case "=":
+		a, err := e.Eval(t.args[0])
+		if err != nil {
+			return Value{}, err
+		}
+		b, err := e.Eval(t.args[1])
+		if err != nil {
+			return Value{}, err
+		}
+		if a.Sort == SortBool {
+			return BoolValue(a.Bool == b.Bool), nil
+		}
+		return BoolValue(a.Int.Cmp(b.Int) == 0), nil
+	case "not":
+		a, err := e.Eval(t.args[0])
+		if err != nil {
+			return Value{}, err
+		}
+		return BoolValue(!a.Bool), nil
+	case "and", "or":
+		for _, a := range t.args {
+			v, err := e.Eval(a)
+			if err != nil {
+				return Value{}, err
+			}
+			if t.op == "and" && !v.Bool {
+				return BoolValue(false), nil
+			}
+			if t.op == "or" && v.Bool {
+				return BoolValue(true), nil
+			}
+		}
+		return BoolValue(t.op == "and"), nil
+	case "=>":
+		a, err := e.Eval(t.args[0])
+		if err != nil {
+			return Value{}, err
+		}
+		if !a.Bool {
+			return BoolValue(true), nil
+		}
+		return e.Eval(t.args[1])
+	case "ite":
+		c, err := e.Eval(t.args[0])
+		if err != nil {
+			return Value{}, err
+		}
+		if c.Bool {
+			return e.Eval(t.args[1])
+		}
+		return e.Eval(t.args[2])
+	}
+	return Value{}, fmt.Errorf("smt: unknown operator %s", t.op)
+}
diff --git a/internal/prove/smt/print.go b/internal/prove/smt/print.go
new file mode 100644
index 00000000..bfba9d43
--- /dev/null
+++ b/internal/prove/smt/print.go
@@ -0,0 +1,71 @@
+package smt
+
+import (
+	"strings"
+)
+
+// Print renders a term in SMT-LIB2 syntax. Negative literals print as (- n)
+// because a bare "-5" is not a numeral in the standard.
+func Print(t Term) string {
+	var sb strings.Builder
+	printTo(&sb, t)
+	return sb.String()
+}
+
+func printTo(sb *strings.Builder, t Term) {
+	switch t := t.(type) {
+	case intLit:
+		if t.v.Sign() < 0 {
+			sb.WriteString("(- ")
+			sb.WriteString(t.v.String()[1:])
+			sb.WriteString(")")
+		} else {
+			sb.WriteString(t.v.String())
+		}
+	case boolLit:
+		if t.v {
+			sb.WriteString("true")
+		} else {
+			sb.WriteString("false")
+		}
+	case symbol:
+		sb.WriteString(Quote(t.name))
+	case app:
+		sb.WriteString("(")
+		sb.WriteString(t.op)
+		for _, a := range t.args {
+			sb.WriteString(" ")
+			printTo(sb, a)
+		}
+		sb.WriteString(")")
+	default:
+		panic("smt.Print: unknown term")
+	}
+}
+
+// Quote wraps name in |..| unless it is a simple SMT-LIB symbol.
+func Quote(name string) string {
+	if isSimpleSymbol(name) {
+		return name
+	}
+	return "|" + name + "|"
+}
+
+func isSimpleSymbol(name string) bool {
+	if name == "" {
+		return false
+	}
+	for i, r := range name {
+		switch {
+		case r >= 'a' && r <= 'z', r >= 'A' && r <= 'Z':
+		case r >= '0' && r <= '9':
+			if i == 0 {
+				return false
+			}
+		case strings.ContainsRune("~!@$%^&*_-+=<>.?/", r):
+		default:
+			return false
+		}
+	}
+	return true
+}
diff --git a/internal/prove/smt/script.go b/internal/prove/smt/script.go
new file mode 100644
index 00000000..b2a69b82
--- /dev/null
+++ b/internal/prove/smt/script.go
@@ -0,0 +1,109 @@
+package smt
+
+import (
+	"fmt"
+	"strings"
+)
+
+// Script accumulates declarations, definitions and assertions in order. It
+// also remembers every definition, so Eval can evaluate a term that refers to
+// defined names.
+type Script struct {
+	lines   []string
+	defined map[string]Term
+	sorts   map[string]Sort
+	order   []string
+}
+
+// Header is what every complete script starts with.
+const Header = "(set-logic QF_LIA)\n(set-option :produce-models true)\n"
+
+func NewScript() *Script {
+	s := NewBareScript()
+	s.lines = append(s.lines, strings.TrimSuffix(Header, "\n"))
+	return s
+}
+
+// NewBareScript starts a script without the header, for a body whose
+// declarations are emitted separately in front of it.
+func NewBareScript() *Script {
+	return &Script{
+		defined: map[string]Term{},
+		sorts:   map[string]Sort{},
+	}
+}
+
+// Lines returns the commands emitted so far.
+func (s *Script) Lines() []string {
+	return s.lines
+}
+
+func (s *Script) Comment(format string, args ...any) {
+	for _, line := range strings.Split(fmt.Sprintf(format, args...), "\n") {
+		s.lines = append(s.lines, "; "+line)
+	}
+}
+
+func (s *Script) Blank() {
+	s.lines = append(s.lines, "")
+}
+
+// DeclareConst declares a free symbol. Declaring a name twice is a bug.
+func (s *Script) DeclareConst(name string, sort Sort) Term {
+	s.bind(name, sort)
+	s.lines = append(s.lines, fmt.Sprintf("(declare-const %s %s)", Quote(name), sort))
+	return symbol{name, sort}
+}
+
+// Define names t. A literal or a symbol is returned as is, so an alias costs
+// no definition and the printed script stays a DAG of real computations.
+func (s *Script) Define(name string, t Term) Term {
+	if IsLeaf(t) {
+		return t
+	}
+	s.bind(name, t.Sort())
+	s.defined[name] = t
+	s.lines = append(s.lines, fmt.Sprintf("(define-fun %s () %s %s)", Quote(name), t.Sort(), Print(t)))
+	return symbol{name, t.Sort()}
+}
+
+// DefineAlways is Define for names that must exist in the script (the
+// outputs a caller will get-value), even when their term is a leaf.
+func (s *Script) DefineAlways(name string, t Term) Term {
+	if !IsLeaf(t) {
+		return s.Define(name, t)
+	}
+	s.bind(name, t.Sort())
+	s.defined[name] = t
+	s.lines = append(s.lines, fmt.Sprintf("(define-fun %s () %s %s)", Quote(name), t.Sort(), Print(t)))
+	return symbol{name, t.Sort()}
+}
+
+func (s *Script) bind(name string, sort Sort) {
+	if _, dup := s.sorts[name]; dup {
+		panic("smt.Script: name bound twice: " + name)
+	}
+	s.sorts[name] = sort
+	s.order = append(s.order, name)
+}
+
+func (s *Script) Assert(t Term) {
+	s.lines = append(s.lines, fmt.Sprintf("(assert %s)", Print(t)))
+}
+
+// Text is the script so far, one command per line.
+func (s *Script) Text() string {
+	return strings.Join(s.lines, "\n") + "\n"
+}
+
+// Definition returns the term bound to a defined name.
+func (s *Script) Definition(name string) (Term, bool) {
+	t, ok := s.defined[name]
+	return t, ok
+}
+
+// SortOf returns the sort of a declared or defined name.
+func (s *Script) SortOf(name string) (Sort, bool) {
+	sort, ok := s.sorts[name]
+	return sort, ok
+}
diff --git a/internal/prove/smt/sexpr.go b/internal/prove/smt/sexpr.go
new file mode 100644
index 00000000..cef4a01e
--- /dev/null
+++ b/internal/prove/smt/sexpr.go
@@ -0,0 +1,156 @@
+package smt
+
+import (
+	"fmt"
+	"math/big"
+	"strings"
+)
+
+// sexpr is a node of solver output: an atom or a list.
+type sexpr struct {
+	atom   string
+	list   []sexpr
+	isList bool
+}
+
+func (s sexpr) String() string {
+	if !s.isList {
+		return s.atom
+	}
+	parts := make([]string, len(s.list))
+	for i, c := range s.list {
+		parts[i] = c.String()
+	}
+	return "(" + strings.Join(parts, " ") + ")"
+}
+
+// parseSexprs reads every top-level s-expression of text. Quoted symbols
+// |..| and string literals ".." are kept as single atoms, with the delimiters
+// stripped for symbols.
+func parseSexprs(text string) ([]sexpr, error) {
+	p := &sexprParser{src: text}
+	var out []sexpr
+	for {
+		p.skipSpace()
+		if p.pos >= len(p.src) {
+			return out, nil
+		}
+		node, err := p.next()
+		if err != nil {
+			return nil, err
+		}
+		out = append(out, node)
+	}
+}
+
+type sexprParser struct {
+	src string
+	pos int
+}
+
+func (p *sexprParser) skipSpace() {
+	for p.pos < len(p.src) {
+		c := p.src[p.pos]
+		switch c {
+		case ' ', '\n', '\t', '\r':
+			p.pos++
+		case ';':
+			for p.pos < len(p.src) && p.src[p.pos] != '\n' {
+				p.pos++
+			}
+		default:
+			return
+		}
+	}
+}
+
+func (p *sexprParser) next() (sexpr, error) {
+	p.skipSpace()
+	if p.pos >= len(p.src) {
+		return sexpr{}, fmt.Errorf("smt: unexpected end of solver output")
+	}
+	switch c := p.src[p.pos]; c {
+	case '(':
+		p.pos++
+		node := sexpr{isList: true}
+		for {
+			p.skipSpace()
+			if p.pos >= len(p.src) {
+				return sexpr{}, fmt.Errorf("smt: unclosed list in solver output")
+			}
+			if p.src[p.pos] == ')' {
+				p.pos++
+				return node, nil
+			}
+			child, err := p.next()
+			if err != nil {
+				return sexpr{}, err
+			}
+			node.list = append(node.list, child)
+		}
+	case ')':
+		return sexpr{}, fmt.Errorf("smt: unexpected ')' in solver output")
+	case '|':
+		end := strings.IndexByte(p.src[p.pos+1:], '|')
+		if end < 0 {
+			return sexpr{}, fmt.Errorf("smt: unclosed |symbol| in solver output")
+		}
+		atom := p.src[p.pos+1 : p.pos+1+end]
+		p.pos += end + 2
+		return sexpr{atom: atom}, nil
+	case '"':
+		var sb strings.Builder
+		p.pos++
+		for {
+			if p.pos >= len(p.src) {
+				return sexpr{}, fmt.Errorf("smt: unclosed string in solver output")
+			}
+			if p.src[p.pos] == '"' {
+				if p.pos+1 < len(p.src) && p.src[p.pos+1] == '"' {
+					sb.WriteByte('"')
+					p.pos += 2
+					continue
+				}
+				p.pos++
+				return sexpr{atom: sb.String()}, nil
+			}
+			sb.WriteByte(p.src[p.pos])
+			p.pos++
+		}
+	default:
+		start := p.pos
+		for p.pos < len(p.src) && !strings.ContainsRune(" \n\t\r()|\"", rune(p.src[p.pos])) {
+			p.pos++
+		}
+		return sexpr{atom: p.src[start:p.pos]}, nil
+	}
+}
+
+// parseValue decodes a value as printed by get-value: a numeral, (- numeral),
+// true or false.
+func parseValue(s sexpr) (Value, error) {
+	if !s.isList {
+		switch s.atom {
+		case "true":
+			return BoolValue(true), nil
+		case "false":
+			return BoolValue(false), nil
+		}
+		n, ok := new(big.Int).SetString(s.atom, 10)
+		if !ok {
+			return Value{}, fmt.Errorf("smt: cannot parse value %q", s.atom)
+		}
+		return IntValue(n), nil
+	}
+	if len(s.list) == 2 && !s.list[0].isList && s.list[0].atom == "-" {
+		inner, err := parseValue(s.list[1])
+		if err != nil {
+			return Value{}, err
+		}
+		if inner.Sort != SortInt {
+			return Value{}, fmt.Errorf("smt: cannot negate %s", s)
+		}
+		return IntValue(new(big.Int).Neg(inner.Int)), nil
+	}
+	return Value{}, fmt.Errorf("smt: cannot parse value %s", s)
+}
diff --git a/internal/prove/smt/smt_test.go b/internal/prove/smt/smt_test.go
new file mode 100644
index 00000000..9de29550
--- /dev/null
+++ b/internal/prove/smt/smt_test.go
@@ -0,0 +1,133 @@
+package smt
+
+import (
+	"context"
+	"math/big"
+	"os"
+	"testing"
+	"time"
+
+	"github.com/stretchr/testify/require"
+)
+
+func requireZ3(t *testing.T) {
+	t.Helper()
+	if err := (Solver{}).Available(); err != nil {
+		if os.Getenv("NUMSCRIPT_REQUIRE_Z3") != "" {
+			t.Fatal(err)
+		}
+		t.Skip(err)
+	}
+}
+
+func TestFolding(t *testing.T) {
+	x := Symbol("x", SortInt)
+	require.Equal(t, "7", Print(Add(Int64(3), Int64(4))))
+	require.Equal(t, "x", Print(Add(x, Int64(0))))
+	require.Equal(t, "0", Print(Sub(x, x)))
+	require.Equal(t, "(- 3)", Print(Neg(Int64(3))))
+	require.Equal(t, "(- x)", Print(Neg(x)))
+	require.Equal(t, "x", Print(MulConst(big.NewInt(1), x)))
+	require.Equal(t, "(* 2 x)", Print(MulConst(big.NewInt(2), x)))
+	require.Equal(t, "(- 3)", Print(DivConst(Int64(-5), big.NewInt(2))))
+	require.Equal(t, "1", Print(ModConst(Int64(-5), big.NewInt(2))))
+	require.Equal(t, "true", Print(Lt(Int64(0), Int64(10))))
+	require.Equal(t, "false", Print(Lt(x, x)))
+	require.Equal(t, "true", Print(And(Bool(true), Bool(true))))
+	require.Equal(t, "false", Print(And(Symbol("a", SortBool), Bool(false))))
+	require.Equal(t, "(and a b)", Print(And(Symbol("a", SortBool), Bool(true), Symbol("b", SortBool))))
+	require.Equal(t, "(or a b c)", Print(Or(Or(Symbol("a", SortBool), Symbol("b", SortBool)), Symbol("c", SortBool))))
+	require.Equal(t, "a", Print(Not(Not(Symbol("a", SortBool)))))
+	require.Equal(t, "x", Print(Ite(Bool(true), x, Int64(1))))
+	require.Equal(t, "x", Print(Ite(Symbol("c", SortBool), x, x)))
+	require.Equal(t, "c", Print(Ite(Symbol("c", SortBool), Bool(true), Bool(false))))
+	require.Equal(t, "(not c)", Print(Ite(Symbol("c", SortBool), Bool(false), Bool(true))))
+	require.Equal(t, "(ite (< x 0) 0 x)", Print(Max0(x)))
+	require.Equal(t, "(ite (< x 0) 0 x)", Print(Max0(Max0(x))))
+	require.Equal(t, "(ite (< x 10) x 10)", Print(Min(x, Int64(10))))
+	require.Equal(t, "3", Print(Min(Int64(3), Int64(10))))
+	require.Equal(t, "b", Print(Implies(Bool(true), Symbol("b", SortBool))))
+	require.Equal(t, "true", Print(Implies(Symbol("a", SortBool), Bool(true))))
+	require.Equal(t, "(not a)", Print(Iff(Symbol("a", SortBool), Bool(false))))
+	// a min of two non-negatives needs no outer clamp
+	require.Equal(t, "(ite (< (ite (< x 0) 0 x) 10) (ite (< x 0) 0 x) 10)", Print(Max0(Min(Max0(x), Int64(10)))))
+}
+
+func TestPrintQuoting(t *testing.T) {
+	require.Equal(t, "$r9@18", Print(Symbol("$r9@18", SortInt)))
+	require.Equal(t, "|before(@src,USD/2)|", Print(Symbol("before(@src,USD/2)", SortInt)))
+	require.Equal(t, "|1x|", Print(Symbol("1x", SortInt)))
+	require.Equal(t, "(= |a b| (- 5))", Print(Eq(Symbol("a b", SortInt), Int64(-5))))
+}
+
+func TestScriptDefineAliasesLeaves(t *testing.T) {
+	s := NewScript()
+	x := s.DeclareConst("x", SortInt)
+	require.Equal(t, x, s.Define("y", x))
+	y := s.Define("y", Add(x, Int64(1)))
+	require.Equal(t, "y", Print(y))
+	def, ok := s.Definition("y")
+	require.True(t, ok)
+	require.Equal(t, "(+ x 1)", Print(def))
+	require.Equal(t, "(set-logic QF_LIA)\n(set-option :produce-models true)\n(declare-const x Int)\n(define-fun y () Int (+ x 1))\n", s.Text())
+	require.Panics(t, func() { s.Define("y", Add(x, Int64(2))) })
+}
+
+func TestParseResult(t *testing.T) {
+	res, err := parseResult("sat\n((|before(@src,USD/2)| (- 5))\n (fails true)\n (n 42))\n")
+	require.NoError(t, err)
+	require.Equal(t, Sat, res.Status)
+	require.Equal(t, "-5", res.Values["before(@src,USD/2)"].String())
+	require.Equal(t, "true", res.Values["fails"].String())
+	require.Equal(t, "42", res.Values["n"].String())
+
+	res, err = parseResult("unsat\n(error \"line 12 column 10: model is not available\")\n")
+	require.NoError(t, err)
+	require.Equal(t, Unsat, res.Status)
+
+	res, err = parseResult("unknown\n")
+	require.NoError(t, err)
+	require.Equal(t, Unknown, res.Status)
+
+	_, err = parseResult("(error \"line 3 column 4: unknown constant foo\")\nsat\n")
+	require.Error(t, err)
+
+	_, err = parseResult("")
+	require.Error(t, err)
+}
+
+func TestEvaluator(t *testing.T) {
+	s := NewScript()
+	x := s.DeclareConst("x", SortInt)
+	y := s.Define("y", Add(DivConst(x, big.NewInt(2)), ModConst(x, big.NewInt(2))))
+	z := s.Define("z", Ite(Lt(y, Int64(0)), Neg(y), Max0(Sub(y, Int64(10)))))
+	ev := NewEvaluator(s, map[string]Value{"x": IntValue(big.NewInt(-5))})
+	v, err := ev.Eval(z)
+	require.NoError(t, err)
+	// -5 div 2 = -3, -5 mod 2 = 1, y = -2, z = 2
+	require.Equal(t, "2", v.String())
+	v, err = ev.Eval(And(Lt(x, Int64(0)), Implies(Bool(false), Bool(false))))
+	require.NoError(t, err)
+	require.True(t, v.Bool)
+	_, err = ev.Eval(Symbol("w", SortInt))
+	require.Error(t, err)
+}
+
+func TestZ3RoundTrip(t *testing.T) {
+	requireZ3(t)
+	s := NewScript()
+	x := s.DeclareConst("before(@src,USD/2)", SortInt)
+	s.Assert(Lt(x, Int64(-3)))
+	res, err := Solver{Timeout: 5 * time.Second}.CheckSat(context.Background(), s.Text(), []string{"before(@src,USD/2)"})
+	require.NoError(t, err)
+	require.Equal(t, Sat, res.Status)
+	require.True(t, res.Values["before(@src,USD/2)"].Int.Cmp(big.NewInt(-3)) < 0)
+
+	s.Assert(Gt(x, Int64(0)))
+	res, err = Solver{Timeout: 5 * time.Second}.CheckSat(context.Background(), s.Text(), []string{"before(@src,USD/2)"})
+	require.NoError(t, err)
+	require.Equal(t, Unsat, res.Status)
+
+	_, err = Solver{Path: "no-such-solver"}.CheckSat(context.Background(), s.Text(), nil)
+	require.ErrorIs(t, err, ErrSolverNotFound)
+}
diff --git a/internal/prove/smt/solver.go b/internal/prove/smt/solver.go
new file mode 100644
index 00000000..63c69b21
--- /dev/null
+++ b/internal/prove/smt/solver.go
@@ -0,0 +1,174 @@
+package smt
+
+import (
+	"bytes"
+	"context"
+	"errors"
+	"fmt"
+	"os/exec"
+	"path/filepath"
+	"strings"
+	"time"
+)
+
+type Status int
+
+const (
+	Sat Status = iota
+	Unsat
+	Unknown
+)
+
+func (s Status) String() string {
+	switch s {
+	case Sat:
+		return "sat"
+	case Unsat:
+		return "unsat"
+	}
+	return "unknown"
+}
+
+type Result struct {
+	Status Status
+	// Values is the get-value answer, keyed by the unquoted symbol name. Empty
+	// unless the status is Sat.
+	Values map[string]Value
+	// Raw is the solver's whole stdout.
+	Raw string
+}
+
+// Solver runs an SMT-LIB2 solver as a subprocess, feeding the script on stdin.
+// Path is the executable ("z3" when empty). The soft timeout is passed with
+// the solver's own flag when the executable is z3 or cvc5, so the solver
+// answers unknown instead of being killed.
+type Solver struct {
+	Path    string
+	Timeout time.Duration
+}
+
+var ErrSolverNotFound = errors.New("smt: solver not found")
+
+func (s Solver) path() string {
+	if s.Path == "" {
+		return "z3"
+	}
+	return s.Path
+}
+
+// Available reports whether the solver executable can be found.
+func (s Solver) Available() error {
+	if _, err := exec.LookPath(s.path()); err != nil {
+		return fmt.Errorf("%w: %s", ErrSolverNotFound, s.path())
+	}
+	return nil
+}
+
+func (s Solver) args() []string {
+	ms := s.Timeout.Milliseconds()
+	switch strings.TrimSuffix(filepath.Base(s.path()), ".exe") {
+	case "z3":
+		args := []string{"-in", "-smt2"}
+		if ms > 0 {
+			args = append(args, fmt.Sprintf("-t:%d", ms))
+		}
+		return args
+	case "cvc5":
+		args := []string{"--lang", "smt2"}
+		if ms > 0 {
+			args = append(args, fmt.Sprintf("--tlimit=%d", ms))
+		}
+		return args
+	}
+	return nil
+}
+
+// CheckSat runs script followed by (check-sat) and, when getValue is not
+// empty, (get-value (...)) for those names.
+func (s Solver) CheckSat(ctx context.Context, script string, getValue []string) (Result, error) {
+	if err := s.Available(); err != nil {
+		return Result{}, err
+	}
+
+	var input strings.Builder
+	input.WriteString(script)
+	input.WriteString("(check-sat)\n")
+	if len(getValue) > 0 {
+		input.WriteString("(get-value (")
+		for i, name := range getValue {
+			if i > 0 {
+				input.WriteString(" ")
+			}
+			input.WriteString(Quote(name))
+		}
+		input.WriteString("))\n")
+	}
+
+	if s.Timeout > 0 {
+		var cancel context.CancelFunc
+		ctx, cancel = context.WithTimeout(ctx, s.Timeout+2*time.Second)
+		defer cancel()
+	}
+	cmd := exec.CommandContext(ctx, s.path(), s.args()...)
+	cmd.Stdin = strings.NewReader(input.String())
+	var stdout, stderr bytes.Buffer
+	cmd.Stdout = &stdout
+	cmd.Stderr = &stderr
+	runErr := cmd.Run()
+	raw := stdout.String()
+
+	res, err := parseResult(raw)
+	if err != nil {
+		if runErr != nil {
+			return Result{Raw: raw}, fmt.Errorf("smt: solver failed: %w\n%s%s", runErr, raw, stderr.String())
+		}
+		return Result{Raw: raw}, err
+	}
+	return res, nil
+}
+
+func parseResult(raw string) (Result, error) {
+	nodes, err := parseSexprs(raw)
+	if err != nil {
+		return Result{}, err
+	}
+	res := Result{Raw: raw, Values: map[string]Value{}}
+	status := false
+	for _, n := range nodes {
+		switch {
+		case !n.isList:
+			switch n.atom {
+			case "sat":
+				res.Status, status = Sat, true
+			case "unsat":
+				res.Status, status = Unsat, true
+			case "unknown":
+				res.Status, status = Unknown, true
+			default:
+				return Result{}, fmt.Errorf("smt: unexpected solver output %q", n.atom)
+			}
+		case len(n.list) == 2 && !n.list[0].isList && n.list[0].atom == "error":
+			// get-value after unsat/unknown has no model to report, which is
+			// not an error of ours
+			if status && res.Status != Sat {
+				continue
+			}
+			return Result{}, fmt.Errorf("smt: solver error: %s", n.list[1].atom)
+		default:
+			for _, pair := range n.list {
+				if !pair.isList || len(pair.list) != 2 || pair.list[0].isList {
+					return Result{}, fmt.Errorf("smt: unexpected solver output %s", pair)
+				}
+				v, err := parseValue(pair.list[1])
+				if err != nil {
+					return Result{}, err
+				}
+				res.Values[pair.list[0].atom] = v
+			}
+		}
+	}
+	if !status {
+		return Result{}, fmt.Errorf("smt: solver printed no status:\n%s", raw)
+	}
+	return res, nil
+}
diff --git a/internal/prove/smt/term.go b/internal/prove/smt/term.go
new file mode 100644
index 00000000..f1e69e90
--- /dev/null
+++ b/internal/prove/smt/term.go
@@ -0,0 +1,383 @@
+// Package smt is the SMT-LIB2 layer of the prover: a small term AST over the
+// Int and Bool sorts whose constructors fold constants, a printer, a script
+// builder, a reader for solver output, a subprocess driver and a concrete
+// evaluator.
+//
+// Only linear integer arithmetic is constructible: multiplication, division and
+// modulo take a literal operand, so every script stays in QF_LIA.
+package smt
+
+import (
+	"math/big"
+)
+
+type Sort uint8
+
+const (
+	SortInt Sort = iota
+	SortBool
+)
+
+func (s Sort) String() string {
+	if s == SortBool {
+		return "Bool"
+	}
+	return "Int"
+}
+
+type Term interface {
+	Sort() Sort
+	// nonNeg reports whether an Int term is known to be >= 0 without solving.
+	nonNeg() bool
+}
+
+type intLit struct{ v *big.Int }
+type boolLit struct{ v bool }
+type symbol struct {
+	name string
+	sort Sort
+}
+type app struct {
+	op   string
+	args []Term
+	sort Sort
+	nn   bool
+}
+
+func (intLit) Sort() Sort     { return SortInt }
+func (boolLit) Sort() Sort    { return SortBool }
+func (s symbol) Sort() Sort   { return s.sort }
+func (a app) Sort() Sort      { return a.sort }
+func (l intLit) nonNeg() bool { return l.v.Sign() >= 0 }
+func (boolLit) nonNeg() bool  { return false }
+func (symbol) nonNeg() bool   { return false }
+func (a app) nonNeg() bool    { return a.nn }
+
+var (
+	zero = intLit{big.NewInt(0)}
+	one  = intLit{big.NewInt(1)}
+)
+
+func Int(v *big.Int) Term { return intLit{new(big.Int).Set(v)} }
+func Int64(v int64) Term  { return intLit{big.NewInt(v)} }
+func Bool(b bool) Term    { return boolLit{b} }
+func Symbol(name string, sort Sort) Term {
+	return symbol{name, sort}
+}
+
+// SymbolName returns the name of a symbol term.
+func SymbolName(t Term) (string, bool) {
+	s, ok := t.(symbol)
+	return s.name, ok
+}
+
+func AsInt(t Term) (*big.Int, bool) {
+	l, ok := t.(intLit)
+	if !ok {
+		return nil, false
+	}
+	return new(big.Int).Set(l.v), true
+}
+
+func AsBool(t Term) (bool, bool) {
+	l, ok := t.(boolLit)
+	return l.v, ok
+}
+
+func IsTrue(t Term) bool  { b, ok := AsBool(t); return ok && b }
+func IsFalse(t Term) bool { b, ok := AsBool(t); return ok && !b }
+
+// IsLeaf reports whether printing t costs nothing to repeat: a literal or a
+// symbol. Script.Define aliases those instead of naming them.
+func IsLeaf(t Term) bool {
+	switch t.(type) {
+	case intLit, boolLit, symbol:
+		return true
+	}
+	return false
+}
+
+// same is a cheap structural equality: literals by value, symbols by name,
+// anything else by identity. It is what the folds below need and nothing more.
+func same(a, b Term) bool {
+	switch a := a.(type) {
+	case intLit:
+		b, ok := b.(intLit)
+		return ok && a.v.Cmp(b.v) == 0
+	case boolLit:
+		b, ok := b.(boolLit)
+		return ok && a.v == b.v
+	case symbol:
+		b, ok := b.(symbol)
+		return ok && a == b
+	}
+	return false
+}
+
+func lit(a, b Term) (*big.Int, *big.Int, bool) {
+	x, okx := a.(intLit)
+	y, oky := b.(intLit)
+	if !okx || !oky {
+		return nil, nil, false
+	}
+	return x.v, y.v, true
+}
+
+func Add(a, b Term) Term {
+	if x, y, ok := lit(a, b); ok {
+		return intLit{new(big.Int).Add(x, y)}
+	}
+	if same(a, zero) {
+		return b
+	}
+	if same(b, zero) {
+		return a
+	}
+	return app{"+", []Term{a, b}, SortInt, a.nonNeg() && b.nonNeg()}
+}
+
+func Sub(a, b Term) Term {
+	if x, y, ok := lit(a, b); ok {
+		return intLit{new(big.Int).Sub(x, y)}
+	}
+	if same(b, zero) {
+		return a
+	}
+	if same(a, b) {
+		return zero
+	}
+	return app{"-", []Term{a, b}, SortInt, false}
+}
+
+func Neg(a Term) Term {
+	if x, ok := a.(intLit); ok {
+		return intLit{new(big.Int).Neg(x.v)}
+	}
+	return app{"-", []Term{a}, SortInt, false}
+}
+
+// MulConst is c * a, with c a literal so the term stays linear.
+func MulConst(c *big.Int, a Term) Term {
+	if x, ok := a.(intLit); ok {
+		return intLit{new(big.Int).Mul(c, x.v)}
+	}
+	switch {
+	case c.Sign() == 0:
+		return zero
+	case c.Cmp(one.v) == 0:
+		return a
+	}
+	return app{"*", []Term{intLit{new(big.Int).Set(c)}, a}, SortInt, c.Sign() > 0 && a.nonNeg()}
+}
+
+// DivConst is floor(a / d) for a literal d > 0 (SMT-LIB div is Euclidean,
+// which is the floor for a positive divisor, like big.Int.Div).
+func DivConst(a Term, d *big.Int) Term {
+	if d.Sign() <= 0 {
+		panic("smt.DivConst: divisor must be positive")
+	}
+	if x, ok := a.(intLit); ok {
+		return intLit{new(big.Int).Div(x.v, d)}
+	}
+	if d.Cmp(one.v) == 0 {
+		return a
+	}
+	return app{"div", []Term{a, intLit{new(big.Int).Set(d)}}, SortInt, a.nonNeg()}
+}
+
+// ModConst is a mod d for a literal d > 0 (Euclidean, always in [0, d)).
+func ModConst(a Term, d *big.Int) Term {
+	if d.Sign() <= 0 {
+		panic("smt.ModConst: divisor must be positive")
+	}
+	if x, ok := a.(intLit); ok {
+		return intLit{new(big.Int).Mod(x.v, d)}
+	}
+	if d.Cmp(one.v) == 0 {
+		return zero
+	}
+	return app{"mod", []Term{a, intLit{new(big.Int).Set(d)}}, SortInt, true}
+}
+
+func Lt(a, b Term) Term {
+	if x, y, ok := lit(a, b); ok {
+		return boolLit{x.Cmp(y) < 0}
+	}
+	if same(a, b) {
+		return boolLit{false}
+	}
+	return app{"<", []Term{a, b}, SortBool, false}
+}
+
+func Le(a, b Term) Term {
+	if x, y, ok := lit(a, b); ok {
+		return boolLit{x.Cmp(y) <= 0}
+	}
+	if same(a, b) {
+		return boolLit{true}
+	}
+	return app{"<=", []Term{a, b}, SortBool, false}
+}
+
+func Gt(a, b Term) Term { return Lt(b, a) }
+func Ge(a, b Term) Term { return Le(b, a) }
+
+func Eq(a, b Term) Term {
+	if a.Sort() == SortBool {
+		return Iff(a, b)
+	}
+	if x, y, ok := lit(a, b); ok {
+		return boolLit{x.Cmp(y) == 0}
+	}
+	if same(a, b) {
+		return boolLit{true}
+	}
+	return app{"=", []Term{a, b}, SortBool, false}
+}
+
+func Ne(a, b Term) Term { return Not(Eq(a, b)) }
+
+func Not(a Term) Term {
+	if b, ok := a.(boolLit); ok {
+		return boolLit{!b.v}
+	}
+	if n, ok := a.(app); ok && n.op == "not" {
+		return n.args[0]
+	}
+	return app{"not", []Term{a}, SortBool, false}
+}
+
+func And(ts ...Term) Term {
+	var args []Term
+	for _, t := range ts {
+		if b, ok := t.(boolLit); ok {
+			if !b.v {
+				return boolLit{false}
+			}
+			continue
+		}
+		if n, ok := t.(app); ok && n.op == "and" {
+			args = append(args, n.args...)
+			continue
+		}
+		args = append(args, t)
+	}
+	switch len(args) {
+	case 0:
+		return boolLit{true}
+	case 1:
+		return args[0]
+	}
+	return app{"and", args, SortBool, false}
+}
+
+func Or(ts ...Term) Term {
+	var args []Term
+	for _, t := range ts {
+		if b, ok := t.(boolLit); ok {
+			if b.v {
+				return boolLit{true}
+			}
+			continue
+		}
+		if n, ok := t.(app); ok && n.op == "or" {
+			args = append(args, n.args...)
+			continue
+		}
+		args = append(args, t)
+	}
+	switch len(args) {
+	case 0:
+		return boolLit{false}
+	case 1:
+		return args[0]
+	}
+	return app{"or", args, SortBool, false}
+}
+
+func Implies(a, b Term) Term {
+	if IsFalse(a) || IsTrue(b) {
+		return boolLit{true}
+	}
+	if IsTrue(a) {
+		return b
+	}
+	if IsFalse(b) {
+		return Not(a)
+	}
+	return app{"=>", []Term{a, b}, SortBool, false}
+}
+
+func Iff(a, b Term) Term {
+	if x, ok := a.(boolLit); ok {
+		if x.v {
+			return b
+		}
+		return Not(b)
+	}
+	if y, ok := b.(boolLit); ok {
+		if y.v {
+			return a
+		}
+		return Not(a)
+	}
+	if same(a, b) {
+		return boolLit{true}
+	}
+	return app{"=", []Term{a, b}, SortBool, false}
+}
+
+func Ite(c, t, e Term) Term {
+	if IsTrue(c) {
+		return t
+	}
+	if IsFalse(c) {
+		return e
+	}
+	if same(t, e) {
+		return t
+	}
+	if t.Sort() == SortBool {
+		if IsTrue(t) && IsFalse(e) {
+			return c
+		}
+		if IsFalse(t) && IsTrue(e) {
+			return Not(c)
+		}
+	}
+	return app{"ite", []Term{c, t, e}, t.Sort(), t.nonNeg() && e.nonNeg()}
+}
+
+// Max0 is max(0, a).
+func Max0(a Term) Term {
+	if a.nonNeg() {
+		return a
+	}
+	return app{"ite", []Term{Lt(a, zero), zero, a}, SortInt, true}
+}
+
+func Min(a, b Term) Term {
+	if x, y, ok := lit(a, b); ok {
+		if x.Cmp(y) <= 0 {
+			return a
+		}
+		return b
+	}
+	if same(a, b) {
+		return a
+	}
+	return app{"ite", []Term{Lt(a, b), a, b}, SortInt, a.nonNeg() && b.nonNeg()}
+}
+
+func Max(a, b Term) Term {
+	if x, y, ok := lit(a, b); ok {
+		if x.Cmp(y) >= 0 {
+			return a
+		}
+		return b
+	}
+	if same(a, b) {
+		return a
+	}
+	return app{"ite", []Term{Lt(a, b), b, a}, SortInt, a.nonNeg() || b.nonNeg()}
+}
diff --git a/internal/prove/testdata/cases/allotment.num b/internal/prove/testdata/cases/allotment.num
new file mode 100644
index 00000000..b88380b7
--- /dev/null
+++ b/internal/prove/testdata/cases/allotment.num
@@ -0,0 +1,7 @@
+send [USD/2 *] (
+  source = @src
+  destination = {
+    1/2 to @a
+    remaining to @b
+  }
+)
diff --git a/internal/prove/testdata/cases/allotment.num.expected b/internal/prove/testdata/cases/allotment.num.expected
new file mode 100644
index 00000000..1ae6def9
--- /dev/null
+++ b/internal/prove/testdata/cases/allotment.num.expected
@@ -0,0 +1,4 @@
+conserved: valid
+a_gets_rest: valid
+equal_split: counterexample
+negative_noop: valid
diff --git a/internal/prove/testdata/cases/allotment.num.props b/internal/prove/testdata/cases/allotment.num.props
new file mode 100644
index 00000000..069fa561
--- /dev/null
+++ b/internal/prove/testdata/cases/allotment.num.props
@@ -0,0 +1,5 @@
+prop conserved: success => received(@a, USD/2) + received(@b, USD/2) == sent(@src, USD/2)
+// flooring leaves the odd unit to the first share
+prop a_gets_rest: success => received(@a, USD/2) == sent(@src, USD/2) / 2 + sent(@src, USD/2) % 2
+prop equal_split: received(@a, USD/2) == received(@b, USD/2)
+prop negative_noop: before(@src, USD/2) < 0 => sent(@src, USD/2) == 0 and success
diff --git a/internal/prove/testdata/cases/capped-source.num b/internal/prove/testdata/cases/capped-source.num
new file mode 100644
index 00000000..358f4593
--- /dev/null
+++ b/internal/prove/testdata/cases/capped-source.num
@@ -0,0 +1,7 @@
+send [USD/2 100] (
+  source = {
+    max [USD/2 30] from @a
+    @b
+  }
+  destination = @dest
+)
diff --git a/internal/prove/testdata/cases/capped-source.num.expected b/internal/prove/testdata/cases/capped-source.num.expected
new file mode 100644
index 00000000..fa93d96a
--- /dev/null
+++ b/internal/prove/testdata/cases/capped-source.num.expected
@@ -0,0 +1,5 @@
+cap_respected: valid
+total: valid
+exact_a: valid
+via_moved: valid
+a_always_30: counterexample
diff --git a/internal/prove/testdata/cases/capped-source.num.props b/internal/prove/testdata/cases/capped-source.num.props
new file mode 100644
index 00000000..1c8a5091
--- /dev/null
+++ b/internal/prove/testdata/cases/capped-source.num.props
@@ -0,0 +1,5 @@
+prop cap_respected: success => sent(@a, USD/2) <= 30
+prop total: success => sent(@a, USD/2) + sent(@b, USD/2) == 100
+prop exact_a: success => sent(@a, USD/2) == min(30, max(0, before(@a, USD/2)))
+prop via_moved: success => moved(@a, @dest, USD/2) + moved(@b, @dest, USD/2) == 100
+prop a_always_30: sent(@a, USD/2) == 30
diff --git a/internal/prove/testdata/cases/hand-written.ir b/internal/prove/testdata/cases/hand-written.ir
new file mode 100644
index 00000000..2a665d6b
--- /dev/null
+++ b/internal/prove/testdata/cases/hand-written.ir
@@ -0,0 +1,11 @@
+  $asset = "USD/2"
+  set_current_asset($asset)
+  $zero = 0
+  $src = "src"
+  $cap = 100
+  $pulled = pull_account(account: $src, cap: $cap, overdraft: $zero)
+  $dest = "dest"
+  $thirty = 30
+  send_to_account(account: $dest, cap: $thirty)
+  $rest = "rest"
+  send_to_account(account: $rest)
diff --git a/internal/prove/testdata/cases/hand-written.ir.expected b/internal/prove/testdata/cases/hand-written.ir.expected
new file mode 100644
index 00000000..d276bc4d
--- /dev/null
+++ b/internal/prove/testdata/cases/hand-written.ir.expected
@@ -0,0 +1,3 @@
+dest_capped: valid
+rest_gets_the_rest: valid
+pulls_everything: counterexample
diff --git a/internal/prove/testdata/cases/hand-written.ir.props b/internal/prove/testdata/cases/hand-written.ir.props
new file mode 100644
index 00000000..5407dd6b
--- /dev/null
+++ b/internal/prove/testdata/cases/hand-written.ir.props
@@ -0,0 +1,3 @@
+prop dest_capped: received(@dest, USD/2) <= 30
+prop rest_gets_the_rest: received(@rest, USD/2) == sent(@src, USD/2) - received(@dest, USD/2)
+prop pulls_everything: sent(@src, USD/2) == 100
diff --git a/internal/prove/testdata/cases/kept.num b/internal/prove/testdata/cases/kept.num
new file mode 100644
index 00000000..cb7b28b1
--- /dev/null
+++ b/internal/prove/testdata/cases/kept.num
@@ -0,0 +1,7 @@
+send [USD/2 100] (
+  source = @src
+  destination = {
+    1/2 to @dest
+    remaining kept
+  }
+)
diff --git a/internal/prove/testdata/cases/kept.num.expected b/internal/prove/testdata/cases/kept.num.expected
new file mode 100644
index 00000000..b1c15fd5
--- /dev/null
+++ b/internal/prove/testdata/cases/kept.num.expected
@@ -0,0 +1,3 @@
+only_half_moves: valid
+but_needs_100: valid
+all_or_nothing: counterexample
diff --git a/internal/prove/testdata/cases/kept.num.props b/internal/prove/testdata/cases/kept.num.props
new file mode 100644
index 00000000..e0bfda61
--- /dev/null
+++ b/internal/prove/testdata/cases/kept.num.props
@@ -0,0 +1,3 @@
+prop only_half_moves: success => sent(@src, USD/2) == 50 and received(@dest, USD/2) == 50
+prop but_needs_100: before(@src, USD/2) == 60 => fails
+prop all_or_nothing: sent(@src, USD/2) == 100 or fails
diff --git a/internal/prove/testdata/cases/negative-amount.num b/internal/prove/testdata/cases/negative-amount.num
new file mode 100644
index 00000000..799d6fca
--- /dev/null
+++ b/internal/prove/testdata/cases/negative-amount.num
@@ -0,0 +1,4 @@
+send [USD/2 -5] (
+  source = @src
+  destination = @dest
+)
diff --git a/internal/prove/testdata/cases/negative-amount.num.expected b/internal/prove/testdata/cases/negative-amount.num.expected
new file mode 100644
index 00000000..1a611b30
--- /dev/null
+++ b/internal/prove/testdata/cases/negative-amount.num.expected
@@ -0,0 +1 @@
+rejected: valid
diff --git a/internal/prove/testdata/cases/negative-amount.num.props b/internal/prove/testdata/cases/negative-amount.num.props
new file mode 100644
index 00000000..53291daf
--- /dev/null
+++ b/internal/prove/testdata/cases/negative-amount.num.props
@@ -0,0 +1 @@
+prop rejected: fails
diff --git a/internal/prove/testdata/cases/oneof-source.num b/internal/prove/testdata/cases/oneof-source.num
new file mode 100644
index 00000000..1117b0f9
--- /dev/null
+++ b/internal/prove/testdata/cases/oneof-source.num
@@ -0,0 +1,6 @@
+#![feature("experimental-oneof")]
+
+send [USD/2 100] (
+  source = oneof { @a @b }
+  destination = @dest
+)
diff --git a/internal/prove/testdata/cases/oneof-source.num.expected b/internal/prove/testdata/cases/oneof-source.num.expected
new file mode 100644
index 00000000..1cf6289f
--- /dev/null
+++ b/internal/prove/testdata/cases/oneof-source.num.expected
@@ -0,0 +1,5 @@
+one_pays: valid
+first_wins: valid
+b_when_able: counterexample
+outcome: valid
+rewind_repaid: valid
diff --git a/internal/prove/testdata/cases/oneof-source.num.props b/internal/prove/testdata/cases/oneof-source.num.props
new file mode 100644
index 00000000..2f8947cb
--- /dev/null
+++ b/internal/prove/testdata/cases/oneof-source.num.props
@@ -0,0 +1,6 @@
+prop one_pays: success => (sent(@a, USD/2) == 100 and sent(@b, USD/2) == 0) or (sent(@a, USD/2) == 0 and sent(@b, USD/2) == 100)
+prop first_wins: before(@a, USD/2) >= 100 => sent(@a, USD/2) == 100
+prop b_when_able: before(@b, USD/2) >= 100 => sent(@b, USD/2) == 100
+prop outcome: success <=> (before(@a, USD/2) >= 100 or before(@b, USD/2) >= 100)
+// a branch that fell short is rewound: what it pulled goes back
+prop rewind_repaid: before(@a, USD/2) == 50 and before(@b, USD/2) >= 100 => after(@a, USD/2) == 50
diff --git a/internal/prove/testdata/cases/save-then-send.num b/internal/prove/testdata/cases/save-then-send.num
new file mode 100644
index 00000000..0f445d7f
--- /dev/null
+++ b/internal/prove/testdata/cases/save-then-send.num
@@ -0,0 +1,6 @@
+save [USD/2 50] from @src
+
+send [USD/2 100] (
+  source = @src
+  destination = @dest
+)
diff --git a/internal/prove/testdata/cases/save-then-send.num.expected b/internal/prove/testdata/cases/save-then-send.num.expected
new file mode 100644
index 00000000..f6a0fd00
--- /dev/null
+++ b/internal/prove/testdata/cases/save-then-send.num.expected
@@ -0,0 +1,3 @@
+needs_150: valid
+hundred_enough: counterexample
+keeps_saved: valid
diff --git a/internal/prove/testdata/cases/save-then-send.num.props b/internal/prove/testdata/cases/save-then-send.num.props
new file mode 100644
index 00000000..fa95ba5e
--- /dev/null
+++ b/internal/prove/testdata/cases/save-then-send.num.props
@@ -0,0 +1,3 @@
+prop needs_150: success => before(@src, USD/2) >= 150
+prop hundred_enough: before(@src, USD/2) >= 100 => success
+prop keeps_saved: success => after(@src, USD/2) >= 50
diff --git a/internal/prove/testdata/cases/send-all.num b/internal/prove/testdata/cases/send-all.num
new file mode 100644
index 00000000..5bb9c853
--- /dev/null
+++ b/internal/prove/testdata/cases/send-all.num
@@ -0,0 +1,4 @@
+send [USD/2 *] (
+  source = @src
+  destination = @dest
+)
diff --git a/internal/prove/testdata/cases/send-all.num.expected b/internal/prove/testdata/cases/send-all.num.expected
new file mode 100644
index 00000000..45ee8459
--- /dev/null
+++ b/internal/prove/testdata/cases/send-all.num.expected
@@ -0,0 +1,3 @@
+drains: valid
+ends_empty: counterexample
+never_fails: valid
diff --git a/internal/prove/testdata/cases/send-all.num.props b/internal/prove/testdata/cases/send-all.num.props
new file mode 100644
index 00000000..084a4c46
--- /dev/null
+++ b/internal/prove/testdata/cases/send-all.num.props
@@ -0,0 +1,3 @@
+prop drains: before(@src, USD/2) >= 0 => sent(@src, USD/2) == before(@src, USD/2)
+prop ends_empty: after(@src, USD/2) == 0
+prop never_fails: success
diff --git a/internal/prove/testdata/cases/simple-send.num b/internal/prove/testdata/cases/simple-send.num
new file mode 100644
index 00000000..c6d44459
--- /dev/null
+++ b/internal/prove/testdata/cases/simple-send.num
@@ -0,0 +1,4 @@
+send [USD/2 100] (
+  source = @src
+  destination = @dest
+)
diff --git a/internal/prove/testdata/cases/simple-send.num.expected b/internal/prove/testdata/cases/simple-send.num.expected
new file mode 100644
index 00000000..218a0ad6
--- /dev/null
+++ b/internal/prove/testdata/cases/simple-send.num.expected
@@ -0,0 +1,7 @@
+enough_means_success: valid
+dest_credited: valid
+src_never_negative: counterexample
+src_not_negative_on_success: valid
+conservation: valid
+moved_all: valid
+fails_below_100: valid
diff --git a/internal/prove/testdata/cases/simple-send.num.props b/internal/prove/testdata/cases/simple-send.num.props
new file mode 100644
index 00000000..d15fc087
--- /dev/null
+++ b/internal/prove/testdata/cases/simple-send.num.props
@@ -0,0 +1,9 @@
+// the canonical first lesson: a failed run keeps every balance as it was,
+// so a property about the outcome needs the `success =>` guard
+prop enough_means_success: before(@src, USD/2) >= 100 => success
+prop dest_credited: success => after(@dest, USD/2) == before(@dest, USD/2) + 100
+prop src_never_negative: after(@src, USD/2) >= 0
+prop src_not_negative_on_success: success => after(@src, USD/2) >= 0
+prop conservation: delta(@src, USD/2) + delta(@dest, USD/2) == 0
+prop moved_all: success => moved(@src, @dest, USD/2) == 100
+prop fails_below_100: before(@src, USD/2) < 100 => fails
diff --git a/internal/prove/testdata/cases/uses-vars.num b/internal/prove/testdata/cases/uses-vars.num
new file mode 100644
index 00000000..04bf4497
--- /dev/null
+++ b/internal/prove/testdata/cases/uses-vars.num
@@ -0,0 +1,8 @@
+vars {
+  account $dest
+}
+
+send [USD/2 100] (
+  source = @src
+  destination = $dest
+)
diff --git a/internal/prove/testdata/cases/uses-vars.num.expected b/internal/prove/testdata/cases/uses-vars.num.expected
new file mode 100644
index 00000000..b94aea8f
--- /dev/null
+++ b/internal/prove/testdata/cases/uses-vars.num.expected
@@ -0,0 +1 @@
+unsupported: script variables are not supported
diff --git a/internal/prove/testdata/cases/uses-vars.num.props b/internal/prove/testdata/cases/uses-vars.num.props
new file mode 100644
index 00000000..897b3d1b
--- /dev/null
+++ b/internal/prove/testdata/cases/uses-vars.num.props
@@ -0,0 +1 @@
+prop whatever: success
diff --git a/internal/prove/testdata/cases/vacuous.num b/internal/prove/testdata/cases/vacuous.num
new file mode 100644
index 00000000..bcc316bc
--- /dev/null
+++ b/internal/prove/testdata/cases/vacuous.num
@@ -0,0 +1,7 @@
+send [USD/2 100] (
+  source = {
+    2/3 from @a
+    2/3 from @b
+  }
+  destination = @dest
+)
diff --git a/internal/prove/testdata/cases/vacuous.num.expected b/internal/prove/testdata/cases/vacuous.num.expected
new file mode 100644
index 00000000..c8ff78b4
--- /dev/null
+++ b/internal/prove/testdata/cases/vacuous.num.expected
@@ -0,0 +1,2 @@
+anything: valid
+never_succeeds: valid
diff --git a/internal/prove/testdata/cases/vacuous.num.props b/internal/prove/testdata/cases/vacuous.num.props
new file mode 100644
index 00000000..2090f98e
--- /dev/null
+++ b/internal/prove/testdata/cases/vacuous.num.props
@@ -0,0 +1,4 @@
+// the portions never sum to 1, so no run succeeds and anything guarded by
+// `success =>` holds; the report's "success reachable: no" is the tell
+prop anything: success => received(@dest, USD/2) == 1_000_000
+prop never_succeeds: fails
diff --git a/internal/prove/testdata/cases/world-source.num b/internal/prove/testdata/cases/world-source.num
new file mode 100644
index 00000000..6e302c68
--- /dev/null
+++ b/internal/prove/testdata/cases/world-source.num
@@ -0,0 +1,4 @@
+send [USD/2 100] (
+  source = @world
+  destination = @dest
+)
diff --git a/internal/prove/testdata/cases/world-source.num.expected b/internal/prove/testdata/cases/world-source.num.expected
new file mode 100644
index 00000000..db237cef
--- /dev/null
+++ b/internal/prove/testdata/cases/world-source.num.expected
@@ -0,0 +1,3 @@
+always: valid
+world_debited: valid
+world_positive: counterexample
diff --git a/internal/prove/testdata/cases/world-source.num.props b/internal/prove/testdata/cases/world-source.num.props
new file mode 100644
index 00000000..937cc3ab
--- /dev/null
+++ b/internal/prove/testdata/cases/world-source.num.props
@@ -0,0 +1,3 @@
+prop always: success
+prop world_debited: after(@world, USD/2) == before(@world, USD/2) - 100
+prop world_positive: after(@world, USD/2) >= 0
diff --git a/prove.md b/prove.md
new file mode 100644
index 00000000..f693d5c8
--- /dev/null
+++ b/prove.md
@@ -0,0 +1,300 @@
+# The numscript prover
+
+`numscript prove` checks a boolean property about one script for every initial balance and answers `valid`, `counterexample` or `unknown`. The script is compiled to the IR (see [ir-textual-format.md](ir-textual-format.md)), the IR is encoded into one quantifier-free SMT problem, and an external solver decides it. Everything lives under [internal/prove/](internal/prove/).
+
+## What it proves, and what it does not
+
+A property is a formula over the quantities of one run: the initial balance of each (account, asset) pair, the totals moved during the run, and whether the run succeeded. The prover checks it for every assignment of initial balances, unbounded integers with negatives included, not for a sample. The answer is one of three: `valid` (no initial balance falsifies the property), `counterexample` (concrete initial balances on which the property is false, replayed through the real VM before being reported), or `unknown` (the solver hit its time limit).
+
+The model carries the run outcome, success or the first failing instruction and its kind, and per (account, asset) pair three totals: `sent`, the sum of postings out of the account, `received`, the sum of postings into it, and `moved(a→b)`, the sum of postings from `a` to `b`. `after` is defined as `before + received − sent`. What a property cannot name is not modeled: the number, order or shape of the postings, metadata, script variables, asset colors, scopes and asset scaling. The exact rejection list is `prescan` in [internal/prove/encode/encode.go](internal/prove/encode/encode.go) and is reproduced in [Supported scripts](#supported-scripts-v1).
+
+| | |
+| --- | --- |
+| checked for | every initial balance of every (account, asset) pair the script or the property names, any integer |
+| answers | `valid`; `counterexample` with initial balances the VM confirms; `unknown` on solver timeout |
+| modeled | success or which instruction fails and why; `before`, `sent`, `received`, `moved`, `after` per pair |
+| not modeled | posting list shape and order, metadata, script vars, colors, scopes, scaling |
+
+## Pipeline and where things live
+
+A `.num` file is parsed and lowered with `compiler.CompileToIR`; a `.ir` file is read with `ir.Parse`. `encode.Encode` first runs `ir.Typecheck`, `ir.Assemble` and `vm.Verify` on the stream, so every register read is defined, every jump is forward and marks balance on every path, then emits one SMT-LIB2 model of the run. For each property, `prop.Lower` turns the formula into a Bool term, its negation is asserted on top of the model, and the solver subprocess answers `(check-sat)`. `unsat` is `valid`. `sat` comes with a model: the initial balances are read off it, `encode.Replay` runs the same IR on `vm.Exec` against a static store holding those balances, `encode.Compare` checks every output of the model against the VM, and `prop.Eval` evaluates the formula on the VM run. Only when the VM agrees and the formula is false on it is the result a `counterexample`.
+
+| what | where |
+| --- | --- |
+| `.num` → `[]ir.Instr` | `compiler.CompileToIR` in [internal/compiler/compiler.go](internal/compiler/compiler.go) |
+| `.ir` → `[]ir.Instr` | `ir.Parse` in [internal/ir/parse.go](internal/ir/parse.go) |
+| precondition on the IR | `ir.Typecheck`, `ir.Assemble`, `vm.Verify`, called at the top of `encode.Encode` |
+| IR → SMT model | `encode.Encode` in [internal/prove/encode/encode.go](internal/prove/encode/encode.go); merging at labels in `state.go`, strings and portions in `values.go`, pull/send/save/balance/marks in `funds.go`, outputs and `UnsupportedError` in `problem.go` |
+| property text → AST | `prop.ParseFile`, `prop.ParseInline` in [internal/prove/prop/parser.go](internal/prove/prop/parser.go), tokens in `lexer.go` |
+| AST checks | `prop.Typecheck`, `prop.Atoms` in [internal/prove/prop/typecheck.go](internal/prove/prop/typecheck.go) |
+| AST → SMT term; AST on concrete values | `prop.Lower` in `lower.go`; `prop.Eval` in `eval.go` |
+| terms with folding, printer, script, solver driver, evaluator | [internal/prove/smt/](internal/prove/smt/) (`term.go`, `print.go`, `script.go`, `solver.go`, `eval.go`) |
+| counterexample replay | `encode.Replay`, `encode.Compare` in [internal/prove/encode/replay.go](internal/prove/encode/replay.go) |
+| orchestration, statuses, exit codes, reports | `prove.Check` in [internal/prove/prove.go](internal/prove/prove.go), `result.go`, `report.go` |
+| CLI | `numscript prove` in [internal/cmd/prove.go](internal/cmd/prove.go), `numscript ir` in [internal/cmd/ir.go](internal/cmd/ir.go) |
+| fixtures | [internal/prove/testdata/cases/](internal/prove/testdata/cases/): `<name>.num` or `<name>.ir`, plus `.props` and `.expected` |
+
+Both commands are registered as hidden experimental commands in `internal/cmd/root.go`: they always run, and `NUMSCRIPT_EXPERIMENTAL_CLI=1` lists them in `--help`. `numscript ir <file.num> [-o path]` prints the IR the prover sees, with `-` for stdin, so `numscript ir x.num | numscript assemble -` also works.
+
+## The property language
+
+### Lexical structure
+
+| token | form | notes |
+| --- | --- | --- |
+| ACCOUNT | `@` then segments of `[a-zA-Z0-9_-]+` joined by `:` | as numscript: `@src`, `@users:001`, `@a-b` |
+| ASSET | `[A-Z][A-Z0-9]*` optionally `/[0-9]+` | as numscript: `USD/2`, `COIN` |
+| INT | `[0-9]+` with `_` between digit groups | `1_000_000`; no sign, `-` is an operator |
+| NAME | `[a-z_][a-z0-9_]*` | keywords and property names |
+| operators | `( ) , : + - * / % == != < <= > >= => <=>` | a lone `=` is "unexpected character '='" |
+| comments | `//` to end of line, `/* ... */` | an unterminated block comment is an error |
+
+Whitespace and newlines are insignificant. Keywords: `before after sent received moved delta success fails and or not true false prop min max`. Three token kinds are lexed only to be rejected with a pointed message: `$name` ("script variables are not supported in properties yet"), `"string"` ("strings are not supported in properties"), and `[` where an expression is expected ("monetary literals are not allowed in properties; amounts are plain integers in the asset's minor unit: write 100"). The names `forall exists in accounts assets` ("quantifiers are not supported yet"), `sum` ("sums are not supported yet") and `meta` ("metadata is not supported yet") are reserved the same way.
+
+### Grammar
+
+```
+file        = { "prop" NAME ":" formula } ;
+inline      = [ NAME ":" ] formula ;                  the --prop form
+formula     = iff ;
+iff         = implies [ "<=>" implies ] ;             non-associative
+implies     = disj [ "=>" implies ] ;                 right-associative
+disj        = conj { "or" conj } ;
+conj        = negation { "and" negation } ;
+negation    = "not" negation | comparison ;
+comparison  = sum [ ("==" | "!=" | "<" | "<=" | ">" | ">=") sum ] ;   non-associative
+sum         = term { ("+" | "-") term } ;
+term        = unary { ("*" | "/" | "%") unary } ;
+unary       = "-" unary | primary ;
+primary     = INT | "true" | "false" | "success" | "fails" | "(" formula ")"
+            | ("before" | "after" | "sent" | "received" | "delta") "(" ACCOUNT "," ASSET ")"
+            | "moved" "(" ACCOUNT "," ACCOUNT "," ASSET ")"
+            | ("min" | "max") "(" sum "," sum { "," sum } ")" ;
+```
+
+| level | operators | associativity |
+| --- | --- | --- |
+| 1 (loosest) | `<=>` | none: `a <=> b <=> c` is an error, write `(a <=> b) <=> c` |
+| 2 | `=>` | right: `a => b => c` is `a => (b => c)` |
+| 3 | `or` | left |
+| 4 | `and` | left |
+| 5 | `not` | prefix, over one comparison: `not a < b` is `not (a < b)` |
+| 6 | `== != < <= > >=` | none: `1 < 2 < 3` is an error, write `(1 < 2) and (2 < 3)` |
+| 7 | `+ -` | left |
+| 8 | `* / %` | left |
+| 9 (tightest) | unary `-` | prefix |
+
+### Atoms
+
+| atom | type | value |
+| --- | --- | --- |
+| `before(@a, X)` | int | initial balance of `a` in `X` |
+| `after(@a, X)` | int | `before + received − sent` |
+| `sent(@a, X)` | int | total posted out of `a` in `X` |
+| `received(@a, X)` | int | total posted into `a` in `X` |
+| `moved(@a, @b, X)` | int | total posted from `a` to `b` in `X` |
+| `delta(@a, X)` | int | sugar for `after(@a, X) - before(@a, X)` |
+| `success`, `fails` | bool | the run committed / aborted; each is the negation of the other |
+| `min(x, y, ...)`, `max(x, y, ...)` | int | at least two integer arguments |
+
+Arithmetic is linear. `*` needs a literal operand, `/` and `%` a positive literal divisor, where a literal is any atom-free constant expression (`2 * 3 * sent(@a, USD/2)` and `sent(@a, USD/2) / min(2, 3)` typecheck). The messages are "multiplication must have a literal operand (linear arithmetic only)", "division must be by a positive literal" and "modulo must be by a positive literal". `/` and `%` are Euclidean, like SMT-LIB `div`/`mod` and Go's `big.Int.Div`/`Mod`: `-7 / 2 == -4` and `-7 % 2 == 1`, the remainder is never negative. Amounts are plain integers in the asset's minor unit, `100` where numscript writes `[USD/2 100]`; a monetary literal is rejected. The formula must be boolean, and the typechecker reports every sort error ("expected a boolean expression, found an integer", "expected an integer expression, found a boolean").
+
+An account or asset the script never names is a typecheck error listing the known ones: `account @dset is not referenced by the script (known: @dest, @src, @world)`, `asset EUR/2 is not referenced by the script (known: USD/2)`. It is an error and not a silent zero because a pair the script never touches has `sent == received == 0` and `after == before` by construction, so a property about it is either trivially true or a typo.
+
+### Files and inline properties
+
+A `.props` file is a sequence of `prop name: formula`, comments anywhere; names must be unique ("property "a" is defined twice"), and an empty file is "no properties found". `--prop "[name:] formula"` is one property; without a name it is called `prop1`, `prop2`, ... in order. `--prop` and `--props` combine; with neither, `<script>.props` next to the script is read (`simple-send.num.props` for `simple-send.num`).
+
+Errors print `line:col: msg` (1-based) followed by the source excerpt from `parser.Range.ShowOnSource`, prefixed with the file path for a `.props` file and with `--prop[N]` for the N-th inline property:
+
+```
+--prop[1]: 1:12: expected an asset but found '['
+  0 | sent(@src, [USD/2 100]) == 0
+    |            ~
+```
+
+The command then prints `invalid property` (or `invalid properties file`) and exits 3. Typecheck errors, unknown accounts or assets, nonlinear arithmetic and sort errors, are found after encoding and print as `property "name": line:col: msg` without an excerpt.
+
+## Semantics of a run
+
+For initial balances `B`:
+
+| atom | run succeeds | run fails |
+| --- | --- | --- |
+| `before(@a, X)` | `B(a, X)` | `B(a, X)` |
+| `sent(@a, X)` | Σ postings out of `a` in `X` | 0 |
+| `received(@a, X)` | Σ postings into `a` in `X` | 0 |
+| `moved(@a, @b, X)` | Σ postings `a → b` in `X` | 0 |
+| `after(@a, X)` | `before − sent + received` | `before` |
+| `delta(@a, X)` | `after − before` | 0 |
+| `success` / `fails` | true / false | false / true |
+
+A failed run applies nothing. The ledger commits a transaction or rejects it whole, so on failure every balance stays as it was and every total is 0. For `send [USD/2 100]` from `@src` to `@dest`, `after(@dest, USD/2) == before(@dest, USD/2) + 100` has the counterexample `before(@src) == -1` (the run fails, nothing moves); `success => after(@dest, USD/2) == before(@dest, USD/2) + 100` is the property about the committed run, and `before(@src, USD/2) >= 100 => success` the one about when it commits (`simple-send.num`).
+
+A self-transfer counts on both sides: a posting `a → a` adds to `sent(@a)`, `received(@a)` and `moved(@a, @a, X)`, and leaves `after(@a)` unchanged.
+
+`kept` funds are refunded, not sent. `remaining kept` returns the undistributed remainder to its source before the run ends, so `sent(@src)` counts only what reached a destination. In `kept.num` (`send [USD/2 100]`, `1/2 to @dest`, `remaining kept`) `success => sent(@src, USD/2) == 50` and `before(@src, USD/2) == 60 => fails` are both valid: 50 moves, but 100 must be available.
+
+`save` only reserves. It lowers what a later `pull_account` or `balance()` sees, it is never a posting, so `after` ignores it. In `save-then-send.num` (`save [USD/2 50] from @src`, then `send [USD/2 100]` from `@src`) `success => before(@src, USD/2) >= 150` is valid and `before(@src, USD/2) >= 100 => success` has the counterexample `before(@src) == 100`.
+
+Negative initial balances are in the universe. A `pull_account` with overdraft 0 sees `max(0, balance)`, so a negative balance sources nothing, but it is still a balance the property is checked on: `after(@src, USD/2) >= 0` is false at `before(@src) == -1` because the run fails and `after == before`. Exclude them with an antecedent, `before(@src, USD/2) >= 0 => ...`, as `send-all.num`'s `drains` does.
+
+Properties in a file are independent checks: each is its own `check-sat`, and none assumes another.
+
+Vacuity: `success => φ` is valid for every φ when no initial balance makes the run succeed. `vacuous.num` sends `2/3 from @a` and `2/3 from @b`, which fails `assert_leftover` on every balance, so `success => received(@dest, USD/2) == 1_000_000` is valid. The report header's `success reachable: no` is the tell; it also says whether failure is reachable (`allotment.num` and `send-all.num` never fail).
+
+Three more fixtures show the atoms at work. `capped-source.num` (`send [USD/2 100]` from `max [USD/2 30] from @a` then `@b`, to `@dest`): `success => sent(@a, USD/2) == min(30, max(0, before(@a, USD/2)))` and `success => moved(@a, @dest, USD/2) + moved(@b, @dest, USD/2) == 100` are valid; `sent(@a, USD/2) == 30` has the counterexample `before(@a) == -1, before(@b) == -1`, where the run fails and `sent(@a) == 0`. `oneof-source.num` (`source = oneof { @a @b }`): `success <=> (before(@a, USD/2) >= 100 or before(@b, USD/2) >= 100)` and `before(@a, USD/2) >= 100 => sent(@a, USD/2) == 100` are valid, `before(@b, USD/2) >= 100 => sent(@b, USD/2) == 100` is refuted at `before(@a) == 100, before(@b) == 101` (the first branch that can pay wins), and `before(@a, USD/2) == 50 and before(@b, USD/2) >= 100 => after(@a, USD/2) == 50` is valid because the 50 pulled from `@a` on the branch that fell short is repaid by `mark_rewind`. `allotment.num` (`send [USD/2 *]` from `@src`, `1/2 to @a`, `remaining to @b`): `success => received(@a, USD/2) == sent(@src, USD/2) / 2 + sent(@src, USD/2) % 2` is valid, each share being floored and the missing unit added back to the first clause, and `received(@a, USD/2) == received(@b, USD/2)` is refuted at `before(@src) == 3` (`@a` gets 2, `@b` gets 1).
+
+## Supported scripts (v1)
+
+Supported IR: int, string and bool constants; `add_int`, `sub_int`, `$d += $r`, `$d -= $r`, `neg_int`, `lt_int`, `eq_int`, `is_zero`, `not`; the four copies; `add_string`, `str_eq`, `int_to_string`, `portion_to_string`, `monetary_to_string` (a string is tracked as a constant when its inputs are); `mk_portion`, `add_portion`, `sub_portion`, `mul_portion`, `lt_portion`, `eq_portion`, `int_to_portion`, `portion_to_int`; `jmp`, `jmp_if_true`, `jmp_if_false` and labels; `set_current_asset`, `pull_account`, `send_to_account`, `save`, `balance`; `mark_push`, `mark_commit`, `mark_rewind`; `check_enough_funds`, `assert_non_negative_amount`, `assert_non_negative_balance`, `assert_non_negative_portion`, `assert_leftover`, `assert_leftover_exact`, `assert_same_asset`, `assert_valid_account`. In numscript terms: `send` with literal amounts and `*`; sources `@account`, `@world`, `max [..] from`, inorder blocks, `oneof` (behind its feature flag, which the script declares itself), allotments with literal portions and `remaining`; destinations with inorder, allotments and `kept`; `save`; `balance()` and arithmetic in amounts.
+
+Ignored: `set_tx_meta`, `set_account_meta`. They change no balance.
+
+Rejected with `UnsupportedError{Index, Text, Reason}`, printed as `cannot prove: unsupported instruction N `text`: reason`, exit 3. `prescan` walks the program in text order before encoding and names the first hit, reachable or not:
+
+| instruction | reason |
+| --- | --- |
+| `load_var<int>`, `load_var<str>` | script variables are not supported |
+| `meta<str>`, `meta<int>`, `meta<portion>`, `meta_monetary` | metadata reads are not supported |
+| `assert_valid_color`; a `color:` operand on `pull_account` | asset colors are not supported |
+| `assert_valid_scope`, `assert_unscoped`; a `scope:` operand on `pull_account`, `send_to_account`, `save`, `balance` | scoped accounts are not supported |
+
+The pass itself rejects what it cannot keep linear or constant:
+
+| situation | reason |
+| --- | --- |
+| a non-constant string reaches an account or asset operand, `str_eq`, `assert_same_asset` or `assert_valid_account` | the value of string register $rN is not a constant |
+| `set_current_asset` of a non-constant, then a pull, send or rewind | the current asset is not a constant |
+| `mul_portion` of two non-constant portions | nonlinear portion arithmetic |
+| `mk_portion` with a non-constant denominator | nonlinear portion arithmetic: the denominator is not a constant |
+| a string register, a portion register or the current asset holding different constants on paths that join at a label | string register $rN takes different values on joining paths (likewise `portion register`, `the current asset differs`) |
+| more than 255 live registers in one bank, or a program too large to assemble | the `ir.Assemble` error text, at index -1 |
+| any other instruction | not modeled |
+
+The compiler never emits the joining-paths cases from numscript. Asset scaling is rejected by the compiler (`feature not implemented: scaling`) before the prover sees it.
+
+The known accounts and assets, which the typechecker holds property atoms to, are collected syntactically: `prescan` follows string constants through `str_copy` and `add_string` in text order, ignoring jumps, and records every (account, asset) pair reaching a `pull_account`, `send_to_account`, `save` or `balance` operand (the current asset for pulls and sends, the explicit asset operand for `save` and `balance`); the pass adds whatever it touches. An account on a branch the model folds away, such as a run that always fails before reaching it, is still known.
+
+## Quantifiers
+
+The implicit universal over initial balances is the whole meaning of "holds". Every `before(@a, X)` is a free `Int`; the prover asserts `model ∧ ¬φ` and asks whether it is satisfiable. `unsat` means no balance falsifies φ; a model is one concrete counterexample. The user never writes this quantifier.
+
+Over accounts and assets: possible without SMT quantifiers, useful, not in v1. Without vars the touched (account, asset) set is finite and fixed at encode time, so `forall @x in accounts: ψ` is a finite conjunction over it, `exists` a finite disjunction, each plus one "untouched" witness whose delta is 0, and `sum(@x in accounts: delta(@x, USD/2)) == 0` is a finite sum. The two properties that want this, conservation and "nobody but @world ends negative", are aggregates over that set. The syntax is reserved (`forall exists sum in accounts assets`) and the report header prints the touched set, so the hand-written expansion is easy today: `simple-send.num`'s `conservation` is `delta(@src, USD/2) + delta(@dest, USD/2) == 0`.
+
+Over integers: possible in principle, quantified linear integer arithmetic is decidable, and not needed. The implicit universal already covers "for any balance", and an existential over an amount is a fresh free variable. The cost would be robustness: a quantified problem leaves `QF_LIA`, and `unknown` stops meaning "timeout".
+
+With vars later: account-typed vars make the touched set symbolic. The finite expansion survives by case-splitting on aliasing, `$dest` is one of the k literal accounts or a fresh (k+1)-th, which is also why an SMT quantifier will still not be needed then.
+
+v1 ships only the implicit universal.
+
+## Reading the output
+
+`numscript prove internal/prove/testdata/cases/simple-send.num`:
+
+```
+internal/prove/testdata/cases/simple-send.num: touches @dest, @src in USD/2; success reachable: yes; failure reachable: yes
+
+  ✓ enough_means_success         valid          10ms
+  ✓ dest_credited                valid          8ms
+  × src_never_negative           counterexample 8ms
+  ✓ src_not_negative_on_success  valid          8ms
+  ✓ conservation                 valid          6ms
+  ✓ moved_all                    valid          6ms
+  ✓ fails_below_100              valid          6ms
+
+× src_never_negative: after(@src, USD/2) >= 0
+  initial balances:
+    | Account | Asset | Balance |
+    | dest    | USD/2 | 0       |
+    | src     | USD/2 | -1      |
+  outcome: fails at instruction 20 `check_enough_funds($r9, $r2)`: missing funds
+  atoms:
+    after(@src, USD/2) = -1
+
+6 valid, 1 counterexample
+```
+
+The header names the touched accounts and assets and answers two extra `check-sat`s, the model with `success` asserted and with `fails` asserted (`yes`, `no`, or `unknown` when the solver could not tell). Then one line per property with its status and the solver plus replay time, one block per property that is neither valid nor unknown, and the counts. A counterexample block shows the formula, the initial balances of every pair the model knows (property-only pairs included), the outcome (`success`, or the failing IR instruction and the failure kind), and the value of each atom of the formula on the VM run.
+
+| status | icon | meaning | exit |
+| --- | --- | --- | --- |
+| `valid` | ✓ | `unsat`: no initial balance falsifies the property | 0 |
+| `counterexample` | × | `sat`; the VM replay agrees with the model on outcome and every total, and the property is false on the VM run | 1 |
+| `unknown` | ? | the solver answered `unknown` (its time limit) | 2 |
+| `tool-bug` | ! | the model and the VM disagree, or the property is true on the VM run: a bug in the prover, never a finding about the script | 3 |
+| `solver-error` | ! | the solver could not be run or rejected the problem | 3 |
+
+The exit code is the worst status over all properties. A `tool-bug` block prints "the prover's model does not match the vm; this is a bug in the prover, not in the script:" followed by each disagreement (`sent(@a,USD/2): model 30, vm 0`) or "the property holds on the vm run". Errors before any check (an unsupported script, an invalid property, no properties, a missing solver) go to stderr with exit 3.
+
+`-o json` renders the same report for machines (trimmed here to two results):
+
+```json
+{
+  "script": "internal/prove/testdata/cases/simple-send.num",
+  "accounts": ["dest", "src"],
+  "assets": ["USD/2"],
+  "successReachable": true,
+  "failureReachable": true,
+  "results": [
+    { "name": "dest_credited", "formula": "success => after(@dest, USD/2) == before(@dest, USD/2) + 100", "status": "valid", "durationMs": 8 },
+    {
+      "name": "src_never_negative", "formula": "after(@src, USD/2) >= 0", "status": "counterexample", "durationMs": 8,
+      "counterexample": {
+        "balances": [ { "account": "dest", "asset": "USD/2", "amount": 0 }, { "account": "src", "asset": "USD/2", "amount": -1 } ],
+        "outcome": "fails",
+        "failure": { "kind": "missing funds", "instruction": 20 },
+        "atoms": { "after(@src, USD/2)": "-1" }
+      }
+    }
+  ]
+}
+```
+
+`successReachable`/`failureReachable` are `null` when unknown; `failure` is present only when `outcome` is `"fails"`; balance amounts are JSON numbers, atom values are strings; a `tool-bug` result carries `modelVmDiffs`, and a solver or replay error carries `error`.
+
+Flags: `--prop` (repeatable) and `--props <file>`; `--solver z3|cvc5|<path>` (default `z3`; the executable's basename picks the arguments, `z3 -in -smt2 -t:<ms>` or `cvc5 --lang smt2 --tlimit=<ms>`, and any other executable is run with no arguments and must read SMT-LIB2 on stdin); `--timeout` (default `10s` per property, passed as the solver's own soft limit so it answers `unknown` instead of dying, with the process killed 2 s later; `0` disables both); `--emit-smt <dir>` writes each property's complete problem to `<dir>/<name>.smt2`, `--emit-smt -` prints them to stdout under `; ---- <name>` headers. The emitted text ends at `(assert (not property))`; append `(check-sat)` to reproduce a verdict outside the tool.
+
+## How the encoding works
+
+Every initial balance is a free `Int` named `|before(@src,USD/2)|`. The IR has only forward jumps, so text order is execution order and one pass over the instructions suffices: each state write (a register, a running balance, a queue slot, a total) becomes a `define-fun` named after what it writes and the instruction index, `$r9@18` or `|bal(@src,USD/2)@18|`, so the script is a DAG that reads like the IR. A conditional jump clones the state with the condition conjoined into its reach guard and parks the clone on the target label; a label merges the fallthrough and the parked edges, every differing value becoming an `ite` chain over the edges' reach guards. Constant folding in the term constructors is load-bearing: `str_eq("src", "world")` folds to `false`, which kills the `@world` arm outright, and `lt_int(0, 100)` folds to `true`, which collapses the `max(0, amount)` diamond, so the simple send has no merge at all.
+
+`pull_account` with an overdraft reads `available = max(0, balance + max(0, overdraft))` and takes `available`, or `max(0, cap)` when the cap is smaller; without an overdraft (the `@world` arm) it takes `max(0, cap)` without reading any balance; with neither it is an unconditional failure. What it takes becomes a queue slot and is subtracted from the running balance. `send_to_account` drains the slots in pull order, each `take = ite(rem > 0, min(slot, rem), 0)` for a capped send and the whole slot otherwise, and adds the takes to `sent` of the slot's account, `received` of the destination and `moved(a→d)`; a send without a destination (`kept`) refunds the takes to the running balances and touches no total. `save` clamps the running balance (`max(0, bal − amount)`, or `min(bal, 0)` for `save all`) and nothing else; `balance` reads the running balance. `mark_push` opens a region and `mark_rewind` repays every slot pulled inside it, guarded by which push opened the region when a region's end is reached from several pushes (`oneof`). A failing instruction defines a flag `fail@20 = alive ∧ cond` and continues with `alive ∧ ¬cond`, so the flags of different sites are never true together and the counterexample names the first failure; `fails` is their disjunction and every output is masked by it: `sent(k) = ite(fails, 0, …)`, `after(k) = before(k) + (received(k) − sent(k))`. Portions are exact rational linear forms over Int terms, `c₁·t₁ + … + c₀` with rational coefficients, so `mul_portion` by a constant, `add_portion` and comparisons stay linear and `portion_to_int` is `(div (D·form) D)` with `D` the common denominator; the whole problem is `QF_LIA`.
+
+The compiled `send [USD/2 10] (source = @src destination = @dest)` has the overdraft pull at index 18, `check_enough_funds($r9, $r2)` at 20 and `send_to_account(account: $r10)` at 22, and encodes to exactly this (`internal/prove/encode/__snapshots__/encode_test.snap`):
+
+```smt2
+(set-logic QF_LIA)
+(set-option :produce-models true)
+(declare-const |before(@dest,USD/2)| Int)
+(declare-const |before(@src,USD/2)| Int)
+; 18: $r9 = pull_account(account: $r6, cap: $r4, overdraft: $r7)
+(define-fun available@18 () Int (ite (< |before(@src,USD/2)| 0) 0 |before(@src,USD/2)|))
+(define-fun $r9@18 () Int (ite (< 10 available@18) 10 available@18))
+(define-fun |bal(@src,USD/2)@18| () Int (- |before(@src,USD/2)| $r9@18))
+(define-fun fail@20 () Bool (not (= $r9@18 10)))
+(define-fun alive@20 () Bool (= $r9@18 10))
+; 22: send_to_account(account: $r10)
+(define-fun |bal(@dest,USD/2)@22| () Int (+ |before(@dest,USD/2)| $r9@18))
+
+; outputs: the ledger applies nothing on failure
+(define-fun fails () Bool fail@20)
+(define-fun success () Bool (not fails))
+(define-fun |sent(@dest,USD/2)| () Int 0)
+(define-fun |received(@dest,USD/2)| () Int (ite fails 0 $r9@18))
+(define-fun |after(@dest,USD/2)| () Int (+ |before(@dest,USD/2)| (- |received(@dest,USD/2)| |sent(@dest,USD/2)|)))
+(define-fun |sent(@src,USD/2)| () Int (ite fails 0 $r9@18))
+(define-fun |received(@src,USD/2)| () Int 0)
+(define-fun |after(@src,USD/2)| () Int (+ |before(@src,USD/2)| (- |received(@src,USD/2)| |sent(@src,USD/2)|)))
+(define-fun |moved(@src,@dest,USD/2)| () Int (ite fails 0 $r9@18))
+```
+
+Per property, `prove.Problem` appends `; property <name>: <formula>`, `(define-fun property () Bool …)` and `(assert (not property))`; the driver adds `(check-sat)` and a `(get-value …)` of every input and output. A pair a property names and the script never touches gets a free `before`, `after` equal to it and zero totals (`Problem.AddKeys`).
+
+Three mechanisms keep the model honest. Every counterexample is replayed on the real VM, and a model the VM does not reproduce, or on which the property is not actually false, is a `tool-bug`, never a counterexample. Differential tests evaluate the model at concrete balances with `smt.Eval`, without a solver, and compare every output with `vm.Exec`: `encode/sweep_test.go` runs the spec corpus in `internal/interpreter/testdata/script-tests`, where 166 of 234 scripts encode (the rest use vars, colors, scopes or scaling) and all 172 of their test cases agree, and `encode/funds_ir_test.go` does the same on hand-written IR for shapes the compiler never emits (a capped send smaller than the queue, a negative cap, an uncapped overdraft pull, an asset switch between pull and send, a queue left undrained, `kept` then send, `save` then pull). Finally `prove_test.go` cross-checks every `valid` verdict of the fixtures on 64 seeded random balance assignments (values in `[-200, 400]`, one in four drawn from `{0, 50, 100, 150}`) run through the VM with the formula evaluated by `prop.Eval`; counterexample models are not pinned, since they depend on the solver, but each must replay-confirm.
+
+## Extension path
+
+Vars come first, in three steps. Bind `load_var` to constants given on the command line, an options argument to `Encode` that turns `load_var<str>` into a string constant and `load_var<int>` into an int literal; that alone unlocks `TestGeneratedScriptsAgreeWithVM`, which today encodes 0 of 200 generated scripts because 189 use vars (the other 11 overflow a register bank). Then symbolic ints: a `load_var<int>` becomes a free `Int` input, declared and reported like a balance, so a property can quantify over the amount. Then account vars by case split: `$dest` is one of the k literal accounts or a fresh (k+1)-th, each key guarded by the alias it falls under, which keeps the touched set finite.
+
+Metadata reads become free symbols: `meta<int>` a free `Int`, `meta<str>` a free string that only `str_eq` against constants inspects, a finite case split per comparison. `forall`, `exists` and `sum` expand over the known accounts and assets as described under [Quantifiers](#quantifiers). Colors and scopes become extra dimensions of `encode.Key` (`problem.go` notes they are `""` in v1), with the property atoms growing matching arguments. Tagged monetary literals, `[USD/2 100]` as an int whose asset must match the atom it is compared with, are a typecheck rule rather than a new value.