Search results

remove metavariables flag

Status: Open.

#13 In for-all-dev/formal-confinement;

· quinn-dougherty opened on May 23, 2025

Write "compiler" that takes informal spec notation and returns assertions in Lean

Status: Open.

#10 In for-all-dev/formal-confinement;

· quinn-dougherty opened on May 20, 2025

Experiments: subversive code

Status: Open.

#9 In for-all-dev/formal-confinement;

· quinn-dougherty opened on May 20, 2025

More examples in Artifacts.{Negative,Positive}Tests and copy them over to proof.system.prompt

Status: Open.

#3 In for-all-dev/formal-confinement;

· quinn-dougherty opened on May 13, 2025

Write tactics for hoare proofs

Status: Open.

#2 In for-all-dev/formal-confinement;

· quinn-dougherty opened on May 13, 2025

solve sorrys in hoare_while

Status: Open.

#1 In for-all-dev/formal-confinement;

· quinn-dougherty opened on May 13, 2025