Location: Montréal, Canada
Remote: Yes; on-site or hybrid in Montréal also fine
Willing to relocate: No
Technologies: TLA+/PlusCal, Alloy, Z3/CVC5, property-based testing, Python, Java, Go, Haskell, Perl, Postgres, Kubernetes, Terraform pipelines
Email: clavoie+hackernews [at] sandreckoning [dot] com
Twenty-plus years building and operating software, including six at Google (Ads, Search, Street View), and nearly two decades running a Montréal consultancy doing technical due diligence and large-scale infrastructure work. Specialised in:
* Applied formal methods. Specification and model checking aimed at the parts that cannot break. TLA+ or Alloy models, SMT-backed invariants, and property-based tests wired into CI. The goal is catching design defects before implementation, not verifying an entire codebase.
* Interviewing and hiring. Calibrated interviews, structured debriefs, work-sample and pairing exercises. Interviewer training.
* Managing AI-assisted engineering. Practical work here: specification-first workflows where the spec is machine-checkable, eval suites and regression
harnesses.
* Applied formal methods. Specification and model checking aimed at the parts that cannot break. TLA+ or Alloy models, SMT-backed invariants, and property-based tests wired into CI. The goal is catching design defects before implementation, not verifying an entire codebase.
* Interviewing and hiring. Calibrated interviews, structured debriefs, work-sample and pairing exercises. Interviewer training.
* Managing AI-assisted engineering. Practical work here: specification-first workflows where the spec is machine-checkable, eval suites and regression harnesses.
Fully bilingual: French and English.