A proof-producing compiler for blockchain applications

DOI10.1007/S10817-025-09723-YMaRDI QIDQ6977539zbMATH OpenFDO

Authors Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman

Publication date 28 May 2025

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-025-09723-Y

zbMATH Keywords

formal verificationinteractive proof systemssmart contracts

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Cryptography (94A60)

Cites work

• A formal library for elliptic curves in the Coq proof assistant
• A proof-producing compiler for blockchain applications
• An elementary formal proof of the group law on Weierstrass elliptic curves in any characteristic
• CakeML
• Dafny: an automatic program verifier for functional correctness
• Formal Proof of the Group Law for Edwards Elliptic Curves
• Guarded commands, nondeterminacy and formal derivation of programs
• Metamath Zero: designing a theorem prover prover
• Proof-producing synthesis of CakeML from monadic HOL functions
• Secure distributed programming with value-dependent types
• The Lean 4 theorem prover and programming language
• The Lean theorem prover (system description)
• Why3 -- where programs meet provers

This page was built for publication: A proof-producing compiler for blockchain applications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6977539)