Your verifier is probably lying to you about floats

Here is a promise that looks obviously true:

fn add_twice(x: Float) -> Float
    ensures result == x + 0.2
{
    return x + 0.1 + 0.1
}

Adding a tenth twice is the same as adding two tenths. Every algebra

teacher you have ever had agrees. Most program verifiers agree too.

They are wrong, and so is the promise.

Velaris refuses to prove it, and hands back the number that breaks it:

error[E700] promise cannot be kept: 'add_twice' ensures result == x + 0.2
  proven without running the program:
    x = -1.207290298954004637010939404717646539211273193359375
    gives result = -1.007290298954004459375255464692600071430206298828125

That is not a rounding display artifact. Those are two different

doubles, and the program really does produce the second one.

Why the lie is tempting

To prove things about numbers, a verifier translates your code into

formulas for a solver. The question is which *theory* to translate

into.

The comfortable choice is the theory of real numbers. Reals are

associative, commutative, infinitely precise, and solvers are fast at

them. Translate Float to Real and everything works beautifully:

proofs come back in milliseconds, and x + 0.1 + 0.1 == x + 0.2 is

trivially true.

It is also a statement about a machine that does not exist.

Your processor implements IEEE-754 binary64. In that world 0.1 is not

one tenth — it is the nearest double to one tenth, which is

0.1000000000000000055511151231257827021181583404541015625. Every

operation rounds to the nearest representable value. Addition is not

associative. Adding a tenth twice takes two rounding steps; adding two

tenths takes one. For many values of x those disagree in the last

bit, and one bit is all it takes for == to be false.

So a verifier that models floats as reals will happily certify code

that fails on the machine it is compiled for. The proof is valid. The

theorem is about the wrong object.

What honesty costs

Z3 has a floating-point theory that implements IEEE-754 exactly:

rounding modes, subnormals, infinities, NaN, signed zero. Velaris

translates Float into that theory rather than into Real.

The bill arrives immediately.

It is slow. The FP theory is decided by bit-blasting — expanding

64-bit values into circuits of individual bits and handing the result

to a SAT solver. The refutation above takes about fifteen seconds.

Integer proofs in the same compiler finish in milliseconds. Velaris

gives float queries a thirty second budget and everything else three

seconds, and only pays the larger cost for functions that actually

mention floats.

Fewer things are provable. Plenty of true-in-the-reals facts are

simply false in IEEE-754, and plenty of true-in-IEEE facts are too

expensive to establish. A verifier that pretends floats are reals has a

much better success rate on paper. It is winning a game nobody should

want to play.

Equality gets strange, correctly. Velaris compares floats with

fpEQ, not structural equality, which means NaN is not equal to itself

and positive zero equals negative zero. Both are IEEE behaviour, and

both surprise people. Using structural equality would have been faster

and easier to explain, and would have quietly produced false results at

the edges.

There is a bonus that only shows up once you are honest: comparison

constraints start doing real work. A precondition like `requires

x >= 0.0` silently rules out NaN, because NaN fails every comparison.

The prover knows that, so a promise you could not otherwise establish

sometimes becomes provable for free.

The rule underneath

Velaris has one commitment it will not trade away: **it never claims

something is proven unless the claim is literally true.**

That single rule decided the float design by itself. If you model

floats as reals, "proven" starts meaning "proven about an idealised

machine that does not exist," and the word has quietly been devalued.

Everything after that is negotiation.

The same rule shows up elsewhere in the compiler. Division and modulo

are not native-compiled, because a native fdiv by zero yields

infinity while the language promises a clean error, and two execution

modes that disagree are worse than one slow mode. A premise the solver

cannot translate aborts the whole proof rather than being silently

dropped, because proving with dropped premises manufactures false

counterexamples. Anything unprovable degrades to a runtime check rather

than being waved through.

None of these make the demo look better. All of them are the reason the

demo can be believed.

Try it

The compiler runs in your browser, no install:

<https://gowrishankar-infra.github.io/velaris-lang/playground.html>

Paste the function at the top of this page and watch it refuse. Then

change ensures result == x + 0.2 to something IEEE actually

guarantees — say ensures result >= x — and watch it go through.

If you can make Velaris say "proven" about something that is false at

runtime, that is a soundness bug, and this project treats those as

security reports.

<https://github.com/gowrishankar-infra/velaris-lang>