Josh Gancher
@jgancher.bsky.social
Assistant Prof @ Northeastern. Formal verification + security + crypto. https://gancher.dev
One kind of cool thing I did at CMU (with others) is mechanize verified proof checker for Datalog traces: github.com/secure-found...
Given a trace made by an untrusted solver, the Dafny code replays the trace and builds a proof tree in ghost. By construction, only valid proof trees can be created
Given a trace made by an untrusted solver, the Dafny code replays the trace and builds a proof tree in ghost. By construction, only valid proof trees can be created
veri-datalog/dafny/lcf/def.dfy at trace-reconstruction · secure-foundations/veri-datalog
Verified Datalog. Contribute to secure-foundations/veri-datalog development by creating an account on GitHub.
github.com
May 28, 2025 at 8:22 PM
One kind of cool thing I did at CMU (with others) is mechanize verified proof checker for Datalog traces: github.com/secure-found...
Given a trace made by an untrusted solver, the Dafny code replays the trace and builds a proof tree in ghost. By construction, only valid proof trees can be created
Given a trace made by an untrusted solver, the Dafny code replays the trace and builds a proof tree in ghost. By construction, only valid proof trees can be created