Solidity NTC alternative

I read a while back some blogs on another Non Turing Complete language to write smart contracts. It was I believe written by a team at Stanford and had a Coq proof verifier attached to it. The name ended up with "ty" I think. Can anyone please refresh my memory about how it's called?