LLM2Cert synthesizes certificates checked by SMT solvers and Lean
The method verifies 81 of 105 DynaCertBench instances, 17.1 points above one-shot proposals without feedback.
Stories per day · 30 days
Relatedformal-verification2barrier-certificates1benchmark1hoare-logic1lean1lyapunov1mpc1secret-sharing1type-system1
3 stories, newest first · one card per story
Stories tagged #smt
SMT-Boosted Security Types and Correctness for Low-Level MPC
An SMT-backed type system and Hoare logic check correctness and security of low-level MPC protocols.
Access Control as Verified Parse Constraints
Researchers verify a class of EverParse validators that correctly enforce access-control policies, deploying a machine-checked enforcement gate on seL4.