From: jeremy <jeremy.l.rubin@gmail.com>
To: Bitcoin Development Mailing List <bitcoindev@googlegroups.com>
Subject: [bitcoindev] Re: Formal verification of secp256k1 modular scalar multiplication
Date: Wed, 15 Apr 2026 11:39:41 -0700 (PDT) [thread overview]
Message-ID: <531d1095-435c-4e8f-b8d1-8fdc26aeab2cn@googlegroups.com> (raw)
In-Reply-To: <09b8adf7-0faa-4efa-b53a-7d29a5f40c12@mailbox.org>
[-- Attachment #1.1: Type: text/plain, Size: 2842 bytes --]
This is really neat!
For my purify impl[0], I've also had some success with using CBMC on a toy
curve prime to "prove" correctness, but an actually Rocq proof is obviously
better.
[0] https://judica.org/purify
On Tuesday, April 7, 2026 at 8:13:01 AM UTC-4 remix7531 wrote:
> Hi all,
>
> I have been lurking on this list for years. It is time for my first post.
>
> This is my first result under my OpenSats grant [0]. Full writeup
> with technical details and Rocq (formerly Coq) code examples is on
> my blog [1].
>
> Code and proofs are available on GitHub [2].
>
> I produced a machine-checked proof that secp256k1_scalar_mul computes
> r = a * b mod N correctly for all representable inputs, where N is the
> secp256k1 group order. The proof covers arithmetic correctness, absence
> of integer overflow in all intermediate computations, and memory safety.
> Scalar multiplication sits on the critical path of every signature
> operation.
>
> Together with all supporting helpers, the verified code totals roughly
> 300 lines of C. The proof code totals ~6,400 lines in Rocq, giving a
> proof-to-code ratio of roughly 21:1.
>
> I verified the non-assembly, 64-bit only fallback path using the
> Verified Software Toolchain (VST) [3]. The verified code differs
> from upstream in two ways: assert statements are removed
> (not present in production builds) and macros are converted to
> inline functions. The algorithmic logic is unchanged. When compiled
> with CompCert, the correctness guarantee extends from the
> mathematical specification to assembly.
>
> One mistake I made was a missing "mod 2^256" in a helper
> specification, which made it unprovable. The code was correct,
> the error was in my specification. The proof assistant caught it
> because the proof cannot go through when the specification does
> not match the code's behavior.
>
> Next targets are porting to RefinedC for a framework comparison,
> verifying Pippenger's algorithm for batch signature verification
> (axiomatizing group operations), and evaluating Cryptol/SAW.
>
> Feedback welcome.
>
> remix7531
>
> [0]
>
> https://opensats.org/blog/sixteenth-wave-of-bitcoin-grants#advancing-formal-verification-for-bitcoin-cryptography
> [1] https://remix7531.com/post/formal_verification_secp256k1_scalar_mul/
> [2] https://github.com/remix7531/secp256k1-scalar-fv-test
> [3] https://vst.cs.princeton.edu/
>
>
--
You received this message because you are subscribed to the Google Groups "Bitcoin Development Mailing List" group.
To unsubscribe from this group and stop receiving emails from it, send an email to bitcoindev+unsubscribe@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/bitcoindev/531d1095-435c-4e8f-b8d1-8fdc26aeab2cn%40googlegroups.com.
[-- Attachment #1.2: Type: text/html, Size: 4790 bytes --]
prev parent reply other threads:[~2026-04-15 18:47 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2026-04-07 11:56 [bitcoindev] " 'remix7531' via Bitcoin Development Mailing List
2026-04-15 18:39 ` jeremy [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=531d1095-435c-4e8f-b8d1-8fdc26aeab2cn@googlegroups.com \
--to=jeremy.l.rubin@gmail.com \
--cc=bitcoindev@googlegroups.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox