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 <code>Artifacts.{Negative,Positive}Tests</code> and copy them over to <code>proof.system.prompt</code>

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 <code>sorry</code>s in <code>hoare_while</code>

Status: Open.

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

· quinn-dougherty opened on May 13, 2025