Lompat ke konten utama
Keamanan & pengujian

Verifereum

Verifikasi formal

Kunjungi situs web (buka di tab baru)Verifereum di X (buka di tab baru)Verifereum di GitHub (buka di tab baru)

Lihat selanjutnya

Certora AutoProver

Tentang Verifereum

Verifereum menghubungkan kontrak pintar Ethereum ke pembuktian teorema yang didukung HOL4 sehingga Anda dapat menargetkan klaim kebenaran yang sangat kuat ketika pendekatan SMT otomatis tidak cukup.

Tag

  • Keamanan
  • Edukasi
  • Verifikasi formal

Repositoriverifereum

Info

Tipe
Verifikasi formal
Bintang GitHub
54
Lisensi
GPL-3.0
Pencantuman ditinjau
Juni 2026

Alat serupa

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM adalah semantik yang dapat dieksekusi K-framework dari EVM: arahkan ke kode bita saat Anda memerlukan eksekusi yang diperiksa kesesuaiannya, eksplorasi simbolik, penalaran gas, atau bukti yang melacak aturan Ethereum dengan cermat.

hax

hax

hax adalah alat untuk terjemahan jaminan tinggi dari sebagian besar Rust ke dalam bahasa formal seperti F* atau Rocq.

Certora Prover

Certora Prover

Certora Prover is a cloud formal-verification service that checks specifications written in CVL against deployed contract code. Verification engineers use it to prove that a contract holds stated properties for all inputs.