# Progress on formally verifying Simplicity

**URL:** <https://community.simplicity-lang.org/t/progress-on-formally-verifying-simplicity/91>\
**Category:** Formal verification\
**Created:** [October 14, 2026, 9:11pm UTC](https://community.simplicity-lang.org/t/progress-on-formally-verifying-simplicity/91 "2026-10-14T21:11:55Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![Breno](https://yyz1.discourse-cdn.com/flex007/user_avatar/community.simplicity-lang.org/breno/32/69_2.png) [@Breno](https://community.simplicity-lang.org/u/Breno)\
**Post date:** [October 14, 2026, 9:11pm UTC](https://community.simplicity-lang.org/t/progress-on-formally-verifying-simplicity/91/1 "2026-10-14T21:11:55Z")

</div>

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.

[Explore the code and verification records](https://github.com/brenorb/simplicity/tree/feat/jet-equivalence). Contributions are welcome!

---

<div class="post-metadata">

**Author:** ![schoen](https://avatars.discourse-cdn.com/v4/letter/s/b3f665/32.png) [@schoen](https://community.simplicity-lang.org/u/schoen)\
**Post date:** [October 18, 2026, 6:47pm UTC](https://community.simplicity-lang.org/t/progress-on-formally-verifying-simplicity/91/2 "2026-10-18T18:47:41Z")

</div>

That’s awesome, @Breno!

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?

---

<div class="post-metadata">

**Author:** ![Breno](https://yyz1.discourse-cdn.com/flex007/user_avatar/community.simplicity-lang.org/breno/32/69_2.png) [@Breno](https://community.simplicity-lang.org/u/Breno)\
**Post date:** [October 19, 2026, 8:01pm UTC](https://community.simplicity-lang.org/t/progress-on-formally-verifying-simplicity/91/3 "2026-10-19T20:01:02Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![schoen](https://avatars.discourse-cdn.com/v4/letter/s/b3f665/32.png) [@schoen](https://community.simplicity-lang.org/u/schoen)\
**Post date:** [October 19, 2026, 9:20pm UTC](https://community.simplicity-lang.org/t/progress-on-formally-verifying-simplicity/91/4 "2026-10-19T21:20:04Z")

</div>

Thanks!

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.