Over the past few weeks, I’ve been working on formally verifying Simplicity’s C jets—optimized implementations of Simplicity operations—against their formal specifications.
The objective is to establish whether the actual C code behaves as specified, including outputs, success/failure behavior, and relevant memory effects. Proving agreement provides assurance; demonstrating a mismatch helps identify a bug.
The work now spans 858 incremental commits. Of 533 jets, the proof registry contains 364 implementation-to-specification contracts (68%):
260 without an additional libc premise.
104 conditional on an explicit memcpy model, which does not establish correctness of the system libc implementation.
Alongside these contracts, the project includes shared lemmas, partial proofs, memory and environment construction, initialization proofs, and verification tooling. This supporting work is essential to making the individual jet proofs meaningful and reusable.
Verification is still ongoing. These counts describe registered formal contracts, not exhaustive certification of the library. Results have explicit assumptions and build-configuration boundaries, and review of specification correspondence and intended input-domain coverage remains incomplete.
Can you explain more about the memcpy assumption? Is the idea that we currently have to add an additional axiom that asserts some property of memcpy’s behavior that cannot be deduced rigorously from the actual libc code? What kind of property is that?
Not exactly. It’s not a new global axiom, but a conditional theorem instead. The theorem states that If memcpy works as intended, the jet behaves as specified.
memcpy is a libc function whose implementation we haven’t verified, so we assume it works as it should and we prove the jets based on that assumption. Once we prove that the libc memcpy behaves as assumed, we can supply that proof and remove this particular assumption from the jet proofs.
I asked another AI agent to take a look at the assumption about memcpy, and it suggested that, in all of the places that memcpy is actually used in the Simplicity jet implementations, the amount of memory copied (n) is always 64 bytes or less, with no exceptions.
Therefore, the AI suggested that we could actually weaken the assumption by adding /\ n <= 64, that is, by saying “assuming that memcpy works as intended for copying 64 bytes or less”. The agent suggested that this is actually easier to reason about because it will exercise fewer branches of the memcpy implementation’s code.
This is slightly complicated because there are many different implementations of memcpy that will be available in different settings depending on the compiler or the machine architecture, but it looks like it’s correct overall, that it’s comparatively easier to confirm that it’s correct for buffer sizes less than or equal to 64 bytes, as this will often use a comparatively simple code path in the C or assembly memcpy implementation.