Veridise has worked on our usage of elliptic curve divisors to prove scalar multiplications. They have proved the original technique, the technique when taking the logarithmic derivative, and the technique when evaluated over finite fields. This leaves the formal definition of an interactive protocol and verifying the R1CS defined in the FCMP++ paper aligns.
The prior scope of work (logarithmic derivative, finite fields) was approved with understanding this scope of work would follow.
The estimate is for 40-50 hours at the prior-worked-under rate of $250 an hour. This effects a request of 12,500 USD which will be conducted via MAGIC (as prior work with Veridise has been).
I will caveat this may not be the final contract with Veridise on this topic if we have them formally respond to review comments (which may be necessary or may solely be a nice-to-have depending on how the review goes) or if the work takes longer than expected (which I don't believe likely).
Veridise is the best candidate for this work given their strong work on divisors already and their existing work on R1CS systems generally, and the rate is reasonable. Easy +1 from me.